| Step | Hyp | Ref
| Expression |
| 1 | | peano2 7912 |
. . . . 5
⊢ (𝑁 ∈ ω → suc 𝑁 ∈
ω) |
| 2 | | df-goal 35347 |
. . . . . 6
⊢
∀𝑔𝑖𝑎 = 〈2o, 〈𝑖, 𝑎〉〉 |
| 3 | | opex 5469 |
. . . . . 6
⊢
〈2o, 〈𝑖, 𝑎〉〉 ∈ V |
| 4 | 2, 3 | eqeltri 2837 |
. . . . 5
⊢
∀𝑔𝑖𝑎 ∈ V |
| 5 | | isfmlasuc 35393 |
. . . . 5
⊢ ((suc
𝑁 ∈ ω ∧
∀𝑔𝑖𝑎 ∈ V) →
(∀𝑔𝑖𝑎 ∈ (Fmla‘suc suc 𝑁) ↔ (∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑁) ∨ ∃𝑢 ∈ (Fmla‘suc 𝑁)(∃𝑣 ∈ (Fmla‘suc 𝑁)∀𝑔𝑖𝑎 = (𝑢⊼𝑔𝑣) ∨ ∃𝑗 ∈ ω
∀𝑔𝑖𝑎 = ∀𝑔𝑗𝑢)))) |
| 6 | 1, 4, 5 | sylancl 586 |
. . . 4
⊢ (𝑁 ∈ ω →
(∀𝑔𝑖𝑎 ∈ (Fmla‘suc suc 𝑁) ↔ (∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑁) ∨ ∃𝑢 ∈ (Fmla‘suc 𝑁)(∃𝑣 ∈ (Fmla‘suc 𝑁)∀𝑔𝑖𝑎 = (𝑢⊼𝑔𝑣) ∨ ∃𝑗 ∈ ω
∀𝑔𝑖𝑎 = ∀𝑔𝑗𝑢)))) |
| 7 | 6 | adantr 480 |
. . 3
⊢ ((𝑁 ∈ ω ∧
(∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑁) → 𝑎 ∈ (Fmla‘suc 𝑁))) →
(∀𝑔𝑖𝑎 ∈ (Fmla‘suc suc 𝑁) ↔ (∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑁) ∨ ∃𝑢 ∈ (Fmla‘suc 𝑁)(∃𝑣 ∈ (Fmla‘suc 𝑁)∀𝑔𝑖𝑎 = (𝑢⊼𝑔𝑣) ∨ ∃𝑗 ∈ ω
∀𝑔𝑖𝑎 = ∀𝑔𝑗𝑢)))) |
| 8 | | fmlasssuc 35394 |
. . . . . . . . . 10
⊢ (suc
𝑁 ∈ ω →
(Fmla‘suc 𝑁) ⊆
(Fmla‘suc suc 𝑁)) |
| 9 | 1, 8 | syl 17 |
. . . . . . . . 9
⊢ (𝑁 ∈ ω →
(Fmla‘suc 𝑁) ⊆
(Fmla‘suc suc 𝑁)) |
| 10 | 9 | sseld 3982 |
. . . . . . . 8
⊢ (𝑁 ∈ ω → (𝑎 ∈ (Fmla‘suc 𝑁) → 𝑎 ∈ (Fmla‘suc suc 𝑁))) |
| 11 | 10 | com12 32 |
. . . . . . 7
⊢ (𝑎 ∈ (Fmla‘suc 𝑁) → (𝑁 ∈ ω → 𝑎 ∈ (Fmla‘suc suc 𝑁))) |
| 12 | 11 | imim2i 16 |
. . . . . 6
⊢
((∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑁) → 𝑎 ∈ (Fmla‘suc 𝑁)) → (∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑁) → (𝑁 ∈ ω → 𝑎 ∈ (Fmla‘suc suc 𝑁)))) |
| 13 | 12 | com23 86 |
. . . . 5
⊢
((∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑁) → 𝑎 ∈ (Fmla‘suc 𝑁)) → (𝑁 ∈ ω →
(∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑁) → 𝑎 ∈ (Fmla‘suc suc 𝑁)))) |
| 14 | 13 | impcom 407 |
. . . 4
⊢ ((𝑁 ∈ ω ∧
(∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑁) → 𝑎 ∈ (Fmla‘suc 𝑁))) →
(∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑁) → 𝑎 ∈ (Fmla‘suc suc 𝑁))) |
| 15 | | gonanegoal 35357 |
. . . . . . . . . . 11
⊢ (𝑢⊼𝑔𝑣) ≠
∀𝑔𝑖𝑎 |
| 16 | | eqneqall 2951 |
. . . . . . . . . . 11
⊢ ((𝑢⊼𝑔𝑣) =
∀𝑔𝑖𝑎 → ((𝑢⊼𝑔𝑣) ≠ ∀𝑔𝑖𝑎 → 𝑎 ∈ (Fmla‘suc suc 𝑁))) |
| 17 | 15, 16 | mpi 20 |
. . . . . . . . . 10
⊢ ((𝑢⊼𝑔𝑣) =
∀𝑔𝑖𝑎 → 𝑎 ∈ (Fmla‘suc suc 𝑁)) |
| 18 | 17 | eqcoms 2745 |
. . . . . . . . 9
⊢
(∀𝑔𝑖𝑎 = (𝑢⊼𝑔𝑣) → 𝑎 ∈ (Fmla‘suc suc 𝑁)) |
| 19 | 18 | a1i 11 |
. . . . . . . 8
⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘suc 𝑁)) ∧ 𝑣 ∈ (Fmla‘suc 𝑁)) → (∀𝑔𝑖𝑎 = (𝑢⊼𝑔𝑣) → 𝑎 ∈ (Fmla‘suc suc 𝑁))) |
| 20 | 19 | rexlimdva 3155 |
. . . . . . 7
⊢ ((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘suc 𝑁)) → (∃𝑣 ∈ (Fmla‘suc 𝑁)∀𝑔𝑖𝑎 = (𝑢⊼𝑔𝑣) → 𝑎 ∈ (Fmla‘suc suc 𝑁))) |
| 21 | | df-goal 35347 |
. . . . . . . . . . . . 13
⊢
∀𝑔𝑗𝑢 = 〈2o, 〈𝑗, 𝑢〉〉 |
| 22 | 2, 21 | eqeq12i 2755 |
. . . . . . . . . . . 12
⊢
(∀𝑔𝑖𝑎 = ∀𝑔𝑗𝑢 ↔ 〈2o, 〈𝑖, 𝑎〉〉 = 〈2o,
〈𝑗, 𝑢〉〉) |
| 23 | | 2oex 8517 |
. . . . . . . . . . . . 13
⊢
2o ∈ V |
| 24 | | opex 5469 |
. . . . . . . . . . . . 13
⊢
〈𝑖, 𝑎〉 ∈ V |
| 25 | 23, 24 | opth 5481 |
. . . . . . . . . . . 12
⊢
(〈2o, 〈𝑖, 𝑎〉〉 = 〈2o,
〈𝑗, 𝑢〉〉 ↔ (2o =
2o ∧ 〈𝑖, 𝑎〉 = 〈𝑗, 𝑢〉)) |
| 26 | 22, 25 | bitri 275 |
. . . . . . . . . . 11
⊢
(∀𝑔𝑖𝑎 = ∀𝑔𝑗𝑢 ↔ (2o = 2o ∧
〈𝑖, 𝑎〉 = 〈𝑗, 𝑢〉)) |
| 27 | | vex 3484 |
. . . . . . . . . . . . 13
⊢ 𝑖 ∈ V |
| 28 | | vex 3484 |
. . . . . . . . . . . . 13
⊢ 𝑎 ∈ V |
| 29 | 27, 28 | opth 5481 |
. . . . . . . . . . . 12
⊢
(〈𝑖, 𝑎〉 = 〈𝑗, 𝑢〉 ↔ (𝑖 = 𝑗 ∧ 𝑎 = 𝑢)) |
| 30 | | eleq1w 2824 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 = 𝑎 → (𝑢 ∈ (Fmla‘suc 𝑁) ↔ 𝑎 ∈ (Fmla‘suc 𝑁))) |
| 31 | 30 | eqcoms 2745 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 𝑢 → (𝑢 ∈ (Fmla‘suc 𝑁) ↔ 𝑎 ∈ (Fmla‘suc 𝑁))) |
| 32 | 31, 11 | biimtrdi 253 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝑢 → (𝑢 ∈ (Fmla‘suc 𝑁) → (𝑁 ∈ ω → 𝑎 ∈ (Fmla‘suc suc 𝑁)))) |
| 33 | 32 | impcomd 411 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑢 → ((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘suc 𝑁)) → 𝑎 ∈ (Fmla‘suc suc 𝑁))) |
| 34 | 29, 33 | simplbiim 504 |
. . . . . . . . . . 11
⊢
(〈𝑖, 𝑎〉 = 〈𝑗, 𝑢〉 → ((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘suc 𝑁)) → 𝑎 ∈ (Fmla‘suc suc 𝑁))) |
| 35 | 26, 34 | simplbiim 504 |
. . . . . . . . . 10
⊢
(∀𝑔𝑖𝑎 = ∀𝑔𝑗𝑢 → ((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘suc 𝑁)) → 𝑎 ∈ (Fmla‘suc suc 𝑁))) |
| 36 | 35 | com12 32 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘suc 𝑁)) →
(∀𝑔𝑖𝑎 = ∀𝑔𝑗𝑢 → 𝑎 ∈ (Fmla‘suc suc 𝑁))) |
| 37 | 36 | adantr 480 |
. . . . . . . 8
⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘suc 𝑁)) ∧ 𝑗 ∈ ω) →
(∀𝑔𝑖𝑎 = ∀𝑔𝑗𝑢 → 𝑎 ∈ (Fmla‘suc suc 𝑁))) |
| 38 | 37 | rexlimdva 3155 |
. . . . . . 7
⊢ ((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘suc 𝑁)) → (∃𝑗 ∈ ω
∀𝑔𝑖𝑎 = ∀𝑔𝑗𝑢 → 𝑎 ∈ (Fmla‘suc suc 𝑁))) |
| 39 | 20, 38 | jaod 860 |
. . . . . 6
⊢ ((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘suc 𝑁)) → ((∃𝑣 ∈ (Fmla‘suc 𝑁)∀𝑔𝑖𝑎 = (𝑢⊼𝑔𝑣) ∨ ∃𝑗 ∈ ω
∀𝑔𝑖𝑎 = ∀𝑔𝑗𝑢) → 𝑎 ∈ (Fmla‘suc suc 𝑁))) |
| 40 | 39 | rexlimdva 3155 |
. . . . 5
⊢ (𝑁 ∈ ω →
(∃𝑢 ∈
(Fmla‘suc 𝑁)(∃𝑣 ∈ (Fmla‘suc 𝑁)∀𝑔𝑖𝑎 = (𝑢⊼𝑔𝑣) ∨ ∃𝑗 ∈ ω
∀𝑔𝑖𝑎 = ∀𝑔𝑗𝑢) → 𝑎 ∈ (Fmla‘suc suc 𝑁))) |
| 41 | 40 | adantr 480 |
. . . 4
⊢ ((𝑁 ∈ ω ∧
(∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑁) → 𝑎 ∈ (Fmla‘suc 𝑁))) → (∃𝑢 ∈ (Fmla‘suc 𝑁)(∃𝑣 ∈ (Fmla‘suc 𝑁)∀𝑔𝑖𝑎 = (𝑢⊼𝑔𝑣) ∨ ∃𝑗 ∈ ω
∀𝑔𝑖𝑎 = ∀𝑔𝑗𝑢) → 𝑎 ∈ (Fmla‘suc suc 𝑁))) |
| 42 | 14, 41 | jaod 860 |
. . 3
⊢ ((𝑁 ∈ ω ∧
(∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑁) → 𝑎 ∈ (Fmla‘suc 𝑁))) →
((∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑁) ∨ ∃𝑢 ∈ (Fmla‘suc 𝑁)(∃𝑣 ∈ (Fmla‘suc 𝑁)∀𝑔𝑖𝑎 = (𝑢⊼𝑔𝑣) ∨ ∃𝑗 ∈ ω
∀𝑔𝑖𝑎 = ∀𝑔𝑗𝑢)) → 𝑎 ∈ (Fmla‘suc suc 𝑁))) |
| 43 | 7, 42 | sylbid 240 |
. 2
⊢ ((𝑁 ∈ ω ∧
(∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑁) → 𝑎 ∈ (Fmla‘suc 𝑁))) →
(∀𝑔𝑖𝑎 ∈ (Fmla‘suc suc 𝑁) → 𝑎 ∈ (Fmla‘suc suc 𝑁))) |
| 44 | 43 | ex 412 |
1
⊢ (𝑁 ∈ ω →
((∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑁) → 𝑎 ∈ (Fmla‘suc 𝑁)) → (∀𝑔𝑖𝑎 ∈ (Fmla‘suc suc 𝑁) → 𝑎 ∈ (Fmla‘suc suc 𝑁)))) |