Step | Hyp | Ref
| Expression |
1 | | 1n0 7462 |
. . . . . . 7
⊢
1𝑜 ≠ ∅ |
2 | | df-br 4584 |
. . . . . . . 8
⊢ ((𝑓‘𝑛){〈1𝑜,
1𝑜〉} (𝑓‘suc 𝑛) ↔ 〈(𝑓‘𝑛), (𝑓‘suc 𝑛)〉 ∈ {〈1𝑜,
1𝑜〉}) |
3 | | elsni 4142 |
. . . . . . . . 9
⊢
(〈(𝑓‘𝑛), (𝑓‘suc 𝑛)〉 ∈ {〈1𝑜,
1𝑜〉} → 〈(𝑓‘𝑛), (𝑓‘suc 𝑛)〉 = 〈1𝑜,
1𝑜〉) |
4 | | fvex 6113 |
. . . . . . . . . 10
⊢ (𝑓‘𝑛) ∈ V |
5 | | fvex 6113 |
. . . . . . . . . 10
⊢ (𝑓‘suc 𝑛) ∈ V |
6 | 4, 5 | opth1 4870 |
. . . . . . . . 9
⊢
(〈(𝑓‘𝑛), (𝑓‘suc 𝑛)〉 = 〈1𝑜,
1𝑜〉 → (𝑓‘𝑛) = 1𝑜) |
7 | 3, 6 | syl 17 |
. . . . . . . 8
⊢
(〈(𝑓‘𝑛), (𝑓‘suc 𝑛)〉 ∈ {〈1𝑜,
1𝑜〉} → (𝑓‘𝑛) = 1𝑜) |
8 | 2, 7 | sylbi 206 |
. . . . . . 7
⊢ ((𝑓‘𝑛){〈1𝑜,
1𝑜〉} (𝑓‘suc 𝑛) → (𝑓‘𝑛) = 1𝑜) |
9 | | tz6.12i 6124 |
. . . . . . 7
⊢
(1𝑜 ≠ ∅ → ((𝑓‘𝑛) = 1𝑜 → 𝑛𝑓1𝑜)) |
10 | 1, 8, 9 | mpsyl 66 |
. . . . . 6
⊢ ((𝑓‘𝑛){〈1𝑜,
1𝑜〉} (𝑓‘suc 𝑛) → 𝑛𝑓1𝑜) |
11 | | vex 3176 |
. . . . . . 7
⊢ 𝑛 ∈ V |
12 | | 1on 7454 |
. . . . . . . 8
⊢
1𝑜 ∈ On |
13 | 12 | elexi 3186 |
. . . . . . 7
⊢
1𝑜 ∈ V |
14 | 11, 13 | breldm 5251 |
. . . . . 6
⊢ (𝑛𝑓1𝑜 → 𝑛 ∈ dom 𝑓) |
15 | 10, 14 | syl 17 |
. . . . 5
⊢ ((𝑓‘𝑛){〈1𝑜,
1𝑜〉} (𝑓‘suc 𝑛) → 𝑛 ∈ dom 𝑓) |
16 | 15 | ralimi 2936 |
. . . 4
⊢
(∀𝑛 ∈
ω (𝑓‘𝑛){〈1𝑜,
1𝑜〉} (𝑓‘suc 𝑛) → ∀𝑛 ∈ ω 𝑛 ∈ dom 𝑓) |
17 | | dfss3 3558 |
. . . 4
⊢ (ω
⊆ dom 𝑓 ↔
∀𝑛 ∈ ω
𝑛 ∈ dom 𝑓) |
18 | 16, 17 | sylibr 223 |
. . 3
⊢
(∀𝑛 ∈
ω (𝑓‘𝑛){〈1𝑜,
1𝑜〉} (𝑓‘suc 𝑛) → ω ⊆ dom 𝑓) |
19 | | vex 3176 |
. . . . 5
⊢ 𝑓 ∈ V |
20 | 19 | dmex 6991 |
. . . 4
⊢ dom 𝑓 ∈ V |
21 | 20 | ssex 4730 |
. . 3
⊢ (ω
⊆ dom 𝑓 →
ω ∈ V) |
22 | 18, 21 | syl 17 |
. 2
⊢
(∀𝑛 ∈
ω (𝑓‘𝑛){〈1𝑜,
1𝑜〉} (𝑓‘suc 𝑛) → ω ∈ V) |
23 | | snex 4835 |
. . 3
⊢
{〈1𝑜, 1𝑜〉} ∈
V |
24 | 13, 13 | fvsn 6351 |
. . . . . . . 8
⊢
({〈1𝑜,
1𝑜〉}‘1𝑜) =
1𝑜 |
25 | 13, 13 | funsn 5853 |
. . . . . . . . 9
⊢ Fun
{〈1𝑜, 1𝑜〉} |
26 | 13 | snid 4155 |
. . . . . . . . . 10
⊢
1𝑜 ∈ {1𝑜} |
27 | 13 | dmsnop 5527 |
. . . . . . . . . 10
⊢ dom
{〈1𝑜, 1𝑜〉} =
{1𝑜} |
28 | 26, 27 | eleqtrri 2687 |
. . . . . . . . 9
⊢
1𝑜 ∈ dom {〈1𝑜,
1𝑜〉} |
29 | | funbrfvb 6148 |
. . . . . . . . 9
⊢ ((Fun
{〈1𝑜, 1𝑜〉} ∧
1𝑜 ∈ dom {〈1𝑜,
1𝑜〉}) → (({〈1𝑜,
1𝑜〉}‘1𝑜) =
1𝑜 ↔ 1𝑜{〈1𝑜,
1𝑜〉}1𝑜)) |
30 | 25, 28, 29 | mp2an 704 |
. . . . . . . 8
⊢
(({〈1𝑜,
1𝑜〉}‘1𝑜) =
1𝑜 ↔ 1𝑜{〈1𝑜,
1𝑜〉}1𝑜) |
31 | 24, 30 | mpbi 219 |
. . . . . . 7
⊢
1𝑜{〈1𝑜,
1𝑜〉}1𝑜 |
32 | | breq12 4588 |
. . . . . . . 8
⊢ ((𝑠 = 1𝑜 ∧
𝑡 = 1𝑜)
→ (𝑠{〈1𝑜,
1𝑜〉}𝑡 ↔
1𝑜{〈1𝑜,
1𝑜〉}1𝑜)) |
33 | 13, 13, 32 | spc2ev 3274 |
. . . . . . 7
⊢
(1𝑜{〈1𝑜,
1𝑜〉}1𝑜 → ∃𝑠∃𝑡 𝑠{〈1𝑜,
1𝑜〉}𝑡) |
34 | 31, 33 | ax-mp 5 |
. . . . . 6
⊢
∃𝑠∃𝑡 𝑠{〈1𝑜,
1𝑜〉}𝑡 |
35 | | breq 4585 |
. . . . . . 7
⊢ (𝑥 = {〈1𝑜,
1𝑜〉} → (𝑠𝑥𝑡 ↔ 𝑠{〈1𝑜,
1𝑜〉}𝑡)) |
36 | 35 | 2exbidv 1839 |
. . . . . 6
⊢ (𝑥 = {〈1𝑜,
1𝑜〉} → (∃𝑠∃𝑡 𝑠𝑥𝑡 ↔ ∃𝑠∃𝑡 𝑠{〈1𝑜,
1𝑜〉}𝑡)) |
37 | 34, 36 | mpbiri 247 |
. . . . 5
⊢ (𝑥 = {〈1𝑜,
1𝑜〉} → ∃𝑠∃𝑡 𝑠𝑥𝑡) |
38 | | ssid 3587 |
. . . . . . 7
⊢
{1𝑜} ⊆ {1𝑜} |
39 | 13 | rnsnop 5534 |
. . . . . . 7
⊢ ran
{〈1𝑜, 1𝑜〉} =
{1𝑜} |
40 | 38, 39, 27 | 3sstr4i 3607 |
. . . . . 6
⊢ ran
{〈1𝑜, 1𝑜〉} ⊆ dom
{〈1𝑜, 1𝑜〉} |
41 | | rneq 5272 |
. . . . . . 7
⊢ (𝑥 = {〈1𝑜,
1𝑜〉} → ran 𝑥 = ran {〈1𝑜,
1𝑜〉}) |
42 | | dmeq 5246 |
. . . . . . 7
⊢ (𝑥 = {〈1𝑜,
1𝑜〉} → dom 𝑥 = dom {〈1𝑜,
1𝑜〉}) |
43 | 41, 42 | sseq12d 3597 |
. . . . . 6
⊢ (𝑥 = {〈1𝑜,
1𝑜〉} → (ran 𝑥 ⊆ dom 𝑥 ↔ ran {〈1𝑜,
1𝑜〉} ⊆ dom {〈1𝑜,
1𝑜〉})) |
44 | 40, 43 | mpbiri 247 |
. . . . 5
⊢ (𝑥 = {〈1𝑜,
1𝑜〉} → ran 𝑥 ⊆ dom 𝑥) |
45 | | pm5.5 350 |
. . . . 5
⊢
((∃𝑠∃𝑡 𝑠𝑥𝑡 ∧ ran 𝑥 ⊆ dom 𝑥) → (((∃𝑠∃𝑡 𝑠𝑥𝑡 ∧ ran 𝑥 ⊆ dom 𝑥) → ∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛)) ↔ ∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛))) |
46 | 37, 44, 45 | syl2anc 691 |
. . . 4
⊢ (𝑥 = {〈1𝑜,
1𝑜〉} → (((∃𝑠∃𝑡 𝑠𝑥𝑡 ∧ ran 𝑥 ⊆ dom 𝑥) → ∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛)) ↔ ∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛))) |
47 | | breq 4585 |
. . . . . 6
⊢ (𝑥 = {〈1𝑜,
1𝑜〉} → ((𝑓‘𝑛)𝑥(𝑓‘suc 𝑛) ↔ (𝑓‘𝑛){〈1𝑜,
1𝑜〉} (𝑓‘suc 𝑛))) |
48 | 47 | ralbidv 2969 |
. . . . 5
⊢ (𝑥 = {〈1𝑜,
1𝑜〉} → (∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛) ↔ ∀𝑛 ∈ ω (𝑓‘𝑛){〈1𝑜,
1𝑜〉} (𝑓‘suc 𝑛))) |
49 | 48 | exbidv 1837 |
. . . 4
⊢ (𝑥 = {〈1𝑜,
1𝑜〉} → (∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛) ↔ ∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛){〈1𝑜,
1𝑜〉} (𝑓‘suc 𝑛))) |
50 | 46, 49 | bitrd 267 |
. . 3
⊢ (𝑥 = {〈1𝑜,
1𝑜〉} → (((∃𝑠∃𝑡 𝑠𝑥𝑡 ∧ ran 𝑥 ⊆ dom 𝑥) → ∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛)) ↔ ∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛){〈1𝑜,
1𝑜〉} (𝑓‘suc 𝑛))) |
51 | | ax-dc 9151 |
. . 3
⊢
((∃𝑠∃𝑡 𝑠𝑥𝑡 ∧ ran 𝑥 ⊆ dom 𝑥) → ∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛)) |
52 | 23, 50, 51 | vtocl 3232 |
. 2
⊢
∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛){〈1𝑜,
1𝑜〉} (𝑓‘suc 𝑛) |
53 | 22, 52 | exlimiiv 1846 |
1
⊢ ω
∈ V |