Step | Hyp | Ref
| Expression |
1 | | peano2 7621 |
. . . . 5
⊢ (𝑁 ∈ ω → suc 𝑁 ∈
ω) |
2 | | ovexd 7205 |
. . . . 5
⊢ (𝑁 ∈ ω → (𝑎⊼𝑔𝑏) ∈ V) |
3 | | isfmlasuc 32921 |
. . . . 5
⊢ ((suc
𝑁 ∈ ω ∧
(𝑎⊼𝑔𝑏) ∈ V) → ((𝑎⊼𝑔𝑏) ∈ (Fmla‘suc suc 𝑁) ↔ ((𝑎⊼𝑔𝑏) ∈ (Fmla‘suc 𝑁) ∨ ∃𝑢 ∈ (Fmla‘suc 𝑁)(∃𝑣 ∈ (Fmla‘suc 𝑁)(𝑎⊼𝑔𝑏) = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω (𝑎⊼𝑔𝑏) = ∀𝑔𝑖𝑢)))) |
4 | 1, 2, 3 | syl2anc 587 |
. . . 4
⊢ (𝑁 ∈ ω → ((𝑎⊼𝑔𝑏) ∈ (Fmla‘suc suc
𝑁) ↔ ((𝑎⊼𝑔𝑏) ∈ (Fmla‘suc 𝑁) ∨ ∃𝑢 ∈ (Fmla‘suc 𝑁)(∃𝑣 ∈ (Fmla‘suc 𝑁)(𝑎⊼𝑔𝑏) = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω (𝑎⊼𝑔𝑏) = ∀𝑔𝑖𝑢)))) |
5 | 4 | adantr 484 |
. . 3
⊢ ((𝑁 ∈ ω ∧ ((𝑎⊼𝑔𝑏) ∈ (Fmla‘suc 𝑁) → (𝑎 ∈ (Fmla‘suc 𝑁) ∧ 𝑏 ∈ (Fmla‘suc 𝑁)))) → ((𝑎⊼𝑔𝑏) ∈ (Fmla‘suc suc 𝑁) ↔ ((𝑎⊼𝑔𝑏) ∈ (Fmla‘suc 𝑁) ∨ ∃𝑢 ∈ (Fmla‘suc 𝑁)(∃𝑣 ∈ (Fmla‘suc 𝑁)(𝑎⊼𝑔𝑏) = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω (𝑎⊼𝑔𝑏) = ∀𝑔𝑖𝑢)))) |
6 | | fmlasssuc 32922 |
. . . . . . . . . . 11
⊢ (suc
𝑁 ∈ ω →
(Fmla‘suc 𝑁) ⊆
(Fmla‘suc suc 𝑁)) |
7 | 1, 6 | syl 17 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ω →
(Fmla‘suc 𝑁) ⊆
(Fmla‘suc suc 𝑁)) |
8 | 7 | sseld 3876 |
. . . . . . . . 9
⊢ (𝑁 ∈ ω → (𝑎 ∈ (Fmla‘suc 𝑁) → 𝑎 ∈ (Fmla‘suc suc 𝑁))) |
9 | 7 | sseld 3876 |
. . . . . . . . 9
⊢ (𝑁 ∈ ω → (𝑏 ∈ (Fmla‘suc 𝑁) → 𝑏 ∈ (Fmla‘suc suc 𝑁))) |
10 | 8, 9 | anim12d 612 |
. . . . . . . 8
⊢ (𝑁 ∈ ω → ((𝑎 ∈ (Fmla‘suc 𝑁) ∧ 𝑏 ∈ (Fmla‘suc 𝑁)) → (𝑎 ∈ (Fmla‘suc suc 𝑁) ∧ 𝑏 ∈ (Fmla‘suc suc 𝑁)))) |
11 | 10 | com12 32 |
. . . . . . 7
⊢ ((𝑎 ∈ (Fmla‘suc 𝑁) ∧ 𝑏 ∈ (Fmla‘suc 𝑁)) → (𝑁 ∈ ω → (𝑎 ∈ (Fmla‘suc suc 𝑁) ∧ 𝑏 ∈ (Fmla‘suc suc 𝑁)))) |
12 | 11 | imim2i 16 |
. . . . . 6
⊢ (((𝑎⊼𝑔𝑏) ∈ (Fmla‘suc 𝑁) → (𝑎 ∈ (Fmla‘suc 𝑁) ∧ 𝑏 ∈ (Fmla‘suc 𝑁))) → ((𝑎⊼𝑔𝑏) ∈ (Fmla‘suc 𝑁) → (𝑁 ∈ ω → (𝑎 ∈ (Fmla‘suc suc 𝑁) ∧ 𝑏 ∈ (Fmla‘suc suc 𝑁))))) |
13 | 12 | com23 86 |
. . . . 5
⊢ (((𝑎⊼𝑔𝑏) ∈ (Fmla‘suc 𝑁) → (𝑎 ∈ (Fmla‘suc 𝑁) ∧ 𝑏 ∈ (Fmla‘suc 𝑁))) → (𝑁 ∈ ω → ((𝑎⊼𝑔𝑏) ∈ (Fmla‘suc 𝑁) → (𝑎 ∈ (Fmla‘suc suc 𝑁) ∧ 𝑏 ∈ (Fmla‘suc suc 𝑁))))) |
14 | 13 | impcom 411 |
. . . 4
⊢ ((𝑁 ∈ ω ∧ ((𝑎⊼𝑔𝑏) ∈ (Fmla‘suc 𝑁) → (𝑎 ∈ (Fmla‘suc 𝑁) ∧ 𝑏 ∈ (Fmla‘suc 𝑁)))) → ((𝑎⊼𝑔𝑏) ∈ (Fmla‘suc 𝑁) → (𝑎 ∈ (Fmla‘suc suc 𝑁) ∧ 𝑏 ∈ (Fmla‘suc suc 𝑁)))) |
15 | | gonafv 32883 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ V ∧ 𝑏 ∈ V) → (𝑎⊼𝑔𝑏) = 〈1o,
〈𝑎, 𝑏〉〉) |
16 | 15 | el2v 3406 |
. . . . . . . . . . . . 13
⊢ (𝑎⊼𝑔𝑏) = 〈1o,
〈𝑎, 𝑏〉〉 |
17 | 16 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑢 ∈ (Fmla‘suc 𝑁) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)) → (𝑎⊼𝑔𝑏) = 〈1o, 〈𝑎, 𝑏〉〉) |
18 | | gonafv 32883 |
. . . . . . . . . . . 12
⊢ ((𝑢 ∈ (Fmla‘suc 𝑁) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)) → (𝑢⊼𝑔𝑣) = 〈1o, 〈𝑢, 𝑣〉〉) |
19 | 17, 18 | eqeq12d 2754 |
. . . . . . . . . . 11
⊢ ((𝑢 ∈ (Fmla‘suc 𝑁) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)) → ((𝑎⊼𝑔𝑏) = (𝑢⊼𝑔𝑣) ↔ 〈1o, 〈𝑎, 𝑏〉〉 = 〈1o,
〈𝑢, 𝑣〉〉)) |
20 | | 1oex 8144 |
. . . . . . . . . . . 12
⊢
1o ∈ V |
21 | | opex 5322 |
. . . . . . . . . . . 12
⊢
〈𝑎, 𝑏〉 ∈ V |
22 | 20, 21 | opth 5334 |
. . . . . . . . . . 11
⊢
(〈1o, 〈𝑎, 𝑏〉〉 = 〈1o,
〈𝑢, 𝑣〉〉 ↔ (1o =
1o ∧ 〈𝑎, 𝑏〉 = 〈𝑢, 𝑣〉)) |
23 | 19, 22 | bitrdi 290 |
. . . . . . . . . 10
⊢ ((𝑢 ∈ (Fmla‘suc 𝑁) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)) → ((𝑎⊼𝑔𝑏) = (𝑢⊼𝑔𝑣) ↔ (1o = 1o ∧
〈𝑎, 𝑏〉 = 〈𝑢, 𝑣〉))) |
24 | 23 | adantll 714 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘suc 𝑁)) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)) → ((𝑎⊼𝑔𝑏) = (𝑢⊼𝑔𝑣) ↔ (1o = 1o ∧
〈𝑎, 𝑏〉 = 〈𝑢, 𝑣〉))) |
25 | | vex 3402 |
. . . . . . . . . . . . . 14
⊢ 𝑎 ∈ V |
26 | | vex 3402 |
. . . . . . . . . . . . . 14
⊢ 𝑏 ∈ V |
27 | 25, 26 | opth 5334 |
. . . . . . . . . . . . 13
⊢
(〈𝑎, 𝑏〉 = 〈𝑢, 𝑣〉 ↔ (𝑎 = 𝑢 ∧ 𝑏 = 𝑣)) |
28 | | eleq1w 2815 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 = 𝑎 → (𝑢 ∈ (Fmla‘suc 𝑁) ↔ 𝑎 ∈ (Fmla‘suc 𝑁))) |
29 | 28 | equcoms 2032 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑢 → (𝑢 ∈ (Fmla‘suc 𝑁) ↔ 𝑎 ∈ (Fmla‘suc 𝑁))) |
30 | | eleq1w 2815 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 = 𝑏 → (𝑣 ∈ (Fmla‘suc 𝑁) ↔ 𝑏 ∈ (Fmla‘suc 𝑁))) |
31 | 30 | equcoms 2032 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = 𝑣 → (𝑣 ∈ (Fmla‘suc 𝑁) ↔ 𝑏 ∈ (Fmla‘suc 𝑁))) |
32 | 29, 31 | bi2anan9 639 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → ((𝑢 ∈ (Fmla‘suc 𝑁) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)) ↔ (𝑎 ∈ (Fmla‘suc 𝑁) ∧ 𝑏 ∈ (Fmla‘suc 𝑁)))) |
33 | 32, 11 | syl6bi 256 |
. . . . . . . . . . . . 13
⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → ((𝑢 ∈ (Fmla‘suc 𝑁) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)) → (𝑁 ∈ ω → (𝑎 ∈ (Fmla‘suc suc 𝑁) ∧ 𝑏 ∈ (Fmla‘suc suc 𝑁))))) |
34 | 27, 33 | sylbi 220 |
. . . . . . . . . . . 12
⊢
(〈𝑎, 𝑏〉 = 〈𝑢, 𝑣〉 → ((𝑢 ∈ (Fmla‘suc 𝑁) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)) → (𝑁 ∈ ω → (𝑎 ∈ (Fmla‘suc suc 𝑁) ∧ 𝑏 ∈ (Fmla‘suc suc 𝑁))))) |
35 | 34 | adantl 485 |
. . . . . . . . . . 11
⊢
((1o = 1o ∧ 〈𝑎, 𝑏〉 = 〈𝑢, 𝑣〉) → ((𝑢 ∈ (Fmla‘suc 𝑁) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)) → (𝑁 ∈ ω → (𝑎 ∈ (Fmla‘suc suc 𝑁) ∧ 𝑏 ∈ (Fmla‘suc suc 𝑁))))) |
36 | 35 | com13 88 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ω → ((𝑢 ∈ (Fmla‘suc 𝑁) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)) → ((1o = 1o
∧ 〈𝑎, 𝑏〉 = 〈𝑢, 𝑣〉) → (𝑎 ∈ (Fmla‘suc suc 𝑁) ∧ 𝑏 ∈ (Fmla‘suc suc 𝑁))))) |
37 | 36 | impl 459 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘suc 𝑁)) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)) → ((1o = 1o
∧ 〈𝑎, 𝑏〉 = 〈𝑢, 𝑣〉) → (𝑎 ∈ (Fmla‘suc suc 𝑁) ∧ 𝑏 ∈ (Fmla‘suc suc 𝑁)))) |
38 | 24, 37 | sylbid 243 |
. . . . . . . 8
⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘suc 𝑁)) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)) → ((𝑎⊼𝑔𝑏) = (𝑢⊼𝑔𝑣) → (𝑎 ∈ (Fmla‘suc suc 𝑁) ∧ 𝑏 ∈ (Fmla‘suc suc 𝑁)))) |
39 | 38 | rexlimdva 3194 |
. . . . . . 7
⊢ ((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘suc 𝑁)) → (∃𝑣 ∈ (Fmla‘suc 𝑁)(𝑎⊼𝑔𝑏) = (𝑢⊼𝑔𝑣) → (𝑎 ∈ (Fmla‘suc suc 𝑁) ∧ 𝑏 ∈ (Fmla‘suc suc 𝑁)))) |
40 | | gonanegoal 32885 |
. . . . . . . . . 10
⊢ (𝑎⊼𝑔𝑏) ≠
∀𝑔𝑖𝑢 |
41 | | eqneqall 2945 |
. . . . . . . . . 10
⊢ ((𝑎⊼𝑔𝑏) =
∀𝑔𝑖𝑢 → ((𝑎⊼𝑔𝑏) ≠ ∀𝑔𝑖𝑢 → (𝑎 ∈ (Fmla‘suc suc 𝑁) ∧ 𝑏 ∈ (Fmla‘suc suc 𝑁)))) |
42 | 40, 41 | mpi 20 |
. . . . . . . . 9
⊢ ((𝑎⊼𝑔𝑏) =
∀𝑔𝑖𝑢 → (𝑎 ∈ (Fmla‘suc suc 𝑁) ∧ 𝑏 ∈ (Fmla‘suc suc 𝑁))) |
43 | 42 | a1i 11 |
. . . . . . . 8
⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘suc 𝑁)) ∧ 𝑖 ∈ ω) → ((𝑎⊼𝑔𝑏) = ∀𝑔𝑖𝑢 → (𝑎 ∈ (Fmla‘suc suc 𝑁) ∧ 𝑏 ∈ (Fmla‘suc suc 𝑁)))) |
44 | 43 | rexlimdva 3194 |
. . . . . . 7
⊢ ((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘suc 𝑁)) → (∃𝑖 ∈ ω (𝑎⊼𝑔𝑏) =
∀𝑔𝑖𝑢 → (𝑎 ∈ (Fmla‘suc suc 𝑁) ∧ 𝑏 ∈ (Fmla‘suc suc 𝑁)))) |
45 | 39, 44 | jaod 858 |
. . . . . 6
⊢ ((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘suc 𝑁)) → ((∃𝑣 ∈ (Fmla‘suc 𝑁)(𝑎⊼𝑔𝑏) = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω (𝑎⊼𝑔𝑏) = ∀𝑔𝑖𝑢) → (𝑎 ∈ (Fmla‘suc suc 𝑁) ∧ 𝑏 ∈ (Fmla‘suc suc 𝑁)))) |
46 | 45 | rexlimdva 3194 |
. . . . 5
⊢ (𝑁 ∈ ω →
(∃𝑢 ∈
(Fmla‘suc 𝑁)(∃𝑣 ∈ (Fmla‘suc 𝑁)(𝑎⊼𝑔𝑏) = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω (𝑎⊼𝑔𝑏) = ∀𝑔𝑖𝑢) → (𝑎 ∈ (Fmla‘suc suc 𝑁) ∧ 𝑏 ∈ (Fmla‘suc suc 𝑁)))) |
47 | 46 | adantr 484 |
. . . 4
⊢ ((𝑁 ∈ ω ∧ ((𝑎⊼𝑔𝑏) ∈ (Fmla‘suc 𝑁) → (𝑎 ∈ (Fmla‘suc 𝑁) ∧ 𝑏 ∈ (Fmla‘suc 𝑁)))) → (∃𝑢 ∈ (Fmla‘suc 𝑁)(∃𝑣 ∈ (Fmla‘suc 𝑁)(𝑎⊼𝑔𝑏) = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω (𝑎⊼𝑔𝑏) = ∀𝑔𝑖𝑢) → (𝑎 ∈ (Fmla‘suc suc 𝑁) ∧ 𝑏 ∈ (Fmla‘suc suc 𝑁)))) |
48 | 14, 47 | jaod 858 |
. . 3
⊢ ((𝑁 ∈ ω ∧ ((𝑎⊼𝑔𝑏) ∈ (Fmla‘suc 𝑁) → (𝑎 ∈ (Fmla‘suc 𝑁) ∧ 𝑏 ∈ (Fmla‘suc 𝑁)))) → (((𝑎⊼𝑔𝑏) ∈ (Fmla‘suc 𝑁) ∨ ∃𝑢 ∈ (Fmla‘suc 𝑁)(∃𝑣 ∈ (Fmla‘suc 𝑁)(𝑎⊼𝑔𝑏) = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω (𝑎⊼𝑔𝑏) = ∀𝑔𝑖𝑢)) → (𝑎 ∈ (Fmla‘suc suc 𝑁) ∧ 𝑏 ∈ (Fmla‘suc suc 𝑁)))) |
49 | 5, 48 | sylbid 243 |
. 2
⊢ ((𝑁 ∈ ω ∧ ((𝑎⊼𝑔𝑏) ∈ (Fmla‘suc 𝑁) → (𝑎 ∈ (Fmla‘suc 𝑁) ∧ 𝑏 ∈ (Fmla‘suc 𝑁)))) → ((𝑎⊼𝑔𝑏) ∈ (Fmla‘suc suc 𝑁) → (𝑎 ∈ (Fmla‘suc suc 𝑁) ∧ 𝑏 ∈ (Fmla‘suc suc 𝑁)))) |
50 | 49 | ex 416 |
1
⊢ (𝑁 ∈ ω → (((𝑎⊼𝑔𝑏) ∈ (Fmla‘suc 𝑁) → (𝑎 ∈ (Fmla‘suc 𝑁) ∧ 𝑏 ∈ (Fmla‘suc 𝑁))) → ((𝑎⊼𝑔𝑏) ∈ (Fmla‘suc suc 𝑁) → (𝑎 ∈ (Fmla‘suc suc 𝑁) ∧ 𝑏 ∈ (Fmla‘suc suc 𝑁))))) |