Step | Hyp | Ref
| Expression |
1 | | goaln0 32926 |
. . 3
⊢
(∀𝑔𝑖𝑎 ∈ (Fmla‘𝑁) → 𝑁 ≠ ∅) |
2 | 1 | adantl 485 |
. 2
⊢ ((𝑁 ∈ ω ∧
∀𝑔𝑖𝑎 ∈ (Fmla‘𝑁)) → 𝑁 ≠ ∅) |
3 | | nnsuc 7616 |
. . . 4
⊢ ((𝑁 ∈ ω ∧ 𝑁 ≠ ∅) →
∃𝑛 ∈ ω
𝑁 = suc 𝑛) |
4 | | suceq 6237 |
. . . . . . . . . . 11
⊢ (𝑥 = ∅ → suc 𝑥 = suc ∅) |
5 | 4 | fveq2d 6678 |
. . . . . . . . . 10
⊢ (𝑥 = ∅ →
(Fmla‘suc 𝑥) =
(Fmla‘suc ∅)) |
6 | 5 | eleq2d 2818 |
. . . . . . . . 9
⊢ (𝑥 = ∅ →
(∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑥) ↔ ∀𝑔𝑖𝑎 ∈ (Fmla‘suc
∅))) |
7 | 5 | eleq2d 2818 |
. . . . . . . . 9
⊢ (𝑥 = ∅ → (𝑎 ∈ (Fmla‘suc 𝑥) ↔ 𝑎 ∈ (Fmla‘suc
∅))) |
8 | 6, 7 | imbi12d 348 |
. . . . . . . 8
⊢ (𝑥 = ∅ →
((∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑥) → 𝑎 ∈ (Fmla‘suc 𝑥)) ↔ (∀𝑔𝑖𝑎 ∈ (Fmla‘suc ∅) → 𝑎 ∈ (Fmla‘suc
∅)))) |
9 | | suceq 6237 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → suc 𝑥 = suc 𝑦) |
10 | 9 | fveq2d 6678 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (Fmla‘suc 𝑥) = (Fmla‘suc 𝑦)) |
11 | 10 | eleq2d 2818 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑥) ↔ ∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑦))) |
12 | 10 | eleq2d 2818 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑎 ∈ (Fmla‘suc 𝑥) ↔ 𝑎 ∈ (Fmla‘suc 𝑦))) |
13 | 11, 12 | imbi12d 348 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → ((∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑥) → 𝑎 ∈ (Fmla‘suc 𝑥)) ↔ (∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑦) → 𝑎 ∈ (Fmla‘suc 𝑦)))) |
14 | | suceq 6237 |
. . . . . . . . . . 11
⊢ (𝑥 = suc 𝑦 → suc 𝑥 = suc suc 𝑦) |
15 | 14 | fveq2d 6678 |
. . . . . . . . . 10
⊢ (𝑥 = suc 𝑦 → (Fmla‘suc 𝑥) = (Fmla‘suc suc 𝑦)) |
16 | 15 | eleq2d 2818 |
. . . . . . . . 9
⊢ (𝑥 = suc 𝑦 → (∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑥) ↔ ∀𝑔𝑖𝑎 ∈ (Fmla‘suc suc 𝑦))) |
17 | 15 | eleq2d 2818 |
. . . . . . . . 9
⊢ (𝑥 = suc 𝑦 → (𝑎 ∈ (Fmla‘suc 𝑥) ↔ 𝑎 ∈ (Fmla‘suc suc 𝑦))) |
18 | 16, 17 | imbi12d 348 |
. . . . . . . 8
⊢ (𝑥 = suc 𝑦 → ((∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑥) → 𝑎 ∈ (Fmla‘suc 𝑥)) ↔ (∀𝑔𝑖𝑎 ∈ (Fmla‘suc suc 𝑦) → 𝑎 ∈ (Fmla‘suc suc 𝑦)))) |
19 | | suceq 6237 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑛 → suc 𝑥 = suc 𝑛) |
20 | 19 | fveq2d 6678 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑛 → (Fmla‘suc 𝑥) = (Fmla‘suc 𝑛)) |
21 | 20 | eleq2d 2818 |
. . . . . . . . 9
⊢ (𝑥 = 𝑛 → (∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑥) ↔ ∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑛))) |
22 | 20 | eleq2d 2818 |
. . . . . . . . 9
⊢ (𝑥 = 𝑛 → (𝑎 ∈ (Fmla‘suc 𝑥) ↔ 𝑎 ∈ (Fmla‘suc 𝑛))) |
23 | 21, 22 | imbi12d 348 |
. . . . . . . 8
⊢ (𝑥 = 𝑛 → ((∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑥) → 𝑎 ∈ (Fmla‘suc 𝑥)) ↔ (∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑛) → 𝑎 ∈ (Fmla‘suc 𝑛)))) |
24 | | peano1 7620 |
. . . . . . . . . 10
⊢ ∅
∈ ω |
25 | | df-goal 32875 |
. . . . . . . . . . 11
⊢
∀𝑔𝑖𝑎 = 〈2o, 〈𝑖, 𝑎〉〉 |
26 | | opex 5322 |
. . . . . . . . . . 11
⊢
〈2o, 〈𝑖, 𝑎〉〉 ∈ V |
27 | 25, 26 | eqeltri 2829 |
. . . . . . . . . 10
⊢
∀𝑔𝑖𝑎 ∈ V |
28 | | isfmlasuc 32921 |
. . . . . . . . . 10
⊢ ((∅
∈ ω ∧ ∀𝑔𝑖𝑎 ∈ V) →
(∀𝑔𝑖𝑎 ∈ (Fmla‘suc ∅) ↔
(∀𝑔𝑖𝑎 ∈ (Fmla‘∅) ∨
∃𝑢 ∈
(Fmla‘∅)(∃𝑣 ∈
(Fmla‘∅)∀𝑔𝑖𝑎 = (𝑢⊼𝑔𝑣) ∨ ∃𝑘 ∈ ω
∀𝑔𝑖𝑎 = ∀𝑔𝑘𝑢)))) |
29 | 24, 27, 28 | mp2an 692 |
. . . . . . . . 9
⊢
(∀𝑔𝑖𝑎 ∈ (Fmla‘suc ∅) ↔
(∀𝑔𝑖𝑎 ∈ (Fmla‘∅) ∨
∃𝑢 ∈
(Fmla‘∅)(∃𝑣 ∈
(Fmla‘∅)∀𝑔𝑖𝑎 = (𝑢⊼𝑔𝑣) ∨ ∃𝑘 ∈ ω
∀𝑔𝑖𝑎 = ∀𝑔𝑘𝑢))) |
30 | | eqeq1 2742 |
. . . . . . . . . . . . 13
⊢ (𝑥 =
∀𝑔𝑖𝑎 → (𝑥 = (𝑘∈𝑔𝑗) ↔ ∀𝑔𝑖𝑎 = (𝑘∈𝑔𝑗))) |
31 | 30 | 2rexbidv 3210 |
. . . . . . . . . . . 12
⊢ (𝑥 =
∀𝑔𝑖𝑎 → (∃𝑘 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑘∈𝑔𝑗) ↔ ∃𝑘 ∈ ω ∃𝑗 ∈ ω
∀𝑔𝑖𝑎 = (𝑘∈𝑔𝑗))) |
32 | | fmla0 32915 |
. . . . . . . . . . . 12
⊢
(Fmla‘∅) = {𝑥 ∈ V ∣ ∃𝑘 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑘∈𝑔𝑗)} |
33 | 31, 32 | elrab2 3591 |
. . . . . . . . . . 11
⊢
(∀𝑔𝑖𝑎 ∈ (Fmla‘∅) ↔
(∀𝑔𝑖𝑎 ∈ V ∧ ∃𝑘 ∈ ω ∃𝑗 ∈ ω
∀𝑔𝑖𝑎 = (𝑘∈𝑔𝑗))) |
34 | 25 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ω ∧ 𝑗 ∈ ω) →
∀𝑔𝑖𝑎 = 〈2o, 〈𝑖, 𝑎〉〉) |
35 | | goel 32880 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ω ∧ 𝑗 ∈ ω) → (𝑘∈𝑔𝑗) = 〈∅, 〈𝑘, 𝑗〉〉) |
36 | 34, 35 | eqeq12d 2754 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ω ∧ 𝑗 ∈ ω) →
(∀𝑔𝑖𝑎 = (𝑘∈𝑔𝑗) ↔ 〈2o, 〈𝑖, 𝑎〉〉 = 〈∅, 〈𝑘, 𝑗〉〉)) |
37 | | 2oex 8148 |
. . . . . . . . . . . . . . . 16
⊢
2o ∈ V |
38 | | opex 5322 |
. . . . . . . . . . . . . . . 16
⊢
〈𝑖, 𝑎〉 ∈ V |
39 | 37, 38 | opth 5334 |
. . . . . . . . . . . . . . 15
⊢
(〈2o, 〈𝑖, 𝑎〉〉 = 〈∅, 〈𝑘, 𝑗〉〉 ↔ (2o = ∅
∧ 〈𝑖, 𝑎〉 = 〈𝑘, 𝑗〉)) |
40 | | 2on0 8140 |
. . . . . . . . . . . . . . . . 17
⊢
2o ≠ ∅ |
41 | | eqneqall 2945 |
. . . . . . . . . . . . . . . . 17
⊢
(2o = ∅ → (2o ≠ ∅ → 𝑎 ∈ (Fmla‘suc
∅))) |
42 | 40, 41 | mpi 20 |
. . . . . . . . . . . . . . . 16
⊢
(2o = ∅ → 𝑎 ∈ (Fmla‘suc
∅)) |
43 | 42 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢
((2o = ∅ ∧ 〈𝑖, 𝑎〉 = 〈𝑘, 𝑗〉) → 𝑎 ∈ (Fmla‘suc
∅)) |
44 | 39, 43 | sylbi 220 |
. . . . . . . . . . . . . 14
⊢
(〈2o, 〈𝑖, 𝑎〉〉 = 〈∅, 〈𝑘, 𝑗〉〉 → 𝑎 ∈ (Fmla‘suc
∅)) |
45 | 36, 44 | syl6bi 256 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ω ∧ 𝑗 ∈ ω) →
(∀𝑔𝑖𝑎 = (𝑘∈𝑔𝑗) → 𝑎 ∈ (Fmla‘suc
∅))) |
46 | 45 | rexlimdva 3194 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ω →
(∃𝑗 ∈ ω
∀𝑔𝑖𝑎 = (𝑘∈𝑔𝑗) → 𝑎 ∈ (Fmla‘suc
∅))) |
47 | 46 | rexlimiv 3190 |
. . . . . . . . . . 11
⊢
(∃𝑘 ∈
ω ∃𝑗 ∈
ω ∀𝑔𝑖𝑎 = (𝑘∈𝑔𝑗) → 𝑎 ∈ (Fmla‘suc
∅)) |
48 | 33, 47 | simplbiim 508 |
. . . . . . . . . 10
⊢
(∀𝑔𝑖𝑎 ∈ (Fmla‘∅) → 𝑎 ∈ (Fmla‘suc
∅)) |
49 | | gonanegoal 32885 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢⊼𝑔𝑣) ≠
∀𝑔𝑖𝑎 |
50 | | eqneqall 2945 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢⊼𝑔𝑣) =
∀𝑔𝑖𝑎 → ((𝑢⊼𝑔𝑣) ≠ ∀𝑔𝑖𝑎 → 𝑎 ∈ (Fmla‘suc
∅))) |
51 | 49, 50 | mpi 20 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢⊼𝑔𝑣) =
∀𝑔𝑖𝑎 → 𝑎 ∈ (Fmla‘suc
∅)) |
52 | 51 | eqcoms 2746 |
. . . . . . . . . . . . . 14
⊢
(∀𝑔𝑖𝑎 = (𝑢⊼𝑔𝑣) → 𝑎 ∈ (Fmla‘suc
∅)) |
53 | 52 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∈ (Fmla‘∅)
∧ 𝑣 ∈
(Fmla‘∅)) → (∀𝑔𝑖𝑎 = (𝑢⊼𝑔𝑣) → 𝑎 ∈ (Fmla‘suc
∅))) |
54 | 53 | rexlimdva 3194 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ (Fmla‘∅)
→ (∃𝑣 ∈
(Fmla‘∅)∀𝑔𝑖𝑎 = (𝑢⊼𝑔𝑣) → 𝑎 ∈ (Fmla‘suc
∅))) |
55 | | df-goal 32875 |
. . . . . . . . . . . . . . 15
⊢
∀𝑔𝑘𝑢 = 〈2o, 〈𝑘, 𝑢〉〉 |
56 | 25, 55 | eqeq12i 2753 |
. . . . . . . . . . . . . 14
⊢
(∀𝑔𝑖𝑎 = ∀𝑔𝑘𝑢 ↔ 〈2o, 〈𝑖, 𝑎〉〉 = 〈2o,
〈𝑘, 𝑢〉〉) |
57 | 37, 38 | opth 5334 |
. . . . . . . . . . . . . . . . 17
⊢
(〈2o, 〈𝑖, 𝑎〉〉 = 〈2o,
〈𝑘, 𝑢〉〉 ↔ (2o =
2o ∧ 〈𝑖, 𝑎〉 = 〈𝑘, 𝑢〉)) |
58 | | vex 3402 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑖 ∈ V |
59 | | vex 3402 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑎 ∈ V |
60 | 58, 59 | opth 5334 |
. . . . . . . . . . . . . . . . . 18
⊢
(〈𝑖, 𝑎〉 = 〈𝑘, 𝑢〉 ↔ (𝑖 = 𝑘 ∧ 𝑎 = 𝑢)) |
61 | | eleq1w 2815 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑢 = 𝑎 → (𝑢 ∈ (Fmla‘∅) ↔ 𝑎 ∈
(Fmla‘∅))) |
62 | | fmlasssuc 32922 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (∅
∈ ω → (Fmla‘∅) ⊆ (Fmla‘suc
∅)) |
63 | 24, 62 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(Fmla‘∅) ⊆ (Fmla‘suc ∅) |
64 | 63 | sseli 3873 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 ∈ (Fmla‘∅)
→ 𝑎 ∈
(Fmla‘suc ∅)) |
65 | 61, 64 | syl6bi 256 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 = 𝑎 → (𝑢 ∈ (Fmla‘∅) → 𝑎 ∈ (Fmla‘suc
∅))) |
66 | 65 | eqcoms 2746 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = 𝑢 → (𝑢 ∈ (Fmla‘∅) → 𝑎 ∈ (Fmla‘suc
∅))) |
67 | 60, 66 | simplbiim 508 |
. . . . . . . . . . . . . . . . 17
⊢
(〈𝑖, 𝑎〉 = 〈𝑘, 𝑢〉 → (𝑢 ∈ (Fmla‘∅) → 𝑎 ∈ (Fmla‘suc
∅))) |
68 | 57, 67 | simplbiim 508 |
. . . . . . . . . . . . . . . 16
⊢
(〈2o, 〈𝑖, 𝑎〉〉 = 〈2o,
〈𝑘, 𝑢〉〉 → (𝑢 ∈ (Fmla‘∅) → 𝑎 ∈ (Fmla‘suc
∅))) |
69 | 68 | com12 32 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ (Fmla‘∅)
→ (〈2o, 〈𝑖, 𝑎〉〉 = 〈2o,
〈𝑘, 𝑢〉〉 → 𝑎 ∈ (Fmla‘suc
∅))) |
70 | 69 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ (Fmla‘∅)
∧ 𝑘 ∈ ω)
→ (〈2o, 〈𝑖, 𝑎〉〉 = 〈2o,
〈𝑘, 𝑢〉〉 → 𝑎 ∈ (Fmla‘suc
∅))) |
71 | 56, 70 | syl5bi 245 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∈ (Fmla‘∅)
∧ 𝑘 ∈ ω)
→ (∀𝑔𝑖𝑎 = ∀𝑔𝑘𝑢 → 𝑎 ∈ (Fmla‘suc
∅))) |
72 | 71 | rexlimdva 3194 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ (Fmla‘∅)
→ (∃𝑘 ∈
ω ∀𝑔𝑖𝑎 = ∀𝑔𝑘𝑢 → 𝑎 ∈ (Fmla‘suc
∅))) |
73 | 54, 72 | jaod 858 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (Fmla‘∅)
→ ((∃𝑣 ∈
(Fmla‘∅)∀𝑔𝑖𝑎 = (𝑢⊼𝑔𝑣) ∨ ∃𝑘 ∈ ω
∀𝑔𝑖𝑎 = ∀𝑔𝑘𝑢) → 𝑎 ∈ (Fmla‘suc
∅))) |
74 | 73 | rexlimiv 3190 |
. . . . . . . . . 10
⊢
(∃𝑢 ∈
(Fmla‘∅)(∃𝑣 ∈
(Fmla‘∅)∀𝑔𝑖𝑎 = (𝑢⊼𝑔𝑣) ∨ ∃𝑘 ∈ ω
∀𝑔𝑖𝑎 = ∀𝑔𝑘𝑢) → 𝑎 ∈ (Fmla‘suc
∅)) |
75 | 48, 74 | jaoi 856 |
. . . . . . . . 9
⊢
((∀𝑔𝑖𝑎 ∈ (Fmla‘∅) ∨
∃𝑢 ∈
(Fmla‘∅)(∃𝑣 ∈
(Fmla‘∅)∀𝑔𝑖𝑎 = (𝑢⊼𝑔𝑣) ∨ ∃𝑘 ∈ ω
∀𝑔𝑖𝑎 = ∀𝑔𝑘𝑢)) → 𝑎 ∈ (Fmla‘suc
∅)) |
76 | 29, 75 | sylbi 220 |
. . . . . . . 8
⊢
(∀𝑔𝑖𝑎 ∈ (Fmla‘suc ∅) → 𝑎 ∈ (Fmla‘suc
∅)) |
77 | | goalrlem 32929 |
. . . . . . . 8
⊢ (𝑦 ∈ ω →
((∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑦) → 𝑎 ∈ (Fmla‘suc 𝑦)) → (∀𝑔𝑖𝑎 ∈ (Fmla‘suc suc 𝑦) → 𝑎 ∈ (Fmla‘suc suc 𝑦)))) |
78 | 8, 13, 18, 23, 76, 77 | finds 7629 |
. . . . . . 7
⊢ (𝑛 ∈ ω →
(∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑛) → 𝑎 ∈ (Fmla‘suc 𝑛))) |
79 | 78 | adantr 484 |
. . . . . 6
⊢ ((𝑛 ∈ ω ∧ 𝑁 = suc 𝑛) → (∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑛) → 𝑎 ∈ (Fmla‘suc 𝑛))) |
80 | | fveq2 6674 |
. . . . . . . . 9
⊢ (𝑁 = suc 𝑛 → (Fmla‘𝑁) = (Fmla‘suc 𝑛)) |
81 | 80 | eleq2d 2818 |
. . . . . . . 8
⊢ (𝑁 = suc 𝑛 → (∀𝑔𝑖𝑎 ∈ (Fmla‘𝑁) ↔ ∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑛))) |
82 | 80 | eleq2d 2818 |
. . . . . . . 8
⊢ (𝑁 = suc 𝑛 → (𝑎 ∈ (Fmla‘𝑁) ↔ 𝑎 ∈ (Fmla‘suc 𝑛))) |
83 | 81, 82 | imbi12d 348 |
. . . . . . 7
⊢ (𝑁 = suc 𝑛 → ((∀𝑔𝑖𝑎 ∈ (Fmla‘𝑁) → 𝑎 ∈ (Fmla‘𝑁)) ↔ (∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑛) → 𝑎 ∈ (Fmla‘suc 𝑛)))) |
84 | 83 | adantl 485 |
. . . . . 6
⊢ ((𝑛 ∈ ω ∧ 𝑁 = suc 𝑛) → ((∀𝑔𝑖𝑎 ∈ (Fmla‘𝑁) → 𝑎 ∈ (Fmla‘𝑁)) ↔ (∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑛) → 𝑎 ∈ (Fmla‘suc 𝑛)))) |
85 | 79, 84 | mpbird 260 |
. . . . 5
⊢ ((𝑛 ∈ ω ∧ 𝑁 = suc 𝑛) → (∀𝑔𝑖𝑎 ∈ (Fmla‘𝑁) → 𝑎 ∈ (Fmla‘𝑁))) |
86 | 85 | rexlimiva 3191 |
. . . 4
⊢
(∃𝑛 ∈
ω 𝑁 = suc 𝑛 →
(∀𝑔𝑖𝑎 ∈ (Fmla‘𝑁) → 𝑎 ∈ (Fmla‘𝑁))) |
87 | 3, 86 | syl 17 |
. . 3
⊢ ((𝑁 ∈ ω ∧ 𝑁 ≠ ∅) →
(∀𝑔𝑖𝑎 ∈ (Fmla‘𝑁) → 𝑎 ∈ (Fmla‘𝑁))) |
88 | 87 | impancom 455 |
. 2
⊢ ((𝑁 ∈ ω ∧
∀𝑔𝑖𝑎 ∈ (Fmla‘𝑁)) → (𝑁 ≠ ∅ → 𝑎 ∈ (Fmla‘𝑁))) |
89 | 2, 88 | mpd 15 |
1
⊢ ((𝑁 ∈ ω ∧
∀𝑔𝑖𝑎 ∈ (Fmla‘𝑁)) → 𝑎 ∈ (Fmla‘𝑁)) |