Step | Hyp | Ref
| Expression |
1 | | 1n0 7575 |
. . . . . . 7
⊢
1𝑜 ≠ ∅ |
2 | | df-br 4654 |
. . . . . . . 8
⊢ ((𝑓‘𝑛){〈1𝑜,
1𝑜〉} (𝑓‘suc 𝑛) ↔ 〈(𝑓‘𝑛), (𝑓‘suc 𝑛)〉 ∈ {〈1𝑜,
1𝑜〉}) |
3 | | elsni 4194 |
. . . . . . . . 9
⊢
(〈(𝑓‘𝑛), (𝑓‘suc 𝑛)〉 ∈ {〈1𝑜,
1𝑜〉} → 〈(𝑓‘𝑛), (𝑓‘suc 𝑛)〉 = 〈1𝑜,
1𝑜〉) |
4 | | fvex 6201 |
. . . . . . . . . 10
⊢ (𝑓‘𝑛) ∈ V |
5 | | fvex 6201 |
. . . . . . . . . 10
⊢ (𝑓‘suc 𝑛) ∈ V |
6 | 4, 5 | opth1 4944 |
. . . . . . . . 9
⊢
(〈(𝑓‘𝑛), (𝑓‘suc 𝑛)〉 = 〈1𝑜,
1𝑜〉 → (𝑓‘𝑛) = 1𝑜) |
7 | 3, 6 | syl 17 |
. . . . . . . 8
⊢
(〈(𝑓‘𝑛), (𝑓‘suc 𝑛)〉 ∈ {〈1𝑜,
1𝑜〉} → (𝑓‘𝑛) = 1𝑜) |
8 | 2, 7 | sylbi 207 |
. . . . . . 7
⊢ ((𝑓‘𝑛){〈1𝑜,
1𝑜〉} (𝑓‘suc 𝑛) → (𝑓‘𝑛) = 1𝑜) |
9 | | tz6.12i 6214 |
. . . . . . 7
⊢
(1𝑜 ≠ ∅ → ((𝑓‘𝑛) = 1𝑜 → 𝑛𝑓1𝑜)) |
10 | 1, 8, 9 | mpsyl 68 |
. . . . . 6
⊢ ((𝑓‘𝑛){〈1𝑜,
1𝑜〉} (𝑓‘suc 𝑛) → 𝑛𝑓1𝑜) |
11 | | vex 3203 |
. . . . . . 7
⊢ 𝑛 ∈ V |
12 | | 1on 7567 |
. . . . . . . 8
⊢
1𝑜 ∈ On |
13 | 12 | elexi 3213 |
. . . . . . 7
⊢
1𝑜 ∈ V |
14 | 11, 13 | breldm 5329 |
. . . . . 6
⊢ (𝑛𝑓1𝑜 → 𝑛 ∈ dom 𝑓) |
15 | 10, 14 | syl 17 |
. . . . 5
⊢ ((𝑓‘𝑛){〈1𝑜,
1𝑜〉} (𝑓‘suc 𝑛) → 𝑛 ∈ dom 𝑓) |
16 | 15 | ralimi 2952 |
. . . 4
⊢
(∀𝑛 ∈
ω (𝑓‘𝑛){〈1𝑜,
1𝑜〉} (𝑓‘suc 𝑛) → ∀𝑛 ∈ ω 𝑛 ∈ dom 𝑓) |
17 | | dfss3 3592 |
. . . 4
⊢ (ω
⊆ dom 𝑓 ↔
∀𝑛 ∈ ω
𝑛 ∈ dom 𝑓) |
18 | 16, 17 | sylibr 224 |
. . 3
⊢
(∀𝑛 ∈
ω (𝑓‘𝑛){〈1𝑜,
1𝑜〉} (𝑓‘suc 𝑛) → ω ⊆ dom 𝑓) |
19 | | vex 3203 |
. . . . 5
⊢ 𝑓 ∈ V |
20 | 19 | dmex 7099 |
. . . 4
⊢ dom 𝑓 ∈ V |
21 | 20 | ssex 4802 |
. . 3
⊢ (ω
⊆ dom 𝑓 →
ω ∈ V) |
22 | 18, 21 | syl 17 |
. 2
⊢
(∀𝑛 ∈
ω (𝑓‘𝑛){〈1𝑜,
1𝑜〉} (𝑓‘suc 𝑛) → ω ∈ V) |
23 | | snex 4908 |
. . 3
⊢
{〈1𝑜, 1𝑜〉} ∈
V |
24 | 13, 13 | fvsn 6446 |
. . . . . . . 8
⊢
({〈1𝑜,
1𝑜〉}‘1𝑜) =
1𝑜 |
25 | 13, 13 | funsn 5939 |
. . . . . . . . 9
⊢ Fun
{〈1𝑜, 1𝑜〉} |
26 | 13 | snid 4208 |
. . . . . . . . . 10
⊢
1𝑜 ∈ {1𝑜} |
27 | 13 | dmsnop 5609 |
. . . . . . . . . 10
⊢ dom
{〈1𝑜, 1𝑜〉} =
{1𝑜} |
28 | 26, 27 | eleqtrri 2700 |
. . . . . . . . 9
⊢
1𝑜 ∈ dom {〈1𝑜,
1𝑜〉} |
29 | | funbrfvb 6238 |
. . . . . . . . 9
⊢ ((Fun
{〈1𝑜, 1𝑜〉} ∧
1𝑜 ∈ dom {〈1𝑜,
1𝑜〉}) → (({〈1𝑜,
1𝑜〉}‘1𝑜) =
1𝑜 ↔ 1𝑜{〈1𝑜,
1𝑜〉}1𝑜)) |
30 | 25, 28, 29 | mp2an 708 |
. . . . . . . 8
⊢
(({〈1𝑜,
1𝑜〉}‘1𝑜) =
1𝑜 ↔ 1𝑜{〈1𝑜,
1𝑜〉}1𝑜) |
31 | 24, 30 | mpbi 220 |
. . . . . . 7
⊢
1𝑜{〈1𝑜,
1𝑜〉}1𝑜 |
32 | | breq12 4658 |
. . . . . . . 8
⊢ ((𝑠 = 1𝑜 ∧
𝑡 = 1𝑜)
→ (𝑠{〈1𝑜,
1𝑜〉}𝑡 ↔
1𝑜{〈1𝑜,
1𝑜〉}1𝑜)) |
33 | 13, 13, 32 | spc2ev 3301 |
. . . . . . 7
⊢
(1𝑜{〈1𝑜,
1𝑜〉}1𝑜 → ∃𝑠∃𝑡 𝑠{〈1𝑜,
1𝑜〉}𝑡) |
34 | 31, 33 | ax-mp 5 |
. . . . . 6
⊢
∃𝑠∃𝑡 𝑠{〈1𝑜,
1𝑜〉}𝑡 |
35 | | breq 4655 |
. . . . . . 7
⊢ (𝑥 = {〈1𝑜,
1𝑜〉} → (𝑠𝑥𝑡 ↔ 𝑠{〈1𝑜,
1𝑜〉}𝑡)) |
36 | 35 | 2exbidv 1852 |
. . . . . 6
⊢ (𝑥 = {〈1𝑜,
1𝑜〉} → (∃𝑠∃𝑡 𝑠𝑥𝑡 ↔ ∃𝑠∃𝑡 𝑠{〈1𝑜,
1𝑜〉}𝑡)) |
37 | 34, 36 | mpbiri 248 |
. . . . 5
⊢ (𝑥 = {〈1𝑜,
1𝑜〉} → ∃𝑠∃𝑡 𝑠𝑥𝑡) |
38 | | ssid 3624 |
. . . . . . 7
⊢
{1𝑜} ⊆ {1𝑜} |
39 | 13 | rnsnop 5616 |
. . . . . . 7
⊢ ran
{〈1𝑜, 1𝑜〉} =
{1𝑜} |
40 | 38, 39, 27 | 3sstr4i 3644 |
. . . . . 6
⊢ ran
{〈1𝑜, 1𝑜〉} ⊆ dom
{〈1𝑜, 1𝑜〉} |
41 | | rneq 5351 |
. . . . . . 7
⊢ (𝑥 = {〈1𝑜,
1𝑜〉} → ran 𝑥 = ran {〈1𝑜,
1𝑜〉}) |
42 | | dmeq 5324 |
. . . . . . 7
⊢ (𝑥 = {〈1𝑜,
1𝑜〉} → dom 𝑥 = dom {〈1𝑜,
1𝑜〉}) |
43 | 41, 42 | sseq12d 3634 |
. . . . . 6
⊢ (𝑥 = {〈1𝑜,
1𝑜〉} → (ran 𝑥 ⊆ dom 𝑥 ↔ ran {〈1𝑜,
1𝑜〉} ⊆ dom {〈1𝑜,
1𝑜〉})) |
44 | 40, 43 | mpbiri 248 |
. . . . 5
⊢ (𝑥 = {〈1𝑜,
1𝑜〉} → ran 𝑥 ⊆ dom 𝑥) |
45 | | pm5.5 351 |
. . . . 5
⊢
((∃𝑠∃𝑡 𝑠𝑥𝑡 ∧ ran 𝑥 ⊆ dom 𝑥) → (((∃𝑠∃𝑡 𝑠𝑥𝑡 ∧ ran 𝑥 ⊆ dom 𝑥) → ∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛)) ↔ ∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛))) |
46 | 37, 44, 45 | syl2anc 693 |
. . . 4
⊢ (𝑥 = {〈1𝑜,
1𝑜〉} → (((∃𝑠∃𝑡 𝑠𝑥𝑡 ∧ ran 𝑥 ⊆ dom 𝑥) → ∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛)) ↔ ∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛))) |
47 | | breq 4655 |
. . . . . 6
⊢ (𝑥 = {〈1𝑜,
1𝑜〉} → ((𝑓‘𝑛)𝑥(𝑓‘suc 𝑛) ↔ (𝑓‘𝑛){〈1𝑜,
1𝑜〉} (𝑓‘suc 𝑛))) |
48 | 47 | ralbidv 2986 |
. . . . 5
⊢ (𝑥 = {〈1𝑜,
1𝑜〉} → (∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛) ↔ ∀𝑛 ∈ ω (𝑓‘𝑛){〈1𝑜,
1𝑜〉} (𝑓‘suc 𝑛))) |
49 | 48 | exbidv 1850 |
. . . 4
⊢ (𝑥 = {〈1𝑜,
1𝑜〉} → (∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛) ↔ ∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛){〈1𝑜,
1𝑜〉} (𝑓‘suc 𝑛))) |
50 | 46, 49 | bitrd 268 |
. . 3
⊢ (𝑥 = {〈1𝑜,
1𝑜〉} → (((∃𝑠∃𝑡 𝑠𝑥𝑡 ∧ ran 𝑥 ⊆ dom 𝑥) → ∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛)) ↔ ∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛){〈1𝑜,
1𝑜〉} (𝑓‘suc 𝑛))) |
51 | | ax-dc 9268 |
. . 3
⊢
((∃𝑠∃𝑡 𝑠𝑥𝑡 ∧ ran 𝑥 ⊆ dom 𝑥) → ∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛)) |
52 | 23, 50, 51 | vtocl 3259 |
. 2
⊢
∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛){〈1𝑜,
1𝑜〉} (𝑓‘suc 𝑛) |
53 | 22, 52 | exlimiiv 1859 |
1
⊢ ω
∈ V |