Step | Hyp | Ref
| Expression |
1 | | 1n0 8435 |
. . . . . . 7
⊢
1o ≠ ∅ |
2 | | df-br 5107 |
. . . . . . . 8
⊢ ((𝑓‘𝑛){⟨1o, 1o⟩}
(𝑓‘suc 𝑛) ↔ ⟨(𝑓‘𝑛), (𝑓‘suc 𝑛)⟩ ∈ {⟨1o,
1o⟩}) |
3 | | elsni 4604 |
. . . . . . . . 9
⊢
(⟨(𝑓‘𝑛), (𝑓‘suc 𝑛)⟩ ∈ {⟨1o,
1o⟩} → ⟨(𝑓‘𝑛), (𝑓‘suc 𝑛)⟩ = ⟨1o,
1o⟩) |
4 | | fvex 6856 |
. . . . . . . . . 10
⊢ (𝑓‘𝑛) ∈ V |
5 | | fvex 6856 |
. . . . . . . . . 10
⊢ (𝑓‘suc 𝑛) ∈ V |
6 | 4, 5 | opth1 5433 |
. . . . . . . . 9
⊢
(⟨(𝑓‘𝑛), (𝑓‘suc 𝑛)⟩ = ⟨1o,
1o⟩ → (𝑓‘𝑛) = 1o) |
7 | 3, 6 | syl 17 |
. . . . . . . 8
⊢
(⟨(𝑓‘𝑛), (𝑓‘suc 𝑛)⟩ ∈ {⟨1o,
1o⟩} → (𝑓‘𝑛) = 1o) |
8 | 2, 7 | sylbi 216 |
. . . . . . 7
⊢ ((𝑓‘𝑛){⟨1o, 1o⟩}
(𝑓‘suc 𝑛) → (𝑓‘𝑛) = 1o) |
9 | | tz6.12i 6871 |
. . . . . . 7
⊢
(1o ≠ ∅ → ((𝑓‘𝑛) = 1o → 𝑛𝑓1o)) |
10 | 1, 8, 9 | mpsyl 68 |
. . . . . 6
⊢ ((𝑓‘𝑛){⟨1o, 1o⟩}
(𝑓‘suc 𝑛) → 𝑛𝑓1o) |
11 | | vex 3450 |
. . . . . . 7
⊢ 𝑛 ∈ V |
12 | | 1oex 8423 |
. . . . . . 7
⊢
1o ∈ V |
13 | 11, 12 | breldm 5865 |
. . . . . 6
⊢ (𝑛𝑓1o → 𝑛 ∈ dom 𝑓) |
14 | 10, 13 | syl 17 |
. . . . 5
⊢ ((𝑓‘𝑛){⟨1o, 1o⟩}
(𝑓‘suc 𝑛) → 𝑛 ∈ dom 𝑓) |
15 | 14 | ralimi 3087 |
. . . 4
⊢
(∀𝑛 ∈
ω (𝑓‘𝑛){⟨1o,
1o⟩} (𝑓‘suc 𝑛) → ∀𝑛 ∈ ω 𝑛 ∈ dom 𝑓) |
16 | | dfss3 3933 |
. . . 4
⊢ (ω
⊆ dom 𝑓 ↔
∀𝑛 ∈ ω
𝑛 ∈ dom 𝑓) |
17 | 15, 16 | sylibr 233 |
. . 3
⊢
(∀𝑛 ∈
ω (𝑓‘𝑛){⟨1o,
1o⟩} (𝑓‘suc 𝑛) → ω ⊆ dom 𝑓) |
18 | | vex 3450 |
. . . . 5
⊢ 𝑓 ∈ V |
19 | 18 | dmex 7849 |
. . . 4
⊢ dom 𝑓 ∈ V |
20 | 19 | ssex 5279 |
. . 3
⊢ (ω
⊆ dom 𝑓 →
ω ∈ V) |
21 | 17, 20 | syl 17 |
. 2
⊢
(∀𝑛 ∈
ω (𝑓‘𝑛){⟨1o,
1o⟩} (𝑓‘suc 𝑛) → ω ∈ V) |
22 | | snex 5389 |
. . 3
⊢
{⟨1o, 1o⟩} ∈ V |
23 | 12, 12 | fvsn 7128 |
. . . . . . . 8
⊢
({⟨1o, 1o⟩}‘1o) =
1o |
24 | 12, 12 | funsn 6555 |
. . . . . . . . 9
⊢ Fun
{⟨1o, 1o⟩} |
25 | 12 | snid 4623 |
. . . . . . . . . 10
⊢
1o ∈ {1o} |
26 | 12 | dmsnop 6169 |
. . . . . . . . . 10
⊢ dom
{⟨1o, 1o⟩} = {1o} |
27 | 25, 26 | eleqtrri 2837 |
. . . . . . . . 9
⊢
1o ∈ dom {⟨1o,
1o⟩} |
28 | | funbrfvb 6898 |
. . . . . . . . 9
⊢ ((Fun
{⟨1o, 1o⟩} ∧ 1o ∈ dom
{⟨1o, 1o⟩}) → (({⟨1o,
1o⟩}‘1o) = 1o ↔
1o{⟨1o,
1o⟩}1o)) |
29 | 24, 27, 28 | mp2an 691 |
. . . . . . . 8
⊢
(({⟨1o, 1o⟩}‘1o) =
1o ↔ 1o{⟨1o,
1o⟩}1o) |
30 | 23, 29 | mpbi 229 |
. . . . . . 7
⊢
1o{⟨1o,
1o⟩}1o |
31 | | breq12 5111 |
. . . . . . . 8
⊢ ((𝑠 = 1o ∧ 𝑡 = 1o) → (𝑠{⟨1o,
1o⟩}𝑡
↔ 1o{⟨1o,
1o⟩}1o)) |
32 | 12, 12, 31 | spc2ev 3567 |
. . . . . . 7
⊢
(1o{⟨1o, 1o⟩}1o
→ ∃𝑠∃𝑡 𝑠{⟨1o,
1o⟩}𝑡) |
33 | 30, 32 | ax-mp 5 |
. . . . . 6
⊢
∃𝑠∃𝑡 𝑠{⟨1o,
1o⟩}𝑡 |
34 | | breq 5108 |
. . . . . . 7
⊢ (𝑥 = {⟨1o,
1o⟩} → (𝑠𝑥𝑡 ↔ 𝑠{⟨1o,
1o⟩}𝑡)) |
35 | 34 | 2exbidv 1928 |
. . . . . 6
⊢ (𝑥 = {⟨1o,
1o⟩} → (∃𝑠∃𝑡 𝑠𝑥𝑡 ↔ ∃𝑠∃𝑡 𝑠{⟨1o,
1o⟩}𝑡)) |
36 | 33, 35 | mpbiri 258 |
. . . . 5
⊢ (𝑥 = {⟨1o,
1o⟩} → ∃𝑠∃𝑡 𝑠𝑥𝑡) |
37 | | ssid 3967 |
. . . . . . 7
⊢
{1o} ⊆ {1o} |
38 | 12 | rnsnop 6177 |
. . . . . . 7
⊢ ran
{⟨1o, 1o⟩} = {1o} |
39 | 37, 38, 26 | 3sstr4i 3988 |
. . . . . 6
⊢ ran
{⟨1o, 1o⟩} ⊆ dom {⟨1o,
1o⟩} |
40 | | rneq 5892 |
. . . . . . 7
⊢ (𝑥 = {⟨1o,
1o⟩} → ran 𝑥 = ran {⟨1o,
1o⟩}) |
41 | | dmeq 5860 |
. . . . . . 7
⊢ (𝑥 = {⟨1o,
1o⟩} → dom 𝑥 = dom {⟨1o,
1o⟩}) |
42 | 40, 41 | sseq12d 3978 |
. . . . . 6
⊢ (𝑥 = {⟨1o,
1o⟩} → (ran 𝑥 ⊆ dom 𝑥 ↔ ran {⟨1o,
1o⟩} ⊆ dom {⟨1o,
1o⟩})) |
43 | 39, 42 | mpbiri 258 |
. . . . 5
⊢ (𝑥 = {⟨1o,
1o⟩} → ran 𝑥 ⊆ dom 𝑥) |
44 | | pm5.5 362 |
. . . . 5
⊢
((∃𝑠∃𝑡 𝑠𝑥𝑡 ∧ ran 𝑥 ⊆ dom 𝑥) → (((∃𝑠∃𝑡 𝑠𝑥𝑡 ∧ ran 𝑥 ⊆ dom 𝑥) → ∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛)) ↔ ∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛))) |
45 | 36, 43, 44 | syl2anc 585 |
. . . 4
⊢ (𝑥 = {⟨1o,
1o⟩} → (((∃𝑠∃𝑡 𝑠𝑥𝑡 ∧ ran 𝑥 ⊆ dom 𝑥) → ∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛)) ↔ ∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛))) |
46 | | breq 5108 |
. . . . . 6
⊢ (𝑥 = {⟨1o,
1o⟩} → ((𝑓‘𝑛)𝑥(𝑓‘suc 𝑛) ↔ (𝑓‘𝑛){⟨1o, 1o⟩}
(𝑓‘suc 𝑛))) |
47 | 46 | ralbidv 3175 |
. . . . 5
⊢ (𝑥 = {⟨1o,
1o⟩} → (∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛) ↔ ∀𝑛 ∈ ω (𝑓‘𝑛){⟨1o, 1o⟩}
(𝑓‘suc 𝑛))) |
48 | 47 | exbidv 1925 |
. . . 4
⊢ (𝑥 = {⟨1o,
1o⟩} → (∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛) ↔ ∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛){⟨1o, 1o⟩}
(𝑓‘suc 𝑛))) |
49 | 45, 48 | bitrd 279 |
. . 3
⊢ (𝑥 = {⟨1o,
1o⟩} → (((∃𝑠∃𝑡 𝑠𝑥𝑡 ∧ ran 𝑥 ⊆ dom 𝑥) → ∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛)) ↔ ∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛){⟨1o, 1o⟩}
(𝑓‘suc 𝑛))) |
50 | | ax-dc 10383 |
. . 3
⊢
((∃𝑠∃𝑡 𝑠𝑥𝑡 ∧ ran 𝑥 ⊆ dom 𝑥) → ∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛)) |
51 | 22, 49, 50 | vtocl 3519 |
. 2
⊢
∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛){⟨1o, 1o⟩}
(𝑓‘suc 𝑛) |
52 | 21, 51 | exlimiiv 1935 |
1
⊢ ω
∈ V |