| Step | Hyp | Ref
| Expression |
| 1 | | fveq2 6906 |
. . . . 5
⊢ (𝑥 = ∅ →
(Fmla‘𝑥) =
(Fmla‘∅)) |
| 2 | 1 | eleq2d 2827 |
. . . 4
⊢ (𝑥 = ∅ → (∅
∈ (Fmla‘𝑥)
↔ ∅ ∈ (Fmla‘∅))) |
| 3 | 2 | notbid 318 |
. . 3
⊢ (𝑥 = ∅ → (¬ ∅
∈ (Fmla‘𝑥)
↔ ¬ ∅ ∈ (Fmla‘∅))) |
| 4 | | fveq2 6906 |
. . . . 5
⊢ (𝑥 = 𝑦 → (Fmla‘𝑥) = (Fmla‘𝑦)) |
| 5 | 4 | eleq2d 2827 |
. . . 4
⊢ (𝑥 = 𝑦 → (∅ ∈ (Fmla‘𝑥) ↔ ∅ ∈
(Fmla‘𝑦))) |
| 6 | 5 | notbid 318 |
. . 3
⊢ (𝑥 = 𝑦 → (¬ ∅ ∈
(Fmla‘𝑥) ↔ ¬
∅ ∈ (Fmla‘𝑦))) |
| 7 | | fveq2 6906 |
. . . . 5
⊢ (𝑥 = suc 𝑦 → (Fmla‘𝑥) = (Fmla‘suc 𝑦)) |
| 8 | 7 | eleq2d 2827 |
. . . 4
⊢ (𝑥 = suc 𝑦 → (∅ ∈ (Fmla‘𝑥) ↔ ∅ ∈
(Fmla‘suc 𝑦))) |
| 9 | 8 | notbid 318 |
. . 3
⊢ (𝑥 = suc 𝑦 → (¬ ∅ ∈
(Fmla‘𝑥) ↔ ¬
∅ ∈ (Fmla‘suc 𝑦))) |
| 10 | | fveq2 6906 |
. . . . 5
⊢ (𝑥 = 𝑁 → (Fmla‘𝑥) = (Fmla‘𝑁)) |
| 11 | 10 | eleq2d 2827 |
. . . 4
⊢ (𝑥 = 𝑁 → (∅ ∈ (Fmla‘𝑥) ↔ ∅ ∈
(Fmla‘𝑁))) |
| 12 | 11 | notbid 318 |
. . 3
⊢ (𝑥 = 𝑁 → (¬ ∅ ∈
(Fmla‘𝑥) ↔ ¬
∅ ∈ (Fmla‘𝑁))) |
| 13 | | 0ex 5307 |
. . . . . . . . . . . 12
⊢ ∅
∈ V |
| 14 | | opex 5469 |
. . . . . . . . . . . 12
⊢
〈𝑖, 𝑗〉 ∈ V |
| 15 | 13, 14 | pm3.2i 470 |
. . . . . . . . . . 11
⊢ (∅
∈ V ∧ 〈𝑖,
𝑗〉 ∈
V) |
| 16 | 15 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (∅
∈ V ∧ 〈𝑖,
𝑗〉 ∈
V)) |
| 17 | | necom 2994 |
. . . . . . . . . . 11
⊢ (∅
≠ 〈∅, 〈𝑖, 𝑗〉〉 ↔ 〈∅,
〈𝑖, 𝑗〉〉 ≠ ∅) |
| 18 | | opnz 5478 |
. . . . . . . . . . 11
⊢
(〈∅, 〈𝑖, 𝑗〉〉 ≠ ∅ ↔ (∅
∈ V ∧ 〈𝑖,
𝑗〉 ∈
V)) |
| 19 | 17, 18 | bitri 275 |
. . . . . . . . . 10
⊢ (∅
≠ 〈∅, 〈𝑖, 𝑗〉〉 ↔ (∅ ∈ V ∧
〈𝑖, 𝑗〉 ∈ V)) |
| 20 | 16, 19 | sylibr 234 |
. . . . . . . . 9
⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ∅
≠ 〈∅, 〈𝑖, 𝑗〉〉) |
| 21 | 20 | neneqd 2945 |
. . . . . . . 8
⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ¬
∅ = 〈∅, 〈𝑖, 𝑗〉〉) |
| 22 | | goel 35352 |
. . . . . . . . 9
⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (𝑖∈𝑔𝑗) = 〈∅, 〈𝑖, 𝑗〉〉) |
| 23 | 22 | eqeq2d 2748 |
. . . . . . . 8
⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (∅
= (𝑖∈𝑔𝑗) ↔ ∅ = 〈∅, 〈𝑖, 𝑗〉〉)) |
| 24 | 21, 23 | mtbird 325 |
. . . . . . 7
⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ¬
∅ = (𝑖∈𝑔𝑗)) |
| 25 | 24 | rgen2 3199 |
. . . . . 6
⊢
∀𝑖 ∈
ω ∀𝑗 ∈
ω ¬ ∅ = (𝑖∈𝑔𝑗) |
| 26 | | ralnex2 3133 |
. . . . . 6
⊢
(∀𝑖 ∈
ω ∀𝑗 ∈
ω ¬ ∅ = (𝑖∈𝑔𝑗) ↔ ¬ ∃𝑖 ∈ ω ∃𝑗 ∈ ω ∅ = (𝑖∈𝑔𝑗)) |
| 27 | 25, 26 | mpbi 230 |
. . . . 5
⊢ ¬
∃𝑖 ∈ ω
∃𝑗 ∈ ω
∅ = (𝑖∈𝑔𝑗) |
| 28 | 27 | intnan 486 |
. . . 4
⊢ ¬
(∅ ∈ V ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω ∅ = (𝑖∈𝑔𝑗)) |
| 29 | | fmla0 35387 |
. . . . . 6
⊢
(Fmla‘∅) = {𝑥 ∈ V ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)} |
| 30 | 29 | eleq2i 2833 |
. . . . 5
⊢ (∅
∈ (Fmla‘∅) ↔ ∅ ∈ {𝑥 ∈ V ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)}) |
| 31 | | eqeq1 2741 |
. . . . . . 7
⊢ (𝑥 = ∅ → (𝑥 = (𝑖∈𝑔𝑗) ↔ ∅ = (𝑖∈𝑔𝑗))) |
| 32 | 31 | 2rexbidv 3222 |
. . . . . 6
⊢ (𝑥 = ∅ → (∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω ∅ = (𝑖∈𝑔𝑗))) |
| 33 | 32 | elrab 3692 |
. . . . 5
⊢ (∅
∈ {𝑥 ∈ V ∣
∃𝑖 ∈ ω
∃𝑗 ∈ ω
𝑥 = (𝑖∈𝑔𝑗)} ↔ (∅ ∈ V ∧
∃𝑖 ∈ ω
∃𝑗 ∈ ω
∅ = (𝑖∈𝑔𝑗))) |
| 34 | 30, 33 | bitri 275 |
. . . 4
⊢ (∅
∈ (Fmla‘∅) ↔ (∅ ∈ V ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω ∅ = (𝑖∈𝑔𝑗))) |
| 35 | 28, 34 | mtbir 323 |
. . 3
⊢ ¬
∅ ∈ (Fmla‘∅) |
| 36 | | simpr 484 |
. . . . . 6
⊢ ((𝑦 ∈ ω ∧ ¬
∅ ∈ (Fmla‘𝑦)) → ¬ ∅ ∈
(Fmla‘𝑦)) |
| 37 | | 1oex 8516 |
. . . . . . . . . . . . . 14
⊢
1o ∈ V |
| 38 | | opex 5469 |
. . . . . . . . . . . . . 14
⊢
〈𝑢, 𝑣〉 ∈ V |
| 39 | 37, 38 | opnzi 5479 |
. . . . . . . . . . . . 13
⊢
〈1o, 〈𝑢, 𝑣〉〉 ≠ ∅ |
| 40 | 39 | nesymi 2998 |
. . . . . . . . . . . 12
⊢ ¬
∅ = 〈1o, 〈𝑢, 𝑣〉〉 |
| 41 | | gonafv 35355 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ (Fmla‘𝑦) ∧ 𝑣 ∈ (Fmla‘𝑦)) → (𝑢⊼𝑔𝑣) = 〈1o, 〈𝑢, 𝑣〉〉) |
| 42 | 41 | adantll 714 |
. . . . . . . . . . . . 13
⊢ (((𝑦 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑦)) ∧ 𝑣 ∈ (Fmla‘𝑦)) → (𝑢⊼𝑔𝑣) = 〈1o, 〈𝑢, 𝑣〉〉) |
| 43 | 42 | eqeq2d 2748 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑦)) ∧ 𝑣 ∈ (Fmla‘𝑦)) → (∅ = (𝑢⊼𝑔𝑣) ↔ ∅ = 〈1o,
〈𝑢, 𝑣〉〉)) |
| 44 | 40, 43 | mtbiri 327 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑦)) ∧ 𝑣 ∈ (Fmla‘𝑦)) → ¬ ∅ = (𝑢⊼𝑔𝑣)) |
| 45 | 44 | ralrimiva 3146 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑦)) → ∀𝑣 ∈ (Fmla‘𝑦) ¬ ∅ = (𝑢⊼𝑔𝑣)) |
| 46 | | 2oex 8517 |
. . . . . . . . . . . . . . 15
⊢
2o ∈ V |
| 47 | | opex 5469 |
. . . . . . . . . . . . . . 15
⊢
〈𝑖, 𝑢〉 ∈ V |
| 48 | 46, 47 | opnzi 5479 |
. . . . . . . . . . . . . 14
⊢
〈2o, 〈𝑖, 𝑢〉〉 ≠ ∅ |
| 49 | 48 | nesymi 2998 |
. . . . . . . . . . . . 13
⊢ ¬
∅ = 〈2o, 〈𝑖, 𝑢〉〉 |
| 50 | | df-goal 35347 |
. . . . . . . . . . . . . 14
⊢
∀𝑔𝑖𝑢 = 〈2o, 〈𝑖, 𝑢〉〉 |
| 51 | 50 | eqeq2i 2750 |
. . . . . . . . . . . . 13
⊢ (∅
= ∀𝑔𝑖𝑢 ↔ ∅ = 〈2o,
〈𝑖, 𝑢〉〉) |
| 52 | 49, 51 | mtbir 323 |
. . . . . . . . . . . 12
⊢ ¬
∅ = ∀𝑔𝑖𝑢 |
| 53 | 52 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑦)) ∧ 𝑖 ∈ ω) → ¬ ∅ =
∀𝑔𝑖𝑢) |
| 54 | 53 | ralrimiva 3146 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑦)) → ∀𝑖 ∈ ω ¬ ∅ =
∀𝑔𝑖𝑢) |
| 55 | 45, 54 | jca 511 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑦)) → (∀𝑣 ∈ (Fmla‘𝑦) ¬ ∅ = (𝑢⊼𝑔𝑣) ∧ ∀𝑖 ∈ ω ¬ ∅ =
∀𝑔𝑖𝑢)) |
| 56 | 55 | ralrimiva 3146 |
. . . . . . . 8
⊢ (𝑦 ∈ ω →
∀𝑢 ∈
(Fmla‘𝑦)(∀𝑣 ∈ (Fmla‘𝑦) ¬ ∅ = (𝑢⊼𝑔𝑣) ∧ ∀𝑖 ∈ ω ¬ ∅ =
∀𝑔𝑖𝑢)) |
| 57 | 56 | adantr 480 |
. . . . . . 7
⊢ ((𝑦 ∈ ω ∧ ¬
∅ ∈ (Fmla‘𝑦)) → ∀𝑢 ∈ (Fmla‘𝑦)(∀𝑣 ∈ (Fmla‘𝑦) ¬ ∅ = (𝑢⊼𝑔𝑣) ∧ ∀𝑖 ∈ ω ¬ ∅ =
∀𝑔𝑖𝑢)) |
| 58 | | ralnex 3072 |
. . . . . . . . . . 11
⊢
(∀𝑣 ∈
(Fmla‘𝑦) ¬
∅ = (𝑢⊼𝑔𝑣) ↔ ¬ ∃𝑣 ∈ (Fmla‘𝑦)∅ = (𝑢⊼𝑔𝑣)) |
| 59 | | ralnex 3072 |
. . . . . . . . . . 11
⊢
(∀𝑖 ∈
ω ¬ ∅ = ∀𝑔𝑖𝑢 ↔ ¬ ∃𝑖 ∈ ω ∅ =
∀𝑔𝑖𝑢) |
| 60 | 58, 59 | anbi12i 628 |
. . . . . . . . . 10
⊢
((∀𝑣 ∈
(Fmla‘𝑦) ¬
∅ = (𝑢⊼𝑔𝑣) ∧ ∀𝑖 ∈ ω ¬ ∅ =
∀𝑔𝑖𝑢) ↔ (¬ ∃𝑣 ∈ (Fmla‘𝑦)∅ = (𝑢⊼𝑔𝑣) ∧ ¬ ∃𝑖 ∈ ω ∅ =
∀𝑔𝑖𝑢)) |
| 61 | | ioran 986 |
. . . . . . . . . 10
⊢ (¬
(∃𝑣 ∈
(Fmla‘𝑦)∅ =
(𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω ∅ =
∀𝑔𝑖𝑢) ↔ (¬ ∃𝑣 ∈ (Fmla‘𝑦)∅ = (𝑢⊼𝑔𝑣) ∧ ¬ ∃𝑖 ∈ ω ∅ =
∀𝑔𝑖𝑢)) |
| 62 | 60, 61 | bitr4i 278 |
. . . . . . . . 9
⊢
((∀𝑣 ∈
(Fmla‘𝑦) ¬
∅ = (𝑢⊼𝑔𝑣) ∧ ∀𝑖 ∈ ω ¬ ∅ =
∀𝑔𝑖𝑢) ↔ ¬ (∃𝑣 ∈ (Fmla‘𝑦)∅ = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω ∅ =
∀𝑔𝑖𝑢)) |
| 63 | 62 | ralbii 3093 |
. . . . . . . 8
⊢
(∀𝑢 ∈
(Fmla‘𝑦)(∀𝑣 ∈ (Fmla‘𝑦) ¬ ∅ = (𝑢⊼𝑔𝑣) ∧ ∀𝑖 ∈ ω ¬ ∅ =
∀𝑔𝑖𝑢) ↔ ∀𝑢 ∈ (Fmla‘𝑦) ¬ (∃𝑣 ∈ (Fmla‘𝑦)∅ = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω ∅ =
∀𝑔𝑖𝑢)) |
| 64 | | ralnex 3072 |
. . . . . . . 8
⊢
(∀𝑢 ∈
(Fmla‘𝑦) ¬
(∃𝑣 ∈
(Fmla‘𝑦)∅ =
(𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω ∅ =
∀𝑔𝑖𝑢) ↔ ¬ ∃𝑢 ∈ (Fmla‘𝑦)(∃𝑣 ∈ (Fmla‘𝑦)∅ = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω ∅ =
∀𝑔𝑖𝑢)) |
| 65 | 63, 64 | bitri 275 |
. . . . . . 7
⊢
(∀𝑢 ∈
(Fmla‘𝑦)(∀𝑣 ∈ (Fmla‘𝑦) ¬ ∅ = (𝑢⊼𝑔𝑣) ∧ ∀𝑖 ∈ ω ¬ ∅ =
∀𝑔𝑖𝑢) ↔ ¬ ∃𝑢 ∈ (Fmla‘𝑦)(∃𝑣 ∈ (Fmla‘𝑦)∅ = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω ∅ =
∀𝑔𝑖𝑢)) |
| 66 | 57, 65 | sylib 218 |
. . . . . 6
⊢ ((𝑦 ∈ ω ∧ ¬
∅ ∈ (Fmla‘𝑦)) → ¬ ∃𝑢 ∈ (Fmla‘𝑦)(∃𝑣 ∈ (Fmla‘𝑦)∅ = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω ∅ =
∀𝑔𝑖𝑢)) |
| 67 | | ioran 986 |
. . . . . 6
⊢ (¬
(∅ ∈ (Fmla‘𝑦) ∨ ∃𝑢 ∈ (Fmla‘𝑦)(∃𝑣 ∈ (Fmla‘𝑦)∅ = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω ∅ =
∀𝑔𝑖𝑢)) ↔ (¬ ∅ ∈
(Fmla‘𝑦) ∧ ¬
∃𝑢 ∈
(Fmla‘𝑦)(∃𝑣 ∈ (Fmla‘𝑦)∅ = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω ∅ =
∀𝑔𝑖𝑢))) |
| 68 | 36, 66, 67 | sylanbrc 583 |
. . . . 5
⊢ ((𝑦 ∈ ω ∧ ¬
∅ ∈ (Fmla‘𝑦)) → ¬ (∅ ∈
(Fmla‘𝑦) ∨
∃𝑢 ∈
(Fmla‘𝑦)(∃𝑣 ∈ (Fmla‘𝑦)∅ = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω ∅ =
∀𝑔𝑖𝑢))) |
| 69 | | fmlasuc 35391 |
. . . . . . . 8
⊢ (𝑦 ∈ ω →
(Fmla‘suc 𝑦) =
((Fmla‘𝑦) ∪
{𝑥 ∣ ∃𝑢 ∈ (Fmla‘𝑦)(∃𝑣 ∈ (Fmla‘𝑦)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)})) |
| 70 | 69 | eleq2d 2827 |
. . . . . . 7
⊢ (𝑦 ∈ ω → (∅
∈ (Fmla‘suc 𝑦)
↔ ∅ ∈ ((Fmla‘𝑦) ∪ {𝑥 ∣ ∃𝑢 ∈ (Fmla‘𝑦)(∃𝑣 ∈ (Fmla‘𝑦)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)}))) |
| 71 | | elun 4153 |
. . . . . . . 8
⊢ (∅
∈ ((Fmla‘𝑦)
∪ {𝑥 ∣
∃𝑢 ∈
(Fmla‘𝑦)(∃𝑣 ∈ (Fmla‘𝑦)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)}) ↔ (∅ ∈ (Fmla‘𝑦) ∨ ∅ ∈ {𝑥 ∣ ∃𝑢 ∈ (Fmla‘𝑦)(∃𝑣 ∈ (Fmla‘𝑦)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)})) |
| 72 | | eqeq1 2741 |
. . . . . . . . . . . . 13
⊢ (𝑥 = ∅ → (𝑥 = (𝑢⊼𝑔𝑣) ↔ ∅ = (𝑢⊼𝑔𝑣))) |
| 73 | 72 | rexbidv 3179 |
. . . . . . . . . . . 12
⊢ (𝑥 = ∅ → (∃𝑣 ∈ (Fmla‘𝑦)𝑥 = (𝑢⊼𝑔𝑣) ↔ ∃𝑣 ∈ (Fmla‘𝑦)∅ = (𝑢⊼𝑔𝑣))) |
| 74 | | eqeq1 2741 |
. . . . . . . . . . . . 13
⊢ (𝑥 = ∅ → (𝑥 =
∀𝑔𝑖𝑢 ↔ ∅ =
∀𝑔𝑖𝑢)) |
| 75 | 74 | rexbidv 3179 |
. . . . . . . . . . . 12
⊢ (𝑥 = ∅ → (∃𝑖 ∈ ω 𝑥 =
∀𝑔𝑖𝑢 ↔ ∃𝑖 ∈ ω ∅ =
∀𝑔𝑖𝑢)) |
| 76 | 73, 75 | orbi12d 919 |
. . . . . . . . . . 11
⊢ (𝑥 = ∅ → ((∃𝑣 ∈ (Fmla‘𝑦)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) ↔ (∃𝑣 ∈ (Fmla‘𝑦)∅ = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω ∅ =
∀𝑔𝑖𝑢))) |
| 77 | 76 | rexbidv 3179 |
. . . . . . . . . 10
⊢ (𝑥 = ∅ → (∃𝑢 ∈ (Fmla‘𝑦)(∃𝑣 ∈ (Fmla‘𝑦)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) ↔ ∃𝑢 ∈ (Fmla‘𝑦)(∃𝑣 ∈ (Fmla‘𝑦)∅ = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω ∅ =
∀𝑔𝑖𝑢))) |
| 78 | 13, 77 | elab 3679 |
. . . . . . . . 9
⊢ (∅
∈ {𝑥 ∣
∃𝑢 ∈
(Fmla‘𝑦)(∃𝑣 ∈ (Fmla‘𝑦)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)} ↔ ∃𝑢 ∈ (Fmla‘𝑦)(∃𝑣 ∈ (Fmla‘𝑦)∅ = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω ∅ =
∀𝑔𝑖𝑢)) |
| 79 | 78 | orbi2i 913 |
. . . . . . . 8
⊢ ((∅
∈ (Fmla‘𝑦) ∨
∅ ∈ {𝑥 ∣
∃𝑢 ∈
(Fmla‘𝑦)(∃𝑣 ∈ (Fmla‘𝑦)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)}) ↔ (∅ ∈ (Fmla‘𝑦) ∨ ∃𝑢 ∈ (Fmla‘𝑦)(∃𝑣 ∈ (Fmla‘𝑦)∅ = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω ∅ =
∀𝑔𝑖𝑢))) |
| 80 | 71, 79 | bitri 275 |
. . . . . . 7
⊢ (∅
∈ ((Fmla‘𝑦)
∪ {𝑥 ∣
∃𝑢 ∈
(Fmla‘𝑦)(∃𝑣 ∈ (Fmla‘𝑦)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)}) ↔ (∅ ∈ (Fmla‘𝑦) ∨ ∃𝑢 ∈ (Fmla‘𝑦)(∃𝑣 ∈ (Fmla‘𝑦)∅ = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω ∅ =
∀𝑔𝑖𝑢))) |
| 81 | 70, 80 | bitrdi 287 |
. . . . . 6
⊢ (𝑦 ∈ ω → (∅
∈ (Fmla‘suc 𝑦)
↔ (∅ ∈ (Fmla‘𝑦) ∨ ∃𝑢 ∈ (Fmla‘𝑦)(∃𝑣 ∈ (Fmla‘𝑦)∅ = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω ∅ =
∀𝑔𝑖𝑢)))) |
| 82 | 81 | adantr 480 |
. . . . 5
⊢ ((𝑦 ∈ ω ∧ ¬
∅ ∈ (Fmla‘𝑦)) → (∅ ∈ (Fmla‘suc
𝑦) ↔ (∅ ∈
(Fmla‘𝑦) ∨
∃𝑢 ∈
(Fmla‘𝑦)(∃𝑣 ∈ (Fmla‘𝑦)∅ = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω ∅ =
∀𝑔𝑖𝑢)))) |
| 83 | 68, 82 | mtbird 325 |
. . . 4
⊢ ((𝑦 ∈ ω ∧ ¬
∅ ∈ (Fmla‘𝑦)) → ¬ ∅ ∈
(Fmla‘suc 𝑦)) |
| 84 | 83 | ex 412 |
. . 3
⊢ (𝑦 ∈ ω → (¬
∅ ∈ (Fmla‘𝑦) → ¬ ∅ ∈ (Fmla‘suc
𝑦))) |
| 85 | 3, 6, 9, 12, 35, 84 | finds 7918 |
. 2
⊢ (𝑁 ∈ ω → ¬
∅ ∈ (Fmla‘𝑁)) |
| 86 | | df-nel 3047 |
. 2
⊢ (∅
∉ (Fmla‘𝑁)
↔ ¬ ∅ ∈ (Fmla‘𝑁)) |
| 87 | 85, 86 | sylibr 234 |
1
⊢ (𝑁 ∈ ω → ∅
∉ (Fmla‘𝑁)) |