| Step | Hyp | Ref
| Expression |
| 1 | | gonan0 35397 |
. . 3
⊢ ((𝑎⊼𝑔𝑏) ∈ (Fmla‘𝑁) → 𝑁 ≠ ∅) |
| 2 | 1 | adantl 481 |
. 2
⊢ ((𝑁 ∈ ω ∧ (𝑎⊼𝑔𝑏) ∈ (Fmla‘𝑁)) → 𝑁 ≠ ∅) |
| 3 | | nnsuc 7905 |
. . . 4
⊢ ((𝑁 ∈ ω ∧ 𝑁 ≠ ∅) →
∃𝑥 ∈ ω
𝑁 = suc 𝑥) |
| 4 | | suceq 6450 |
. . . . . . . . . . 11
⊢ (𝑑 = ∅ → suc 𝑑 = suc ∅) |
| 5 | 4 | fveq2d 6910 |
. . . . . . . . . 10
⊢ (𝑑 = ∅ →
(Fmla‘suc 𝑑) =
(Fmla‘suc ∅)) |
| 6 | 5 | eleq2d 2827 |
. . . . . . . . 9
⊢ (𝑑 = ∅ → ((𝑎⊼𝑔𝑏) ∈ (Fmla‘suc 𝑑) ↔ (𝑎⊼𝑔𝑏) ∈ (Fmla‘suc
∅))) |
| 7 | 5 | eleq2d 2827 |
. . . . . . . . . 10
⊢ (𝑑 = ∅ → (𝑎 ∈ (Fmla‘suc 𝑑) ↔ 𝑎 ∈ (Fmla‘suc
∅))) |
| 8 | 5 | eleq2d 2827 |
. . . . . . . . . 10
⊢ (𝑑 = ∅ → (𝑏 ∈ (Fmla‘suc 𝑑) ↔ 𝑏 ∈ (Fmla‘suc
∅))) |
| 9 | 7, 8 | anbi12d 632 |
. . . . . . . . 9
⊢ (𝑑 = ∅ → ((𝑎 ∈ (Fmla‘suc 𝑑) ∧ 𝑏 ∈ (Fmla‘suc 𝑑)) ↔ (𝑎 ∈ (Fmla‘suc ∅) ∧ 𝑏 ∈ (Fmla‘suc
∅)))) |
| 10 | 6, 9 | imbi12d 344 |
. . . . . . . 8
⊢ (𝑑 = ∅ → (((𝑎⊼𝑔𝑏) ∈ (Fmla‘suc 𝑑) → (𝑎 ∈ (Fmla‘suc 𝑑) ∧ 𝑏 ∈ (Fmla‘suc 𝑑))) ↔ ((𝑎⊼𝑔𝑏) ∈ (Fmla‘suc ∅) →
(𝑎 ∈ (Fmla‘suc
∅) ∧ 𝑏 ∈
(Fmla‘suc ∅))))) |
| 11 | | suceq 6450 |
. . . . . . . . . . 11
⊢ (𝑑 = 𝑐 → suc 𝑑 = suc 𝑐) |
| 12 | 11 | fveq2d 6910 |
. . . . . . . . . 10
⊢ (𝑑 = 𝑐 → (Fmla‘suc 𝑑) = (Fmla‘suc 𝑐)) |
| 13 | 12 | eleq2d 2827 |
. . . . . . . . 9
⊢ (𝑑 = 𝑐 → ((𝑎⊼𝑔𝑏) ∈ (Fmla‘suc 𝑑) ↔ (𝑎⊼𝑔𝑏) ∈ (Fmla‘suc 𝑐))) |
| 14 | 12 | eleq2d 2827 |
. . . . . . . . . 10
⊢ (𝑑 = 𝑐 → (𝑎 ∈ (Fmla‘suc 𝑑) ↔ 𝑎 ∈ (Fmla‘suc 𝑐))) |
| 15 | 12 | eleq2d 2827 |
. . . . . . . . . 10
⊢ (𝑑 = 𝑐 → (𝑏 ∈ (Fmla‘suc 𝑑) ↔ 𝑏 ∈ (Fmla‘suc 𝑐))) |
| 16 | 14, 15 | anbi12d 632 |
. . . . . . . . 9
⊢ (𝑑 = 𝑐 → ((𝑎 ∈ (Fmla‘suc 𝑑) ∧ 𝑏 ∈ (Fmla‘suc 𝑑)) ↔ (𝑎 ∈ (Fmla‘suc 𝑐) ∧ 𝑏 ∈ (Fmla‘suc 𝑐)))) |
| 17 | 13, 16 | imbi12d 344 |
. . . . . . . 8
⊢ (𝑑 = 𝑐 → (((𝑎⊼𝑔𝑏) ∈ (Fmla‘suc 𝑑) → (𝑎 ∈ (Fmla‘suc 𝑑) ∧ 𝑏 ∈ (Fmla‘suc 𝑑))) ↔ ((𝑎⊼𝑔𝑏) ∈ (Fmla‘suc 𝑐) → (𝑎 ∈ (Fmla‘suc 𝑐) ∧ 𝑏 ∈ (Fmla‘suc 𝑐))))) |
| 18 | | suceq 6450 |
. . . . . . . . . . 11
⊢ (𝑑 = suc 𝑐 → suc 𝑑 = suc suc 𝑐) |
| 19 | 18 | fveq2d 6910 |
. . . . . . . . . 10
⊢ (𝑑 = suc 𝑐 → (Fmla‘suc 𝑑) = (Fmla‘suc suc 𝑐)) |
| 20 | 19 | eleq2d 2827 |
. . . . . . . . 9
⊢ (𝑑 = suc 𝑐 → ((𝑎⊼𝑔𝑏) ∈ (Fmla‘suc 𝑑) ↔ (𝑎⊼𝑔𝑏) ∈ (Fmla‘suc suc 𝑐))) |
| 21 | 19 | eleq2d 2827 |
. . . . . . . . . 10
⊢ (𝑑 = suc 𝑐 → (𝑎 ∈ (Fmla‘suc 𝑑) ↔ 𝑎 ∈ (Fmla‘suc suc 𝑐))) |
| 22 | 19 | eleq2d 2827 |
. . . . . . . . . 10
⊢ (𝑑 = suc 𝑐 → (𝑏 ∈ (Fmla‘suc 𝑑) ↔ 𝑏 ∈ (Fmla‘suc suc 𝑐))) |
| 23 | 21, 22 | anbi12d 632 |
. . . . . . . . 9
⊢ (𝑑 = suc 𝑐 → ((𝑎 ∈ (Fmla‘suc 𝑑) ∧ 𝑏 ∈ (Fmla‘suc 𝑑)) ↔ (𝑎 ∈ (Fmla‘suc suc 𝑐) ∧ 𝑏 ∈ (Fmla‘suc suc 𝑐)))) |
| 24 | 20, 23 | imbi12d 344 |
. . . . . . . 8
⊢ (𝑑 = suc 𝑐 → (((𝑎⊼𝑔𝑏) ∈ (Fmla‘suc 𝑑) → (𝑎 ∈ (Fmla‘suc 𝑑) ∧ 𝑏 ∈ (Fmla‘suc 𝑑))) ↔ ((𝑎⊼𝑔𝑏) ∈ (Fmla‘suc suc 𝑐) → (𝑎 ∈ (Fmla‘suc suc 𝑐) ∧ 𝑏 ∈ (Fmla‘suc suc 𝑐))))) |
| 25 | | suceq 6450 |
. . . . . . . . . . 11
⊢ (𝑑 = 𝑥 → suc 𝑑 = suc 𝑥) |
| 26 | 25 | fveq2d 6910 |
. . . . . . . . . 10
⊢ (𝑑 = 𝑥 → (Fmla‘suc 𝑑) = (Fmla‘suc 𝑥)) |
| 27 | 26 | eleq2d 2827 |
. . . . . . . . 9
⊢ (𝑑 = 𝑥 → ((𝑎⊼𝑔𝑏) ∈ (Fmla‘suc 𝑑) ↔ (𝑎⊼𝑔𝑏) ∈ (Fmla‘suc 𝑥))) |
| 28 | 26 | eleq2d 2827 |
. . . . . . . . . 10
⊢ (𝑑 = 𝑥 → (𝑎 ∈ (Fmla‘suc 𝑑) ↔ 𝑎 ∈ (Fmla‘suc 𝑥))) |
| 29 | 26 | eleq2d 2827 |
. . . . . . . . . 10
⊢ (𝑑 = 𝑥 → (𝑏 ∈ (Fmla‘suc 𝑑) ↔ 𝑏 ∈ (Fmla‘suc 𝑥))) |
| 30 | 28, 29 | anbi12d 632 |
. . . . . . . . 9
⊢ (𝑑 = 𝑥 → ((𝑎 ∈ (Fmla‘suc 𝑑) ∧ 𝑏 ∈ (Fmla‘suc 𝑑)) ↔ (𝑎 ∈ (Fmla‘suc 𝑥) ∧ 𝑏 ∈ (Fmla‘suc 𝑥)))) |
| 31 | 27, 30 | imbi12d 344 |
. . . . . . . 8
⊢ (𝑑 = 𝑥 → (((𝑎⊼𝑔𝑏) ∈ (Fmla‘suc 𝑑) → (𝑎 ∈ (Fmla‘suc 𝑑) ∧ 𝑏 ∈ (Fmla‘suc 𝑑))) ↔ ((𝑎⊼𝑔𝑏) ∈ (Fmla‘suc 𝑥) → (𝑎 ∈ (Fmla‘suc 𝑥) ∧ 𝑏 ∈ (Fmla‘suc 𝑥))))) |
| 32 | | peano1 7910 |
. . . . . . . . . 10
⊢ ∅
∈ ω |
| 33 | | ovex 7464 |
. . . . . . . . . 10
⊢ (𝑎⊼𝑔𝑏) ∈ V |
| 34 | | isfmlasuc 35393 |
. . . . . . . . . 10
⊢ ((∅
∈ ω ∧ (𝑎⊼𝑔𝑏) ∈ V) → ((𝑎⊼𝑔𝑏) ∈ (Fmla‘suc ∅) ↔
((𝑎⊼𝑔𝑏) ∈ (Fmla‘∅) ∨
∃𝑢 ∈
(Fmla‘∅)(∃𝑣 ∈ (Fmla‘∅)(𝑎⊼𝑔𝑏) = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω (𝑎⊼𝑔𝑏) = ∀𝑔𝑖𝑢)))) |
| 35 | 32, 33, 34 | mp2an 692 |
. . . . . . . . 9
⊢ ((𝑎⊼𝑔𝑏) ∈ (Fmla‘suc
∅) ↔ ((𝑎⊼𝑔𝑏) ∈ (Fmla‘∅) ∨
∃𝑢 ∈
(Fmla‘∅)(∃𝑣 ∈ (Fmla‘∅)(𝑎⊼𝑔𝑏) = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω (𝑎⊼𝑔𝑏) = ∀𝑔𝑖𝑢))) |
| 36 | | eqeq1 2741 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑎⊼𝑔𝑏) → (𝑥 = (𝑖∈𝑔𝑗) ↔ (𝑎⊼𝑔𝑏) = (𝑖∈𝑔𝑗))) |
| 37 | 36 | 2rexbidv 3222 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑎⊼𝑔𝑏) → (∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑎⊼𝑔𝑏) = (𝑖∈𝑔𝑗))) |
| 38 | | fmla0 35387 |
. . . . . . . . . . . 12
⊢
(Fmla‘∅) = {𝑥 ∈ V ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)} |
| 39 | 37, 38 | elrab2 3695 |
. . . . . . . . . . 11
⊢ ((𝑎⊼𝑔𝑏) ∈ (Fmla‘∅)
↔ ((𝑎⊼𝑔𝑏) ∈ V ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑎⊼𝑔𝑏) = (𝑖∈𝑔𝑗))) |
| 40 | | gonafv 35355 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 ∈ V ∧ 𝑏 ∈ V) → (𝑎⊼𝑔𝑏) = 〈1o,
〈𝑎, 𝑏〉〉) |
| 41 | 40 | el2v 3487 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎⊼𝑔𝑏) = 〈1o,
〈𝑎, 𝑏〉〉 |
| 42 | 41 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (𝑎⊼𝑔𝑏) = 〈1o,
〈𝑎, 𝑏〉〉) |
| 43 | | goel 35352 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (𝑖∈𝑔𝑗) = 〈∅, 〈𝑖, 𝑗〉〉) |
| 44 | 42, 43 | eqeq12d 2753 |
. . . . . . . . . . . . . . 15
⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ((𝑎⊼𝑔𝑏) = (𝑖∈𝑔𝑗) ↔ 〈1o, 〈𝑎, 𝑏〉〉 = 〈∅, 〈𝑖, 𝑗〉〉)) |
| 45 | | 1oex 8516 |
. . . . . . . . . . . . . . . . 17
⊢
1o ∈ V |
| 46 | | opex 5469 |
. . . . . . . . . . . . . . . . 17
⊢
〈𝑎, 𝑏〉 ∈ V |
| 47 | 45, 46 | opth 5481 |
. . . . . . . . . . . . . . . 16
⊢
(〈1o, 〈𝑎, 𝑏〉〉 = 〈∅, 〈𝑖, 𝑗〉〉 ↔ (1o = ∅
∧ 〈𝑎, 𝑏〉 = 〈𝑖, 𝑗〉)) |
| 48 | | 1n0 8526 |
. . . . . . . . . . . . . . . . . 18
⊢
1o ≠ ∅ |
| 49 | | eqneqall 2951 |
. . . . . . . . . . . . . . . . . 18
⊢
(1o = ∅ → (1o ≠ ∅ →
(𝑎 ∈ (Fmla‘suc
∅) ∧ 𝑏 ∈
(Fmla‘suc ∅)))) |
| 50 | 48, 49 | mpi 20 |
. . . . . . . . . . . . . . . . 17
⊢
(1o = ∅ → (𝑎 ∈ (Fmla‘suc ∅) ∧ 𝑏 ∈ (Fmla‘suc
∅))) |
| 51 | 50 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢
((1o = ∅ ∧ 〈𝑎, 𝑏〉 = 〈𝑖, 𝑗〉) → (𝑎 ∈ (Fmla‘suc ∅) ∧ 𝑏 ∈ (Fmla‘suc
∅))) |
| 52 | 47, 51 | sylbi 217 |
. . . . . . . . . . . . . . 15
⊢
(〈1o, 〈𝑎, 𝑏〉〉 = 〈∅, 〈𝑖, 𝑗〉〉 → (𝑎 ∈ (Fmla‘suc ∅) ∧ 𝑏 ∈ (Fmla‘suc
∅))) |
| 53 | 44, 52 | biimtrdi 253 |
. . . . . . . . . . . . . 14
⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ((𝑎⊼𝑔𝑏) = (𝑖∈𝑔𝑗) → (𝑎 ∈ (Fmla‘suc ∅) ∧ 𝑏 ∈ (Fmla‘suc
∅)))) |
| 54 | 53 | rexlimdva 3155 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ ω →
(∃𝑗 ∈ ω
(𝑎⊼𝑔𝑏) = (𝑖∈𝑔𝑗) → (𝑎 ∈ (Fmla‘suc ∅) ∧ 𝑏 ∈ (Fmla‘suc
∅)))) |
| 55 | 54 | rexlimiv 3148 |
. . . . . . . . . . . 12
⊢
(∃𝑖 ∈
ω ∃𝑗 ∈
ω (𝑎⊼𝑔𝑏) = (𝑖∈𝑔𝑗) → (𝑎 ∈ (Fmla‘suc ∅) ∧ 𝑏 ∈ (Fmla‘suc
∅))) |
| 56 | 55 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝑎⊼𝑔𝑏) ∈ V ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑎⊼𝑔𝑏) = (𝑖∈𝑔𝑗)) → (𝑎 ∈ (Fmla‘suc ∅) ∧ 𝑏 ∈ (Fmla‘suc
∅))) |
| 57 | 39, 56 | sylbi 217 |
. . . . . . . . . 10
⊢ ((𝑎⊼𝑔𝑏) ∈ (Fmla‘∅)
→ (𝑎 ∈
(Fmla‘suc ∅) ∧ 𝑏 ∈ (Fmla‘suc
∅))) |
| 58 | 41 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢 ∈ (Fmla‘∅)
∧ 𝑣 ∈
(Fmla‘∅)) → (𝑎⊼𝑔𝑏) = 〈1o, 〈𝑎, 𝑏〉〉) |
| 59 | | gonafv 35355 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢 ∈ (Fmla‘∅)
∧ 𝑣 ∈
(Fmla‘∅)) → (𝑢⊼𝑔𝑣) = 〈1o, 〈𝑢, 𝑣〉〉) |
| 60 | 58, 59 | eqeq12d 2753 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ (Fmla‘∅)
∧ 𝑣 ∈
(Fmla‘∅)) → ((𝑎⊼𝑔𝑏) = (𝑢⊼𝑔𝑣) ↔ 〈1o, 〈𝑎, 𝑏〉〉 = 〈1o,
〈𝑢, 𝑣〉〉)) |
| 61 | 45, 46 | opth 5481 |
. . . . . . . . . . . . . . . . 17
⊢
(〈1o, 〈𝑎, 𝑏〉〉 = 〈1o,
〈𝑢, 𝑣〉〉 ↔ (1o =
1o ∧ 〈𝑎, 𝑏〉 = 〈𝑢, 𝑣〉)) |
| 62 | | vex 3484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑎 ∈ V |
| 63 | | vex 3484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑏 ∈ V |
| 64 | 62, 63 | opth 5481 |
. . . . . . . . . . . . . . . . . . 19
⊢
(〈𝑎, 𝑏〉 = 〈𝑢, 𝑣〉 ↔ (𝑎 = 𝑢 ∧ 𝑏 = 𝑣)) |
| 65 | | simpl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → 𝑎 = 𝑢) |
| 66 | 65 | equcomd 2018 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → 𝑢 = 𝑎) |
| 67 | 66 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → (𝑢 ∈ (Fmla‘∅) ↔ 𝑎 ∈
(Fmla‘∅))) |
| 68 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → 𝑏 = 𝑣) |
| 69 | 68 | equcomd 2018 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → 𝑣 = 𝑏) |
| 70 | 69 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → (𝑣 ∈ (Fmla‘∅) ↔ 𝑏 ∈
(Fmla‘∅))) |
| 71 | 67, 70 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → ((𝑢 ∈ (Fmla‘∅) ∧ 𝑣 ∈ (Fmla‘∅))
↔ (𝑎 ∈
(Fmla‘∅) ∧ 𝑏 ∈
(Fmla‘∅)))) |
| 72 | 64, 71 | sylbi 217 |
. . . . . . . . . . . . . . . . . 18
⊢
(〈𝑎, 𝑏〉 = 〈𝑢, 𝑣〉 → ((𝑢 ∈ (Fmla‘∅) ∧ 𝑣 ∈ (Fmla‘∅))
↔ (𝑎 ∈
(Fmla‘∅) ∧ 𝑏 ∈
(Fmla‘∅)))) |
| 73 | 72 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢
((1o = 1o ∧ 〈𝑎, 𝑏〉 = 〈𝑢, 𝑣〉) → ((𝑢 ∈ (Fmla‘∅) ∧ 𝑣 ∈ (Fmla‘∅))
↔ (𝑎 ∈
(Fmla‘∅) ∧ 𝑏 ∈
(Fmla‘∅)))) |
| 74 | 61, 73 | sylbi 217 |
. . . . . . . . . . . . . . . 16
⊢
(〈1o, 〈𝑎, 𝑏〉〉 = 〈1o,
〈𝑢, 𝑣〉〉 → ((𝑢 ∈ (Fmla‘∅) ∧ 𝑣 ∈ (Fmla‘∅))
↔ (𝑎 ∈
(Fmla‘∅) ∧ 𝑏 ∈
(Fmla‘∅)))) |
| 75 | | fmlasssuc 35394 |
. . . . . . . . . . . . . . . . . . 19
⊢ (∅
∈ ω → (Fmla‘∅) ⊆ (Fmla‘suc
∅)) |
| 76 | 32, 75 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢
(Fmla‘∅) ⊆ (Fmla‘suc ∅) |
| 77 | 76 | sseli 3979 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 ∈ (Fmla‘∅)
→ 𝑎 ∈
(Fmla‘suc ∅)) |
| 78 | 76 | sseli 3979 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 ∈ (Fmla‘∅)
→ 𝑏 ∈
(Fmla‘suc ∅)) |
| 79 | 77, 78 | anim12i 613 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 ∈ (Fmla‘∅)
∧ 𝑏 ∈
(Fmla‘∅)) → (𝑎 ∈ (Fmla‘suc ∅) ∧ 𝑏 ∈ (Fmla‘suc
∅))) |
| 80 | 74, 79 | biimtrdi 253 |
. . . . . . . . . . . . . . 15
⊢
(〈1o, 〈𝑎, 𝑏〉〉 = 〈1o,
〈𝑢, 𝑣〉〉 → ((𝑢 ∈ (Fmla‘∅) ∧ 𝑣 ∈ (Fmla‘∅))
→ (𝑎 ∈
(Fmla‘suc ∅) ∧ 𝑏 ∈ (Fmla‘suc
∅)))) |
| 81 | 80 | com12 32 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ (Fmla‘∅)
∧ 𝑣 ∈
(Fmla‘∅)) → (〈1o, 〈𝑎, 𝑏〉〉 = 〈1o,
〈𝑢, 𝑣〉〉 → (𝑎 ∈ (Fmla‘suc ∅) ∧ 𝑏 ∈ (Fmla‘suc
∅)))) |
| 82 | 60, 81 | sylbid 240 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∈ (Fmla‘∅)
∧ 𝑣 ∈
(Fmla‘∅)) → ((𝑎⊼𝑔𝑏) = (𝑢⊼𝑔𝑣) → (𝑎 ∈ (Fmla‘suc ∅) ∧ 𝑏 ∈ (Fmla‘suc
∅)))) |
| 83 | 82 | rexlimdva 3155 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ (Fmla‘∅)
→ (∃𝑣 ∈
(Fmla‘∅)(𝑎⊼𝑔𝑏) = (𝑢⊼𝑔𝑣) → (𝑎 ∈ (Fmla‘suc ∅) ∧ 𝑏 ∈ (Fmla‘suc
∅)))) |
| 84 | | gonanegoal 35357 |
. . . . . . . . . . . . . . 15
⊢ (𝑎⊼𝑔𝑏) ≠
∀𝑔𝑖𝑢 |
| 85 | | eqneqall 2951 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎⊼𝑔𝑏) =
∀𝑔𝑖𝑢 → ((𝑎⊼𝑔𝑏) ≠ ∀𝑔𝑖𝑢 → (𝑎 ∈ (Fmla‘suc ∅) ∧ 𝑏 ∈ (Fmla‘suc
∅)))) |
| 86 | 84, 85 | mpi 20 |
. . . . . . . . . . . . . 14
⊢ ((𝑎⊼𝑔𝑏) =
∀𝑔𝑖𝑢 → (𝑎 ∈ (Fmla‘suc ∅) ∧ 𝑏 ∈ (Fmla‘suc
∅))) |
| 87 | 86 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∈ (Fmla‘∅)
∧ 𝑖 ∈ ω)
→ ((𝑎⊼𝑔𝑏) = ∀𝑔𝑖𝑢 → (𝑎 ∈ (Fmla‘suc ∅) ∧ 𝑏 ∈ (Fmla‘suc
∅)))) |
| 88 | 87 | rexlimdva 3155 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ (Fmla‘∅)
→ (∃𝑖 ∈
ω (𝑎⊼𝑔𝑏) = ∀𝑔𝑖𝑢 → (𝑎 ∈ (Fmla‘suc ∅) ∧ 𝑏 ∈ (Fmla‘suc
∅)))) |
| 89 | 83, 88 | jaod 860 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (Fmla‘∅)
→ ((∃𝑣 ∈
(Fmla‘∅)(𝑎⊼𝑔𝑏) = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω (𝑎⊼𝑔𝑏) = ∀𝑔𝑖𝑢) → (𝑎 ∈ (Fmla‘suc ∅) ∧ 𝑏 ∈ (Fmla‘suc
∅)))) |
| 90 | 89 | rexlimiv 3148 |
. . . . . . . . . 10
⊢
(∃𝑢 ∈
(Fmla‘∅)(∃𝑣 ∈ (Fmla‘∅)(𝑎⊼𝑔𝑏) = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω (𝑎⊼𝑔𝑏) = ∀𝑔𝑖𝑢) → (𝑎 ∈ (Fmla‘suc ∅) ∧ 𝑏 ∈ (Fmla‘suc
∅))) |
| 91 | 57, 90 | jaoi 858 |
. . . . . . . . 9
⊢ (((𝑎⊼𝑔𝑏) ∈ (Fmla‘∅)
∨ ∃𝑢 ∈
(Fmla‘∅)(∃𝑣 ∈ (Fmla‘∅)(𝑎⊼𝑔𝑏) = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω (𝑎⊼𝑔𝑏) = ∀𝑔𝑖𝑢)) → (𝑎 ∈ (Fmla‘suc ∅) ∧ 𝑏 ∈ (Fmla‘suc
∅))) |
| 92 | 35, 91 | sylbi 217 |
. . . . . . . 8
⊢ ((𝑎⊼𝑔𝑏) ∈ (Fmla‘suc
∅) → (𝑎 ∈
(Fmla‘suc ∅) ∧ 𝑏 ∈ (Fmla‘suc
∅))) |
| 93 | | gonarlem 35399 |
. . . . . . . 8
⊢ (𝑐 ∈ ω → (((𝑎⊼𝑔𝑏) ∈ (Fmla‘suc 𝑐) → (𝑎 ∈ (Fmla‘suc 𝑐) ∧ 𝑏 ∈ (Fmla‘suc 𝑐))) → ((𝑎⊼𝑔𝑏) ∈ (Fmla‘suc suc 𝑐) → (𝑎 ∈ (Fmla‘suc suc 𝑐) ∧ 𝑏 ∈ (Fmla‘suc suc 𝑐))))) |
| 94 | 10, 17, 24, 31, 92, 93 | finds 7918 |
. . . . . . 7
⊢ (𝑥 ∈ ω → ((𝑎⊼𝑔𝑏) ∈ (Fmla‘suc 𝑥) → (𝑎 ∈ (Fmla‘suc 𝑥) ∧ 𝑏 ∈ (Fmla‘suc 𝑥)))) |
| 95 | 94 | adantr 480 |
. . . . . 6
⊢ ((𝑥 ∈ ω ∧ 𝑁 = suc 𝑥) → ((𝑎⊼𝑔𝑏) ∈ (Fmla‘suc 𝑥) → (𝑎 ∈ (Fmla‘suc 𝑥) ∧ 𝑏 ∈ (Fmla‘suc 𝑥)))) |
| 96 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑁 = suc 𝑥 → (Fmla‘𝑁) = (Fmla‘suc 𝑥)) |
| 97 | 96 | eleq2d 2827 |
. . . . . . . 8
⊢ (𝑁 = suc 𝑥 → ((𝑎⊼𝑔𝑏) ∈ (Fmla‘𝑁) ↔ (𝑎⊼𝑔𝑏) ∈ (Fmla‘suc 𝑥))) |
| 98 | 96 | eleq2d 2827 |
. . . . . . . . 9
⊢ (𝑁 = suc 𝑥 → (𝑎 ∈ (Fmla‘𝑁) ↔ 𝑎 ∈ (Fmla‘suc 𝑥))) |
| 99 | 96 | eleq2d 2827 |
. . . . . . . . 9
⊢ (𝑁 = suc 𝑥 → (𝑏 ∈ (Fmla‘𝑁) ↔ 𝑏 ∈ (Fmla‘suc 𝑥))) |
| 100 | 98, 99 | anbi12d 632 |
. . . . . . . 8
⊢ (𝑁 = suc 𝑥 → ((𝑎 ∈ (Fmla‘𝑁) ∧ 𝑏 ∈ (Fmla‘𝑁)) ↔ (𝑎 ∈ (Fmla‘suc 𝑥) ∧ 𝑏 ∈ (Fmla‘suc 𝑥)))) |
| 101 | 97, 100 | imbi12d 344 |
. . . . . . 7
⊢ (𝑁 = suc 𝑥 → (((𝑎⊼𝑔𝑏) ∈ (Fmla‘𝑁) → (𝑎 ∈ (Fmla‘𝑁) ∧ 𝑏 ∈ (Fmla‘𝑁))) ↔ ((𝑎⊼𝑔𝑏) ∈ (Fmla‘suc 𝑥) → (𝑎 ∈ (Fmla‘suc 𝑥) ∧ 𝑏 ∈ (Fmla‘suc 𝑥))))) |
| 102 | 101 | adantl 481 |
. . . . . 6
⊢ ((𝑥 ∈ ω ∧ 𝑁 = suc 𝑥) → (((𝑎⊼𝑔𝑏) ∈ (Fmla‘𝑁) → (𝑎 ∈ (Fmla‘𝑁) ∧ 𝑏 ∈ (Fmla‘𝑁))) ↔ ((𝑎⊼𝑔𝑏) ∈ (Fmla‘suc 𝑥) → (𝑎 ∈ (Fmla‘suc 𝑥) ∧ 𝑏 ∈ (Fmla‘suc 𝑥))))) |
| 103 | 95, 102 | mpbird 257 |
. . . . 5
⊢ ((𝑥 ∈ ω ∧ 𝑁 = suc 𝑥) → ((𝑎⊼𝑔𝑏) ∈ (Fmla‘𝑁) → (𝑎 ∈ (Fmla‘𝑁) ∧ 𝑏 ∈ (Fmla‘𝑁)))) |
| 104 | 103 | rexlimiva 3147 |
. . . 4
⊢
(∃𝑥 ∈
ω 𝑁 = suc 𝑥 → ((𝑎⊼𝑔𝑏) ∈ (Fmla‘𝑁) → (𝑎 ∈ (Fmla‘𝑁) ∧ 𝑏 ∈ (Fmla‘𝑁)))) |
| 105 | 3, 104 | syl 17 |
. . 3
⊢ ((𝑁 ∈ ω ∧ 𝑁 ≠ ∅) → ((𝑎⊼𝑔𝑏) ∈ (Fmla‘𝑁) → (𝑎 ∈ (Fmla‘𝑁) ∧ 𝑏 ∈ (Fmla‘𝑁)))) |
| 106 | 105 | impancom 451 |
. 2
⊢ ((𝑁 ∈ ω ∧ (𝑎⊼𝑔𝑏) ∈ (Fmla‘𝑁)) → (𝑁 ≠ ∅ → (𝑎 ∈ (Fmla‘𝑁) ∧ 𝑏 ∈ (Fmla‘𝑁)))) |
| 107 | 2, 106 | mpd 15 |
1
⊢ ((𝑁 ∈ ω ∧ (𝑎⊼𝑔𝑏) ∈ (Fmla‘𝑁)) → (𝑎 ∈ (Fmla‘𝑁) ∧ 𝑏 ∈ (Fmla‘𝑁))) |