| Step | Hyp | Ref
| Expression |
| 1 | | 1n0 8526 |
. . . . . . 7
⊢
1o ≠ ∅ |
| 2 | | df-br 5144 |
. . . . . . . 8
⊢ ((𝑓‘𝑛){〈1o, 1o〉}
(𝑓‘suc 𝑛) ↔ 〈(𝑓‘𝑛), (𝑓‘suc 𝑛)〉 ∈ {〈1o,
1o〉}) |
| 3 | | elsni 4643 |
. . . . . . . . 9
⊢
(〈(𝑓‘𝑛), (𝑓‘suc 𝑛)〉 ∈ {〈1o,
1o〉} → 〈(𝑓‘𝑛), (𝑓‘suc 𝑛)〉 = 〈1o,
1o〉) |
| 4 | | fvex 6919 |
. . . . . . . . . 10
⊢ (𝑓‘𝑛) ∈ V |
| 5 | | fvex 6919 |
. . . . . . . . . 10
⊢ (𝑓‘suc 𝑛) ∈ V |
| 6 | 4, 5 | opth1 5480 |
. . . . . . . . 9
⊢
(〈(𝑓‘𝑛), (𝑓‘suc 𝑛)〉 = 〈1o,
1o〉 → (𝑓‘𝑛) = 1o) |
| 7 | 3, 6 | syl 17 |
. . . . . . . 8
⊢
(〈(𝑓‘𝑛), (𝑓‘suc 𝑛)〉 ∈ {〈1o,
1o〉} → (𝑓‘𝑛) = 1o) |
| 8 | 2, 7 | sylbi 217 |
. . . . . . 7
⊢ ((𝑓‘𝑛){〈1o, 1o〉}
(𝑓‘suc 𝑛) → (𝑓‘𝑛) = 1o) |
| 9 | | tz6.12i 6934 |
. . . . . . 7
⊢
(1o ≠ ∅ → ((𝑓‘𝑛) = 1o → 𝑛𝑓1o)) |
| 10 | 1, 8, 9 | mpsyl 68 |
. . . . . 6
⊢ ((𝑓‘𝑛){〈1o, 1o〉}
(𝑓‘suc 𝑛) → 𝑛𝑓1o) |
| 11 | | vex 3484 |
. . . . . . 7
⊢ 𝑛 ∈ V |
| 12 | | 1oex 8516 |
. . . . . . 7
⊢
1o ∈ V |
| 13 | 11, 12 | breldm 5919 |
. . . . . 6
⊢ (𝑛𝑓1o → 𝑛 ∈ dom 𝑓) |
| 14 | 10, 13 | syl 17 |
. . . . 5
⊢ ((𝑓‘𝑛){〈1o, 1o〉}
(𝑓‘suc 𝑛) → 𝑛 ∈ dom 𝑓) |
| 15 | 14 | ralimi 3083 |
. . . 4
⊢
(∀𝑛 ∈
ω (𝑓‘𝑛){〈1o,
1o〉} (𝑓‘suc 𝑛) → ∀𝑛 ∈ ω 𝑛 ∈ dom 𝑓) |
| 16 | | dfss3 3972 |
. . . 4
⊢ (ω
⊆ dom 𝑓 ↔
∀𝑛 ∈ ω
𝑛 ∈ dom 𝑓) |
| 17 | 15, 16 | sylibr 234 |
. . 3
⊢
(∀𝑛 ∈
ω (𝑓‘𝑛){〈1o,
1o〉} (𝑓‘suc 𝑛) → ω ⊆ dom 𝑓) |
| 18 | | vex 3484 |
. . . . 5
⊢ 𝑓 ∈ V |
| 19 | 18 | dmex 7931 |
. . . 4
⊢ dom 𝑓 ∈ V |
| 20 | 19 | ssex 5321 |
. . 3
⊢ (ω
⊆ dom 𝑓 →
ω ∈ V) |
| 21 | 17, 20 | syl 17 |
. 2
⊢
(∀𝑛 ∈
ω (𝑓‘𝑛){〈1o,
1o〉} (𝑓‘suc 𝑛) → ω ∈ V) |
| 22 | | snex 5436 |
. . 3
⊢
{〈1o, 1o〉} ∈ V |
| 23 | 12, 12 | fvsn 7201 |
. . . . . . . 8
⊢
({〈1o, 1o〉}‘1o) =
1o |
| 24 | 12, 12 | funsn 6619 |
. . . . . . . . 9
⊢ Fun
{〈1o, 1o〉} |
| 25 | 12 | snid 4662 |
. . . . . . . . . 10
⊢
1o ∈ {1o} |
| 26 | 12 | dmsnop 6236 |
. . . . . . . . . 10
⊢ dom
{〈1o, 1o〉} = {1o} |
| 27 | 25, 26 | eleqtrri 2840 |
. . . . . . . . 9
⊢
1o ∈ dom {〈1o,
1o〉} |
| 28 | | funbrfvb 6962 |
. . . . . . . . 9
⊢ ((Fun
{〈1o, 1o〉} ∧ 1o ∈ dom
{〈1o, 1o〉}) → (({〈1o,
1o〉}‘1o) = 1o ↔
1o{〈1o,
1o〉}1o)) |
| 29 | 24, 27, 28 | mp2an 692 |
. . . . . . . 8
⊢
(({〈1o, 1o〉}‘1o) =
1o ↔ 1o{〈1o,
1o〉}1o) |
| 30 | 23, 29 | mpbi 230 |
. . . . . . 7
⊢
1o{〈1o,
1o〉}1o |
| 31 | | breq12 5148 |
. . . . . . . 8
⊢ ((𝑠 = 1o ∧ 𝑡 = 1o) → (𝑠{〈1o,
1o〉}𝑡
↔ 1o{〈1o,
1o〉}1o)) |
| 32 | 12, 12, 31 | spc2ev 3607 |
. . . . . . 7
⊢
(1o{〈1o, 1o〉}1o
→ ∃𝑠∃𝑡 𝑠{〈1o,
1o〉}𝑡) |
| 33 | 30, 32 | ax-mp 5 |
. . . . . 6
⊢
∃𝑠∃𝑡 𝑠{〈1o,
1o〉}𝑡 |
| 34 | | breq 5145 |
. . . . . . 7
⊢ (𝑥 = {〈1o,
1o〉} → (𝑠𝑥𝑡 ↔ 𝑠{〈1o,
1o〉}𝑡)) |
| 35 | 34 | 2exbidv 1924 |
. . . . . 6
⊢ (𝑥 = {〈1o,
1o〉} → (∃𝑠∃𝑡 𝑠𝑥𝑡 ↔ ∃𝑠∃𝑡 𝑠{〈1o,
1o〉}𝑡)) |
| 36 | 33, 35 | mpbiri 258 |
. . . . 5
⊢ (𝑥 = {〈1o,
1o〉} → ∃𝑠∃𝑡 𝑠𝑥𝑡) |
| 37 | | ssid 4006 |
. . . . . . 7
⊢
{1o} ⊆ {1o} |
| 38 | 12 | rnsnop 6244 |
. . . . . . 7
⊢ ran
{〈1o, 1o〉} = {1o} |
| 39 | 37, 38, 26 | 3sstr4i 4035 |
. . . . . 6
⊢ ran
{〈1o, 1o〉} ⊆ dom {〈1o,
1o〉} |
| 40 | | rneq 5947 |
. . . . . . 7
⊢ (𝑥 = {〈1o,
1o〉} → ran 𝑥 = ran {〈1o,
1o〉}) |
| 41 | | dmeq 5914 |
. . . . . . 7
⊢ (𝑥 = {〈1o,
1o〉} → dom 𝑥 = dom {〈1o,
1o〉}) |
| 42 | 40, 41 | sseq12d 4017 |
. . . . . 6
⊢ (𝑥 = {〈1o,
1o〉} → (ran 𝑥 ⊆ dom 𝑥 ↔ ran {〈1o,
1o〉} ⊆ dom {〈1o,
1o〉})) |
| 43 | 39, 42 | mpbiri 258 |
. . . . 5
⊢ (𝑥 = {〈1o,
1o〉} → ran 𝑥 ⊆ dom 𝑥) |
| 44 | | pm5.5 361 |
. . . . 5
⊢
((∃𝑠∃𝑡 𝑠𝑥𝑡 ∧ ran 𝑥 ⊆ dom 𝑥) → (((∃𝑠∃𝑡 𝑠𝑥𝑡 ∧ ran 𝑥 ⊆ dom 𝑥) → ∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛)) ↔ ∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛))) |
| 45 | 36, 43, 44 | syl2anc 584 |
. . . 4
⊢ (𝑥 = {〈1o,
1o〉} → (((∃𝑠∃𝑡 𝑠𝑥𝑡 ∧ ran 𝑥 ⊆ dom 𝑥) → ∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛)) ↔ ∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛))) |
| 46 | | breq 5145 |
. . . . . 6
⊢ (𝑥 = {〈1o,
1o〉} → ((𝑓‘𝑛)𝑥(𝑓‘suc 𝑛) ↔ (𝑓‘𝑛){〈1o, 1o〉}
(𝑓‘suc 𝑛))) |
| 47 | 46 | ralbidv 3178 |
. . . . 5
⊢ (𝑥 = {〈1o,
1o〉} → (∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛) ↔ ∀𝑛 ∈ ω (𝑓‘𝑛){〈1o, 1o〉}
(𝑓‘suc 𝑛))) |
| 48 | 47 | exbidv 1921 |
. . . 4
⊢ (𝑥 = {〈1o,
1o〉} → (∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛) ↔ ∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛){〈1o, 1o〉}
(𝑓‘suc 𝑛))) |
| 49 | 45, 48 | bitrd 279 |
. . 3
⊢ (𝑥 = {〈1o,
1o〉} → (((∃𝑠∃𝑡 𝑠𝑥𝑡 ∧ ran 𝑥 ⊆ dom 𝑥) → ∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛)) ↔ ∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛){〈1o, 1o〉}
(𝑓‘suc 𝑛))) |
| 50 | | ax-dc 10486 |
. . 3
⊢
((∃𝑠∃𝑡 𝑠𝑥𝑡 ∧ ran 𝑥 ⊆ dom 𝑥) → ∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛)) |
| 51 | 22, 49, 50 | vtocl 3558 |
. 2
⊢
∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛){〈1o, 1o〉}
(𝑓‘suc 𝑛) |
| 52 | 21, 51 | exlimiiv 1931 |
1
⊢ ω
∈ V |