| Step | Hyp | Ref
| Expression |
| 1 | | goaln0 35398 |
. . 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 |
. . . . . . . . 9
⊢ (𝑥 = ∅ → (𝑎 ∈ (Fmla‘suc 𝑥) ↔ 𝑎 ∈ (Fmla‘suc
∅))) |
| 8 | 6, 7 | imbi12d 344 |
. . . . . . . 8
⊢ (𝑥 = ∅ →
((∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑥) → 𝑎 ∈ (Fmla‘suc 𝑥)) ↔ (∀𝑔𝑖𝑎 ∈ (Fmla‘suc ∅) → 𝑎 ∈ (Fmla‘suc
∅)))) |
| 9 | | suceq 6450 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → suc 𝑥 = suc 𝑦) |
| 10 | 9 | fveq2d 6910 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (Fmla‘suc 𝑥) = (Fmla‘suc 𝑦)) |
| 11 | 10 | eleq2d 2827 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑥) ↔ ∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑦))) |
| 12 | 10 | eleq2d 2827 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑎 ∈ (Fmla‘suc 𝑥) ↔ 𝑎 ∈ (Fmla‘suc 𝑦))) |
| 13 | 11, 12 | imbi12d 344 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → ((∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑥) → 𝑎 ∈ (Fmla‘suc 𝑥)) ↔ (∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑦) → 𝑎 ∈ (Fmla‘suc 𝑦)))) |
| 14 | | suceq 6450 |
. . . . . . . . . . 11
⊢ (𝑥 = suc 𝑦 → suc 𝑥 = suc suc 𝑦) |
| 15 | 14 | fveq2d 6910 |
. . . . . . . . . 10
⊢ (𝑥 = suc 𝑦 → (Fmla‘suc 𝑥) = (Fmla‘suc suc 𝑦)) |
| 16 | 15 | eleq2d 2827 |
. . . . . . . . 9
⊢ (𝑥 = suc 𝑦 → (∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑥) ↔ ∀𝑔𝑖𝑎 ∈ (Fmla‘suc suc 𝑦))) |
| 17 | 15 | eleq2d 2827 |
. . . . . . . . 9
⊢ (𝑥 = suc 𝑦 → (𝑎 ∈ (Fmla‘suc 𝑥) ↔ 𝑎 ∈ (Fmla‘suc suc 𝑦))) |
| 18 | 16, 17 | imbi12d 344 |
. . . . . . . 8
⊢ (𝑥 = suc 𝑦 → ((∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑥) → 𝑎 ∈ (Fmla‘suc 𝑥)) ↔ (∀𝑔𝑖𝑎 ∈ (Fmla‘suc suc 𝑦) → 𝑎 ∈ (Fmla‘suc suc 𝑦)))) |
| 19 | | suceq 6450 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑛 → suc 𝑥 = suc 𝑛) |
| 20 | 19 | fveq2d 6910 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑛 → (Fmla‘suc 𝑥) = (Fmla‘suc 𝑛)) |
| 21 | 20 | eleq2d 2827 |
. . . . . . . . 9
⊢ (𝑥 = 𝑛 → (∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑥) ↔ ∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑛))) |
| 22 | 20 | eleq2d 2827 |
. . . . . . . . 9
⊢ (𝑥 = 𝑛 → (𝑎 ∈ (Fmla‘suc 𝑥) ↔ 𝑎 ∈ (Fmla‘suc 𝑛))) |
| 23 | 21, 22 | imbi12d 344 |
. . . . . . . 8
⊢ (𝑥 = 𝑛 → ((∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑥) → 𝑎 ∈ (Fmla‘suc 𝑥)) ↔ (∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑛) → 𝑎 ∈ (Fmla‘suc 𝑛)))) |
| 24 | | peano1 7910 |
. . . . . . . . . 10
⊢ ∅
∈ ω |
| 25 | | df-goal 35347 |
. . . . . . . . . . 11
⊢
∀𝑔𝑖𝑎 = 〈2o, 〈𝑖, 𝑎〉〉 |
| 26 | | opex 5469 |
. . . . . . . . . . 11
⊢
〈2o, 〈𝑖, 𝑎〉〉 ∈ V |
| 27 | 25, 26 | eqeltri 2837 |
. . . . . . . . . 10
⊢
∀𝑔𝑖𝑎 ∈ V |
| 28 | | isfmlasuc 35393 |
. . . . . . . . . 10
⊢ ((∅
∈ ω ∧ ∀𝑔𝑖𝑎 ∈ V) →
(∀𝑔𝑖𝑎 ∈ (Fmla‘suc ∅) ↔
(∀𝑔𝑖𝑎 ∈ (Fmla‘∅) ∨
∃𝑢 ∈
(Fmla‘∅)(∃𝑣 ∈
(Fmla‘∅)∀𝑔𝑖𝑎 = (𝑢⊼𝑔𝑣) ∨ ∃𝑘 ∈ ω
∀𝑔𝑖𝑎 = ∀𝑔𝑘𝑢)))) |
| 29 | 24, 27, 28 | mp2an 692 |
. . . . . . . . 9
⊢
(∀𝑔𝑖𝑎 ∈ (Fmla‘suc ∅) ↔
(∀𝑔𝑖𝑎 ∈ (Fmla‘∅) ∨
∃𝑢 ∈
(Fmla‘∅)(∃𝑣 ∈
(Fmla‘∅)∀𝑔𝑖𝑎 = (𝑢⊼𝑔𝑣) ∨ ∃𝑘 ∈ ω
∀𝑔𝑖𝑎 = ∀𝑔𝑘𝑢))) |
| 30 | | eqeq1 2741 |
. . . . . . . . . . . . 13
⊢ (𝑥 =
∀𝑔𝑖𝑎 → (𝑥 = (𝑘∈𝑔𝑗) ↔ ∀𝑔𝑖𝑎 = (𝑘∈𝑔𝑗))) |
| 31 | 30 | 2rexbidv 3222 |
. . . . . . . . . . . 12
⊢ (𝑥 =
∀𝑔𝑖𝑎 → (∃𝑘 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑘∈𝑔𝑗) ↔ ∃𝑘 ∈ ω ∃𝑗 ∈ ω
∀𝑔𝑖𝑎 = (𝑘∈𝑔𝑗))) |
| 32 | | fmla0 35387 |
. . . . . . . . . . . 12
⊢
(Fmla‘∅) = {𝑥 ∈ V ∣ ∃𝑘 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑘∈𝑔𝑗)} |
| 33 | 31, 32 | elrab2 3695 |
. . . . . . . . . . 11
⊢
(∀𝑔𝑖𝑎 ∈ (Fmla‘∅) ↔
(∀𝑔𝑖𝑎 ∈ V ∧ ∃𝑘 ∈ ω ∃𝑗 ∈ ω
∀𝑔𝑖𝑎 = (𝑘∈𝑔𝑗))) |
| 34 | 25 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ω ∧ 𝑗 ∈ ω) →
∀𝑔𝑖𝑎 = 〈2o, 〈𝑖, 𝑎〉〉) |
| 35 | | goel 35352 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ω ∧ 𝑗 ∈ ω) → (𝑘∈𝑔𝑗) = 〈∅, 〈𝑘, 𝑗〉〉) |
| 36 | 34, 35 | eqeq12d 2753 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ω ∧ 𝑗 ∈ ω) →
(∀𝑔𝑖𝑎 = (𝑘∈𝑔𝑗) ↔ 〈2o, 〈𝑖, 𝑎〉〉 = 〈∅, 〈𝑘, 𝑗〉〉)) |
| 37 | | 2oex 8517 |
. . . . . . . . . . . . . . . 16
⊢
2o ∈ V |
| 38 | | opex 5469 |
. . . . . . . . . . . . . . . 16
⊢
〈𝑖, 𝑎〉 ∈ V |
| 39 | 37, 38 | opth 5481 |
. . . . . . . . . . . . . . 15
⊢
(〈2o, 〈𝑖, 𝑎〉〉 = 〈∅, 〈𝑘, 𝑗〉〉 ↔ (2o = ∅
∧ 〈𝑖, 𝑎〉 = 〈𝑘, 𝑗〉)) |
| 40 | | 2on0 8522 |
. . . . . . . . . . . . . . . . 17
⊢
2o ≠ ∅ |
| 41 | | eqneqall 2951 |
. . . . . . . . . . . . . . . . 17
⊢
(2o = ∅ → (2o ≠ ∅ → 𝑎 ∈ (Fmla‘suc
∅))) |
| 42 | 40, 41 | mpi 20 |
. . . . . . . . . . . . . . . 16
⊢
(2o = ∅ → 𝑎 ∈ (Fmla‘suc
∅)) |
| 43 | 42 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢
((2o = ∅ ∧ 〈𝑖, 𝑎〉 = 〈𝑘, 𝑗〉) → 𝑎 ∈ (Fmla‘suc
∅)) |
| 44 | 39, 43 | sylbi 217 |
. . . . . . . . . . . . . 14
⊢
(〈2o, 〈𝑖, 𝑎〉〉 = 〈∅, 〈𝑘, 𝑗〉〉 → 𝑎 ∈ (Fmla‘suc
∅)) |
| 45 | 36, 44 | biimtrdi 253 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ω ∧ 𝑗 ∈ ω) →
(∀𝑔𝑖𝑎 = (𝑘∈𝑔𝑗) → 𝑎 ∈ (Fmla‘suc
∅))) |
| 46 | 45 | rexlimdva 3155 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ω →
(∃𝑗 ∈ ω
∀𝑔𝑖𝑎 = (𝑘∈𝑔𝑗) → 𝑎 ∈ (Fmla‘suc
∅))) |
| 47 | 46 | rexlimiv 3148 |
. . . . . . . . . . 11
⊢
(∃𝑘 ∈
ω ∃𝑗 ∈
ω ∀𝑔𝑖𝑎 = (𝑘∈𝑔𝑗) → 𝑎 ∈ (Fmla‘suc
∅)) |
| 48 | 33, 47 | simplbiim 504 |
. . . . . . . . . 10
⊢
(∀𝑔𝑖𝑎 ∈ (Fmla‘∅) → 𝑎 ∈ (Fmla‘suc
∅)) |
| 49 | | gonanegoal 35357 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢⊼𝑔𝑣) ≠
∀𝑔𝑖𝑎 |
| 50 | | eqneqall 2951 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢⊼𝑔𝑣) =
∀𝑔𝑖𝑎 → ((𝑢⊼𝑔𝑣) ≠ ∀𝑔𝑖𝑎 → 𝑎 ∈ (Fmla‘suc
∅))) |
| 51 | 49, 50 | mpi 20 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢⊼𝑔𝑣) =
∀𝑔𝑖𝑎 → 𝑎 ∈ (Fmla‘suc
∅)) |
| 52 | 51 | eqcoms 2745 |
. . . . . . . . . . . . . 14
⊢
(∀𝑔𝑖𝑎 = (𝑢⊼𝑔𝑣) → 𝑎 ∈ (Fmla‘suc
∅)) |
| 53 | 52 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∈ (Fmla‘∅)
∧ 𝑣 ∈
(Fmla‘∅)) → (∀𝑔𝑖𝑎 = (𝑢⊼𝑔𝑣) → 𝑎 ∈ (Fmla‘suc
∅))) |
| 54 | 53 | rexlimdva 3155 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ (Fmla‘∅)
→ (∃𝑣 ∈
(Fmla‘∅)∀𝑔𝑖𝑎 = (𝑢⊼𝑔𝑣) → 𝑎 ∈ (Fmla‘suc
∅))) |
| 55 | | df-goal 35347 |
. . . . . . . . . . . . . . 15
⊢
∀𝑔𝑘𝑢 = 〈2o, 〈𝑘, 𝑢〉〉 |
| 56 | 25, 55 | eqeq12i 2755 |
. . . . . . . . . . . . . 14
⊢
(∀𝑔𝑖𝑎 = ∀𝑔𝑘𝑢 ↔ 〈2o, 〈𝑖, 𝑎〉〉 = 〈2o,
〈𝑘, 𝑢〉〉) |
| 57 | 37, 38 | opth 5481 |
. . . . . . . . . . . . . . . . 17
⊢
(〈2o, 〈𝑖, 𝑎〉〉 = 〈2o,
〈𝑘, 𝑢〉〉 ↔ (2o =
2o ∧ 〈𝑖, 𝑎〉 = 〈𝑘, 𝑢〉)) |
| 58 | | vex 3484 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑖 ∈ V |
| 59 | | vex 3484 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑎 ∈ V |
| 60 | 58, 59 | opth 5481 |
. . . . . . . . . . . . . . . . . 18
⊢
(〈𝑖, 𝑎〉 = 〈𝑘, 𝑢〉 ↔ (𝑖 = 𝑘 ∧ 𝑎 = 𝑢)) |
| 61 | | eleq1w 2824 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑢 = 𝑎 → (𝑢 ∈ (Fmla‘∅) ↔ 𝑎 ∈
(Fmla‘∅))) |
| 62 | | fmlasssuc 35394 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (∅
∈ ω → (Fmla‘∅) ⊆ (Fmla‘suc
∅)) |
| 63 | 24, 62 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(Fmla‘∅) ⊆ (Fmla‘suc ∅) |
| 64 | 63 | sseli 3979 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 ∈ (Fmla‘∅)
→ 𝑎 ∈
(Fmla‘suc ∅)) |
| 65 | 61, 64 | biimtrdi 253 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 = 𝑎 → (𝑢 ∈ (Fmla‘∅) → 𝑎 ∈ (Fmla‘suc
∅))) |
| 66 | 65 | eqcoms 2745 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = 𝑢 → (𝑢 ∈ (Fmla‘∅) → 𝑎 ∈ (Fmla‘suc
∅))) |
| 67 | 60, 66 | simplbiim 504 |
. . . . . . . . . . . . . . . . 17
⊢
(〈𝑖, 𝑎〉 = 〈𝑘, 𝑢〉 → (𝑢 ∈ (Fmla‘∅) → 𝑎 ∈ (Fmla‘suc
∅))) |
| 68 | 57, 67 | simplbiim 504 |
. . . . . . . . . . . . . . . 16
⊢
(〈2o, 〈𝑖, 𝑎〉〉 = 〈2o,
〈𝑘, 𝑢〉〉 → (𝑢 ∈ (Fmla‘∅) → 𝑎 ∈ (Fmla‘suc
∅))) |
| 69 | 68 | com12 32 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ (Fmla‘∅)
→ (〈2o, 〈𝑖, 𝑎〉〉 = 〈2o,
〈𝑘, 𝑢〉〉 → 𝑎 ∈ (Fmla‘suc
∅))) |
| 70 | 69 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ (Fmla‘∅)
∧ 𝑘 ∈ ω)
→ (〈2o, 〈𝑖, 𝑎〉〉 = 〈2o,
〈𝑘, 𝑢〉〉 → 𝑎 ∈ (Fmla‘suc
∅))) |
| 71 | 56, 70 | biimtrid 242 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∈ (Fmla‘∅)
∧ 𝑘 ∈ ω)
→ (∀𝑔𝑖𝑎 = ∀𝑔𝑘𝑢 → 𝑎 ∈ (Fmla‘suc
∅))) |
| 72 | 71 | rexlimdva 3155 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ (Fmla‘∅)
→ (∃𝑘 ∈
ω ∀𝑔𝑖𝑎 = ∀𝑔𝑘𝑢 → 𝑎 ∈ (Fmla‘suc
∅))) |
| 73 | 54, 72 | jaod 860 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (Fmla‘∅)
→ ((∃𝑣 ∈
(Fmla‘∅)∀𝑔𝑖𝑎 = (𝑢⊼𝑔𝑣) ∨ ∃𝑘 ∈ ω
∀𝑔𝑖𝑎 = ∀𝑔𝑘𝑢) → 𝑎 ∈ (Fmla‘suc
∅))) |
| 74 | 73 | rexlimiv 3148 |
. . . . . . . . . 10
⊢
(∃𝑢 ∈
(Fmla‘∅)(∃𝑣 ∈
(Fmla‘∅)∀𝑔𝑖𝑎 = (𝑢⊼𝑔𝑣) ∨ ∃𝑘 ∈ ω
∀𝑔𝑖𝑎 = ∀𝑔𝑘𝑢) → 𝑎 ∈ (Fmla‘suc
∅)) |
| 75 | 48, 74 | jaoi 858 |
. . . . . . . . 9
⊢
((∀𝑔𝑖𝑎 ∈ (Fmla‘∅) ∨
∃𝑢 ∈
(Fmla‘∅)(∃𝑣 ∈
(Fmla‘∅)∀𝑔𝑖𝑎 = (𝑢⊼𝑔𝑣) ∨ ∃𝑘 ∈ ω
∀𝑔𝑖𝑎 = ∀𝑔𝑘𝑢)) → 𝑎 ∈ (Fmla‘suc
∅)) |
| 76 | 29, 75 | sylbi 217 |
. . . . . . . 8
⊢
(∀𝑔𝑖𝑎 ∈ (Fmla‘suc ∅) → 𝑎 ∈ (Fmla‘suc
∅)) |
| 77 | | goalrlem 35401 |
. . . . . . . 8
⊢ (𝑦 ∈ ω →
((∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑦) → 𝑎 ∈ (Fmla‘suc 𝑦)) → (∀𝑔𝑖𝑎 ∈ (Fmla‘suc suc 𝑦) → 𝑎 ∈ (Fmla‘suc suc 𝑦)))) |
| 78 | 8, 13, 18, 23, 76, 77 | finds 7918 |
. . . . . . 7
⊢ (𝑛 ∈ ω →
(∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑛) → 𝑎 ∈ (Fmla‘suc 𝑛))) |
| 79 | 78 | adantr 480 |
. . . . . 6
⊢ ((𝑛 ∈ ω ∧ 𝑁 = suc 𝑛) → (∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑛) → 𝑎 ∈ (Fmla‘suc 𝑛))) |
| 80 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑁 = suc 𝑛 → (Fmla‘𝑁) = (Fmla‘suc 𝑛)) |
| 81 | 80 | eleq2d 2827 |
. . . . . . . 8
⊢ (𝑁 = suc 𝑛 → (∀𝑔𝑖𝑎 ∈ (Fmla‘𝑁) ↔ ∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑛))) |
| 82 | 80 | eleq2d 2827 |
. . . . . . . 8
⊢ (𝑁 = suc 𝑛 → (𝑎 ∈ (Fmla‘𝑁) ↔ 𝑎 ∈ (Fmla‘suc 𝑛))) |
| 83 | 81, 82 | imbi12d 344 |
. . . . . . 7
⊢ (𝑁 = suc 𝑛 → ((∀𝑔𝑖𝑎 ∈ (Fmla‘𝑁) → 𝑎 ∈ (Fmla‘𝑁)) ↔ (∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑛) → 𝑎 ∈ (Fmla‘suc 𝑛)))) |
| 84 | 83 | adantl 481 |
. . . . . 6
⊢ ((𝑛 ∈ ω ∧ 𝑁 = suc 𝑛) → ((∀𝑔𝑖𝑎 ∈ (Fmla‘𝑁) → 𝑎 ∈ (Fmla‘𝑁)) ↔ (∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑛) → 𝑎 ∈ (Fmla‘suc 𝑛)))) |
| 85 | 79, 84 | mpbird 257 |
. . . . 5
⊢ ((𝑛 ∈ ω ∧ 𝑁 = suc 𝑛) → (∀𝑔𝑖𝑎 ∈ (Fmla‘𝑁) → 𝑎 ∈ (Fmla‘𝑁))) |
| 86 | 85 | rexlimiva 3147 |
. . . 4
⊢
(∃𝑛 ∈
ω 𝑁 = suc 𝑛 →
(∀𝑔𝑖𝑎 ∈ (Fmla‘𝑁) → 𝑎 ∈ (Fmla‘𝑁))) |
| 87 | 3, 86 | syl 17 |
. . 3
⊢ ((𝑁 ∈ ω ∧ 𝑁 ≠ ∅) →
(∀𝑔𝑖𝑎 ∈ (Fmla‘𝑁) → 𝑎 ∈ (Fmla‘𝑁))) |
| 88 | 87 | impancom 451 |
. 2
⊢ ((𝑁 ∈ ω ∧
∀𝑔𝑖𝑎 ∈ (Fmla‘𝑁)) → (𝑁 ≠ ∅ → 𝑎 ∈ (Fmla‘𝑁))) |
| 89 | 2, 88 | mpd 15 |
1
⊢ ((𝑁 ∈ ω ∧
∀𝑔𝑖𝑎 ∈ (Fmla‘𝑁)) → 𝑎 ∈ (Fmla‘𝑁)) |