Step | Hyp | Ref
| Expression |
1 | | 1n0 7732 |
. . . . . . 7
⊢
1𝑜 ≠ ∅ |
2 | | df-br 4788 |
. . . . . . . 8
⊢ ((𝑓‘𝑛){〈1𝑜,
1𝑜〉} (𝑓‘suc 𝑛) ↔ 〈(𝑓‘𝑛), (𝑓‘suc 𝑛)〉 ∈ {〈1𝑜,
1𝑜〉}) |
3 | | elsni 4334 |
. . . . . . . . 9
⊢
(〈(𝑓‘𝑛), (𝑓‘suc 𝑛)〉 ∈ {〈1𝑜,
1𝑜〉} → 〈(𝑓‘𝑛), (𝑓‘suc 𝑛)〉 = 〈1𝑜,
1𝑜〉) |
4 | | fvex 6344 |
. . . . . . . . . 10
⊢ (𝑓‘𝑛) ∈ V |
5 | | fvex 6344 |
. . . . . . . . . 10
⊢ (𝑓‘suc 𝑛) ∈ V |
6 | 4, 5 | opth1 5072 |
. . . . . . . . 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 6357 |
. . . . . . 7
⊢
(1𝑜 ≠ ∅ → ((𝑓‘𝑛) = 1𝑜 → 𝑛𝑓1𝑜)) |
10 | 1, 8, 9 | mpsyl 68 |
. . . . . 6
⊢ ((𝑓‘𝑛){〈1𝑜,
1𝑜〉} (𝑓‘suc 𝑛) → 𝑛𝑓1𝑜) |
11 | | vex 3354 |
. . . . . . 7
⊢ 𝑛 ∈ V |
12 | | 1oex 7724 |
. . . . . . 7
⊢
1𝑜 ∈ V |
13 | 11, 12 | breldm 5466 |
. . . . . 6
⊢ (𝑛𝑓1𝑜 → 𝑛 ∈ dom 𝑓) |
14 | 10, 13 | syl 17 |
. . . . 5
⊢ ((𝑓‘𝑛){〈1𝑜,
1𝑜〉} (𝑓‘suc 𝑛) → 𝑛 ∈ dom 𝑓) |
15 | 14 | ralimi 3101 |
. . . 4
⊢
(∀𝑛 ∈
ω (𝑓‘𝑛){〈1𝑜,
1𝑜〉} (𝑓‘suc 𝑛) → ∀𝑛 ∈ ω 𝑛 ∈ dom 𝑓) |
16 | | dfss3 3741 |
. . . 4
⊢ (ω
⊆ dom 𝑓 ↔
∀𝑛 ∈ ω
𝑛 ∈ dom 𝑓) |
17 | 15, 16 | sylibr 224 |
. . 3
⊢
(∀𝑛 ∈
ω (𝑓‘𝑛){〈1𝑜,
1𝑜〉} (𝑓‘suc 𝑛) → ω ⊆ dom 𝑓) |
18 | | vex 3354 |
. . . . 5
⊢ 𝑓 ∈ V |
19 | 18 | dmex 7249 |
. . . 4
⊢ dom 𝑓 ∈ V |
20 | 19 | ssex 4937 |
. . 3
⊢ (ω
⊆ dom 𝑓 →
ω ∈ V) |
21 | 17, 20 | syl 17 |
. 2
⊢
(∀𝑛 ∈
ω (𝑓‘𝑛){〈1𝑜,
1𝑜〉} (𝑓‘suc 𝑛) → ω ∈ V) |
22 | | snex 5037 |
. . 3
⊢
{〈1𝑜, 1𝑜〉} ∈
V |
23 | 12, 12 | fvsn 6592 |
. . . . . . . 8
⊢
({〈1𝑜,
1𝑜〉}‘1𝑜) =
1𝑜 |
24 | 12, 12 | funsn 6081 |
. . . . . . . . 9
⊢ Fun
{〈1𝑜, 1𝑜〉} |
25 | 12 | snid 4348 |
. . . . . . . . . 10
⊢
1𝑜 ∈ {1𝑜} |
26 | 12 | dmsnop 5750 |
. . . . . . . . . 10
⊢ dom
{〈1𝑜, 1𝑜〉} =
{1𝑜} |
27 | 25, 26 | eleqtrri 2849 |
. . . . . . . . 9
⊢
1𝑜 ∈ dom {〈1𝑜,
1𝑜〉} |
28 | | funbrfvb 6381 |
. . . . . . . . 9
⊢ ((Fun
{〈1𝑜, 1𝑜〉} ∧
1𝑜 ∈ dom {〈1𝑜,
1𝑜〉}) → (({〈1𝑜,
1𝑜〉}‘1𝑜) =
1𝑜 ↔ 1𝑜{〈1𝑜,
1𝑜〉}1𝑜)) |
29 | 24, 27, 28 | mp2an 672 |
. . . . . . . 8
⊢
(({〈1𝑜,
1𝑜〉}‘1𝑜) =
1𝑜 ↔ 1𝑜{〈1𝑜,
1𝑜〉}1𝑜) |
30 | 23, 29 | mpbi 220 |
. . . . . . 7
⊢
1𝑜{〈1𝑜,
1𝑜〉}1𝑜 |
31 | | breq12 4792 |
. . . . . . . 8
⊢ ((𝑠 = 1𝑜 ∧
𝑡 = 1𝑜)
→ (𝑠{〈1𝑜,
1𝑜〉}𝑡 ↔
1𝑜{〈1𝑜,
1𝑜〉}1𝑜)) |
32 | 12, 12, 31 | spc2ev 3452 |
. . . . . . 7
⊢
(1𝑜{〈1𝑜,
1𝑜〉}1𝑜 → ∃𝑠∃𝑡 𝑠{〈1𝑜,
1𝑜〉}𝑡) |
33 | 30, 32 | ax-mp 5 |
. . . . . 6
⊢
∃𝑠∃𝑡 𝑠{〈1𝑜,
1𝑜〉}𝑡 |
34 | | breq 4789 |
. . . . . . 7
⊢ (𝑥 = {〈1𝑜,
1𝑜〉} → (𝑠𝑥𝑡 ↔ 𝑠{〈1𝑜,
1𝑜〉}𝑡)) |
35 | 34 | 2exbidv 2004 |
. . . . . 6
⊢ (𝑥 = {〈1𝑜,
1𝑜〉} → (∃𝑠∃𝑡 𝑠𝑥𝑡 ↔ ∃𝑠∃𝑡 𝑠{〈1𝑜,
1𝑜〉}𝑡)) |
36 | 33, 35 | mpbiri 248 |
. . . . 5
⊢ (𝑥 = {〈1𝑜,
1𝑜〉} → ∃𝑠∃𝑡 𝑠𝑥𝑡) |
37 | | ssid 3773 |
. . . . . . 7
⊢
{1𝑜} ⊆ {1𝑜} |
38 | 12 | rnsnop 5758 |
. . . . . . 7
⊢ ran
{〈1𝑜, 1𝑜〉} =
{1𝑜} |
39 | 37, 38, 26 | 3sstr4i 3793 |
. . . . . 6
⊢ ran
{〈1𝑜, 1𝑜〉} ⊆ dom
{〈1𝑜, 1𝑜〉} |
40 | | rneq 5488 |
. . . . . . 7
⊢ (𝑥 = {〈1𝑜,
1𝑜〉} → ran 𝑥 = ran {〈1𝑜,
1𝑜〉}) |
41 | | dmeq 5461 |
. . . . . . 7
⊢ (𝑥 = {〈1𝑜,
1𝑜〉} → dom 𝑥 = dom {〈1𝑜,
1𝑜〉}) |
42 | 40, 41 | sseq12d 3783 |
. . . . . 6
⊢ (𝑥 = {〈1𝑜,
1𝑜〉} → (ran 𝑥 ⊆ dom 𝑥 ↔ ran {〈1𝑜,
1𝑜〉} ⊆ dom {〈1𝑜,
1𝑜〉})) |
43 | 39, 42 | mpbiri 248 |
. . . . 5
⊢ (𝑥 = {〈1𝑜,
1𝑜〉} → ran 𝑥 ⊆ dom 𝑥) |
44 | | pm5.5 350 |
. . . . 5
⊢
((∃𝑠∃𝑡 𝑠𝑥𝑡 ∧ ran 𝑥 ⊆ dom 𝑥) → (((∃𝑠∃𝑡 𝑠𝑥𝑡 ∧ ran 𝑥 ⊆ dom 𝑥) → ∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛)) ↔ ∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛))) |
45 | 36, 43, 44 | syl2anc 573 |
. . . 4
⊢ (𝑥 = {〈1𝑜,
1𝑜〉} → (((∃𝑠∃𝑡 𝑠𝑥𝑡 ∧ ran 𝑥 ⊆ dom 𝑥) → ∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛)) ↔ ∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛))) |
46 | | breq 4789 |
. . . . . 6
⊢ (𝑥 = {〈1𝑜,
1𝑜〉} → ((𝑓‘𝑛)𝑥(𝑓‘suc 𝑛) ↔ (𝑓‘𝑛){〈1𝑜,
1𝑜〉} (𝑓‘suc 𝑛))) |
47 | 46 | ralbidv 3135 |
. . . . 5
⊢ (𝑥 = {〈1𝑜,
1𝑜〉} → (∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛) ↔ ∀𝑛 ∈ ω (𝑓‘𝑛){〈1𝑜,
1𝑜〉} (𝑓‘suc 𝑛))) |
48 | 47 | exbidv 2002 |
. . . 4
⊢ (𝑥 = {〈1𝑜,
1𝑜〉} → (∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛) ↔ ∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛){〈1𝑜,
1𝑜〉} (𝑓‘suc 𝑛))) |
49 | 45, 48 | bitrd 268 |
. . 3
⊢ (𝑥 = {〈1𝑜,
1𝑜〉} → (((∃𝑠∃𝑡 𝑠𝑥𝑡 ∧ ran 𝑥 ⊆ dom 𝑥) → ∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛)) ↔ ∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛){〈1𝑜,
1𝑜〉} (𝑓‘suc 𝑛))) |
50 | | ax-dc 9473 |
. . 3
⊢
((∃𝑠∃𝑡 𝑠𝑥𝑡 ∧ ran 𝑥 ⊆ dom 𝑥) → ∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛)𝑥(𝑓‘suc 𝑛)) |
51 | 22, 49, 50 | vtocl 3410 |
. 2
⊢
∃𝑓∀𝑛 ∈ ω (𝑓‘𝑛){〈1𝑜,
1𝑜〉} (𝑓‘suc 𝑛) |
52 | 21, 51 | exlimiiv 2011 |
1
⊢ ω
∈ V |