Mathbox for Mario Carneiro < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fmlaomn0 Structured version   Visualization version   GIF version

Theorem fmlaomn0 32880
 Description: The empty set is not a Godel formula of any height. (Contributed by AV, 21-Oct-2023.)
Assertion
Ref Expression
fmlaomn0 (𝑁 ∈ ω → ∅ ∉ (Fmla‘𝑁))

Proof of Theorem fmlaomn0
Dummy variables 𝑥 𝑖 𝑗 𝑢 𝑣 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq2 6663 . . . . 5 (𝑥 = ∅ → (Fmla‘𝑥) = (Fmla‘∅))
21eleq2d 2837 . . . 4 (𝑥 = ∅ → (∅ ∈ (Fmla‘𝑥) ↔ ∅ ∈ (Fmla‘∅)))
32notbid 321 . . 3 (𝑥 = ∅ → (¬ ∅ ∈ (Fmla‘𝑥) ↔ ¬ ∅ ∈ (Fmla‘∅)))
4 fveq2 6663 . . . . 5 (𝑥 = 𝑦 → (Fmla‘𝑥) = (Fmla‘𝑦))
54eleq2d 2837 . . . 4 (𝑥 = 𝑦 → (∅ ∈ (Fmla‘𝑥) ↔ ∅ ∈ (Fmla‘𝑦)))
65notbid 321 . . 3 (𝑥 = 𝑦 → (¬ ∅ ∈ (Fmla‘𝑥) ↔ ¬ ∅ ∈ (Fmla‘𝑦)))
7 fveq2 6663 . . . . 5 (𝑥 = suc 𝑦 → (Fmla‘𝑥) = (Fmla‘suc 𝑦))
87eleq2d 2837 . . . 4 (𝑥 = suc 𝑦 → (∅ ∈ (Fmla‘𝑥) ↔ ∅ ∈ (Fmla‘suc 𝑦)))
98notbid 321 . . 3 (𝑥 = suc 𝑦 → (¬ ∅ ∈ (Fmla‘𝑥) ↔ ¬ ∅ ∈ (Fmla‘suc 𝑦)))
10 fveq2 6663 . . . . 5 (𝑥 = 𝑁 → (Fmla‘𝑥) = (Fmla‘𝑁))
1110eleq2d 2837 . . . 4 (𝑥 = 𝑁 → (∅ ∈ (Fmla‘𝑥) ↔ ∅ ∈ (Fmla‘𝑁)))
1211notbid 321 . . 3 (𝑥 = 𝑁 → (¬ ∅ ∈ (Fmla‘𝑥) ↔ ¬ ∅ ∈ (Fmla‘𝑁)))
13 0ex 5181 . . . . . . . . . . . 12 ∅ ∈ V
14 opex 5328 . . . . . . . . . . . 12 𝑖, 𝑗⟩ ∈ V
1513, 14pm3.2i 474 . . . . . . . . . . 11 (∅ ∈ V ∧ ⟨𝑖, 𝑗⟩ ∈ V)
1615a1i 11 . . . . . . . . . 10 ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (∅ ∈ V ∧ ⟨𝑖, 𝑗⟩ ∈ V))
17 necom 3004 . . . . . . . . . . 11 (∅ ≠ ⟨∅, ⟨𝑖, 𝑗⟩⟩ ↔ ⟨∅, ⟨𝑖, 𝑗⟩⟩ ≠ ∅)
18 opnz 5337 . . . . . . . . . . 11 (⟨∅, ⟨𝑖, 𝑗⟩⟩ ≠ ∅ ↔ (∅ ∈ V ∧ ⟨𝑖, 𝑗⟩ ∈ V))
1917, 18bitri 278 . . . . . . . . . 10 (∅ ≠ ⟨∅, ⟨𝑖, 𝑗⟩⟩ ↔ (∅ ∈ V ∧ ⟨𝑖, 𝑗⟩ ∈ V))
2016, 19sylibr 237 . . . . . . . . 9 ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ∅ ≠ ⟨∅, ⟨𝑖, 𝑗⟩⟩)
2120neneqd 2956 . . . . . . . 8 ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ¬ ∅ = ⟨∅, ⟨𝑖, 𝑗⟩⟩)
22 goel 32837 . . . . . . . . 9 ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (𝑖𝑔𝑗) = ⟨∅, ⟨𝑖, 𝑗⟩⟩)
2322eqeq2d 2769 . . . . . . . 8 ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (∅ = (𝑖𝑔𝑗) ↔ ∅ = ⟨∅, ⟨𝑖, 𝑗⟩⟩))
2421, 23mtbird 328 . . . . . . 7 ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ¬ ∅ = (𝑖𝑔𝑗))
2524rgen2 3132 . . . . . 6 𝑖 ∈ ω ∀𝑗 ∈ ω ¬ ∅ = (𝑖𝑔𝑗)
26 ralnex2 3186 . . . . . 6 (∀𝑖 ∈ ω ∀𝑗 ∈ ω ¬ ∅ = (𝑖𝑔𝑗) ↔ ¬ ∃𝑖 ∈ ω ∃𝑗 ∈ ω ∅ = (𝑖𝑔𝑗))
2725, 26mpbi 233 . . . . 5 ¬ ∃𝑖 ∈ ω ∃𝑗 ∈ ω ∅ = (𝑖𝑔𝑗)
2827intnan 490 . . . 4 ¬ (∅ ∈ V ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω ∅ = (𝑖𝑔𝑗))
29 fmla0 32872 . . . . . 6 (Fmla‘∅) = {𝑥 ∈ V ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖𝑔𝑗)}
3029eleq2i 2843 . . . . 5 (∅ ∈ (Fmla‘∅) ↔ ∅ ∈ {𝑥 ∈ V ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖𝑔𝑗)})
31 eqeq1 2762 . . . . . . 7 (𝑥 = ∅ → (𝑥 = (𝑖𝑔𝑗) ↔ ∅ = (𝑖𝑔𝑗)))
32312rexbidv 3224 . . . . . 6 (𝑥 = ∅ → (∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖𝑔𝑗) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω ∅ = (𝑖𝑔𝑗)))
3332elrab 3604 . . . . 5 (∅ ∈ {𝑥 ∈ V ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖𝑔𝑗)} ↔ (∅ ∈ V ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω ∅ = (𝑖𝑔𝑗)))
3430, 33bitri 278 . . . 4 (∅ ∈ (Fmla‘∅) ↔ (∅ ∈ V ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω ∅ = (𝑖𝑔𝑗)))
3528, 34mtbir 326 . . 3 ¬ ∅ ∈ (Fmla‘∅)
36 simpr 488 . . . . . 6 ((𝑦 ∈ ω ∧ ¬ ∅ ∈ (Fmla‘𝑦)) → ¬ ∅ ∈ (Fmla‘𝑦))
37 1oex 8126 . . . . . . . . . . . . . 14 1o ∈ V
38 opex 5328 . . . . . . . . . . . . . 14 𝑢, 𝑣⟩ ∈ V
3937, 38opnzi 5338 . . . . . . . . . . . . 13 ⟨1o, ⟨𝑢, 𝑣⟩⟩ ≠ ∅
4039nesymi 3008 . . . . . . . . . . . 12 ¬ ∅ = ⟨1o, ⟨𝑢, 𝑣⟩⟩
41 gonafv 32840 . . . . . . . . . . . . . 14 ((𝑢 ∈ (Fmla‘𝑦) ∧ 𝑣 ∈ (Fmla‘𝑦)) → (𝑢𝑔𝑣) = ⟨1o, ⟨𝑢, 𝑣⟩⟩)
4241adantll 713 . . . . . . . . . . . . 13 (((𝑦 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑦)) ∧ 𝑣 ∈ (Fmla‘𝑦)) → (𝑢𝑔𝑣) = ⟨1o, ⟨𝑢, 𝑣⟩⟩)
4342eqeq2d 2769 . . . . . . . . . . . 12 (((𝑦 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑦)) ∧ 𝑣 ∈ (Fmla‘𝑦)) → (∅ = (𝑢𝑔𝑣) ↔ ∅ = ⟨1o, ⟨𝑢, 𝑣⟩⟩))
4440, 43mtbiri 330 . . . . . . . . . . 11 (((𝑦 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑦)) ∧ 𝑣 ∈ (Fmla‘𝑦)) → ¬ ∅ = (𝑢𝑔𝑣))
4544ralrimiva 3113 . . . . . . . . . 10 ((𝑦 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑦)) → ∀𝑣 ∈ (Fmla‘𝑦) ¬ ∅ = (𝑢𝑔𝑣))
46 2oex 8128 . . . . . . . . . . . . . . 15 2o ∈ V
47 opex 5328 . . . . . . . . . . . . . . 15 𝑖, 𝑢⟩ ∈ V
4846, 47opnzi 5338 . . . . . . . . . . . . . 14 ⟨2o, ⟨𝑖, 𝑢⟩⟩ ≠ ∅
4948nesymi 3008 . . . . . . . . . . . . 13 ¬ ∅ = ⟨2o, ⟨𝑖, 𝑢⟩⟩
50 df-goal 32832 . . . . . . . . . . . . . 14 𝑔𝑖𝑢 = ⟨2o, ⟨𝑖, 𝑢⟩⟩
5150eqeq2i 2771 . . . . . . . . . . . . 13 (∅ = ∀𝑔𝑖𝑢 ↔ ∅ = ⟨2o, ⟨𝑖, 𝑢⟩⟩)
5249, 51mtbir 326 . . . . . . . . . . . 12 ¬ ∅ = ∀𝑔𝑖𝑢
5352a1i 11 . . . . . . . . . . 11 (((𝑦 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑦)) ∧ 𝑖 ∈ ω) → ¬ ∅ = ∀𝑔𝑖𝑢)
5453ralrimiva 3113 . . . . . . . . . 10 ((𝑦 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑦)) → ∀𝑖 ∈ ω ¬ ∅ = ∀𝑔𝑖𝑢)
5545, 54jca 515 . . . . . . . . 9 ((𝑦 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑦)) → (∀𝑣 ∈ (Fmla‘𝑦) ¬ ∅ = (𝑢𝑔𝑣) ∧ ∀𝑖 ∈ ω ¬ ∅ = ∀𝑔𝑖𝑢))
5655ralrimiva 3113 . . . . . . . 8 (𝑦 ∈ ω → ∀𝑢 ∈ (Fmla‘𝑦)(∀𝑣 ∈ (Fmla‘𝑦) ¬ ∅ = (𝑢𝑔𝑣) ∧ ∀𝑖 ∈ ω ¬ ∅ = ∀𝑔𝑖𝑢))
5756adantr 484 . . . . . . 7 ((𝑦 ∈ ω ∧ ¬ ∅ ∈ (Fmla‘𝑦)) → ∀𝑢 ∈ (Fmla‘𝑦)(∀𝑣 ∈ (Fmla‘𝑦) ¬ ∅ = (𝑢𝑔𝑣) ∧ ∀𝑖 ∈ ω ¬ ∅ = ∀𝑔𝑖𝑢))
58 ralnex 3163 . . . . . . . . . . 11 (∀𝑣 ∈ (Fmla‘𝑦) ¬ ∅ = (𝑢𝑔𝑣) ↔ ¬ ∃𝑣 ∈ (Fmla‘𝑦)∅ = (𝑢𝑔𝑣))
59 ralnex 3163 . . . . . . . . . . 11 (∀𝑖 ∈ ω ¬ ∅ = ∀𝑔𝑖𝑢 ↔ ¬ ∃𝑖 ∈ ω ∅ = ∀𝑔𝑖𝑢)
6058, 59anbi12i 629 . . . . . . . . . 10 ((∀𝑣 ∈ (Fmla‘𝑦) ¬ ∅ = (𝑢𝑔𝑣) ∧ ∀𝑖 ∈ ω ¬ ∅ = ∀𝑔𝑖𝑢) ↔ (¬ ∃𝑣 ∈ (Fmla‘𝑦)∅ = (𝑢𝑔𝑣) ∧ ¬ ∃𝑖 ∈ ω ∅ = ∀𝑔𝑖𝑢))
61 ioran 981 . . . . . . . . . 10 (¬ (∃𝑣 ∈ (Fmla‘𝑦)∅ = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω ∅ = ∀𝑔𝑖𝑢) ↔ (¬ ∃𝑣 ∈ (Fmla‘𝑦)∅ = (𝑢𝑔𝑣) ∧ ¬ ∃𝑖 ∈ ω ∅ = ∀𝑔𝑖𝑢))
6260, 61bitr4i 281 . . . . . . . . 9 ((∀𝑣 ∈ (Fmla‘𝑦) ¬ ∅ = (𝑢𝑔𝑣) ∧ ∀𝑖 ∈ ω ¬ ∅ = ∀𝑔𝑖𝑢) ↔ ¬ (∃𝑣 ∈ (Fmla‘𝑦)∅ = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω ∅ = ∀𝑔𝑖𝑢))
6362ralbii 3097 . . . . . . . 8 (∀𝑢 ∈ (Fmla‘𝑦)(∀𝑣 ∈ (Fmla‘𝑦) ¬ ∅ = (𝑢𝑔𝑣) ∧ ∀𝑖 ∈ ω ¬ ∅ = ∀𝑔𝑖𝑢) ↔ ∀𝑢 ∈ (Fmla‘𝑦) ¬ (∃𝑣 ∈ (Fmla‘𝑦)∅ = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω ∅ = ∀𝑔𝑖𝑢))
64 ralnex 3163 . . . . . . . 8 (∀𝑢 ∈ (Fmla‘𝑦) ¬ (∃𝑣 ∈ (Fmla‘𝑦)∅ = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω ∅ = ∀𝑔𝑖𝑢) ↔ ¬ ∃𝑢 ∈ (Fmla‘𝑦)(∃𝑣 ∈ (Fmla‘𝑦)∅ = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω ∅ = ∀𝑔𝑖𝑢))
6563, 64bitri 278 . . . . . . 7 (∀𝑢 ∈ (Fmla‘𝑦)(∀𝑣 ∈ (Fmla‘𝑦) ¬ ∅ = (𝑢𝑔𝑣) ∧ ∀𝑖 ∈ ω ¬ ∅ = ∀𝑔𝑖𝑢) ↔ ¬ ∃𝑢 ∈ (Fmla‘𝑦)(∃𝑣 ∈ (Fmla‘𝑦)∅ = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω ∅ = ∀𝑔𝑖𝑢))
6657, 65sylib 221 . . . . . 6 ((𝑦 ∈ ω ∧ ¬ ∅ ∈ (Fmla‘𝑦)) → ¬ ∃𝑢 ∈ (Fmla‘𝑦)(∃𝑣 ∈ (Fmla‘𝑦)∅ = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω ∅ = ∀𝑔𝑖𝑢))
67 ioran 981 . . . . . 6 (¬ (∅ ∈ (Fmla‘𝑦) ∨ ∃𝑢 ∈ (Fmla‘𝑦)(∃𝑣 ∈ (Fmla‘𝑦)∅ = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω ∅ = ∀𝑔𝑖𝑢)) ↔ (¬ ∅ ∈ (Fmla‘𝑦) ∧ ¬ ∃𝑢 ∈ (Fmla‘𝑦)(∃𝑣 ∈ (Fmla‘𝑦)∅ = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω ∅ = ∀𝑔𝑖𝑢)))
6836, 66, 67sylanbrc 586 . . . . 5 ((𝑦 ∈ ω ∧ ¬ ∅ ∈ (Fmla‘𝑦)) → ¬ (∅ ∈ (Fmla‘𝑦) ∨ ∃𝑢 ∈ (Fmla‘𝑦)(∃𝑣 ∈ (Fmla‘𝑦)∅ = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω ∅ = ∀𝑔𝑖𝑢)))
69 fmlasuc 32876 . . . . . . . 8 (𝑦 ∈ ω → (Fmla‘suc 𝑦) = ((Fmla‘𝑦) ∪ {𝑥 ∣ ∃𝑢 ∈ (Fmla‘𝑦)(∃𝑣 ∈ (Fmla‘𝑦)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)}))
7069eleq2d 2837 . . . . . . 7 (𝑦 ∈ ω → (∅ ∈ (Fmla‘suc 𝑦) ↔ ∅ ∈ ((Fmla‘𝑦) ∪ {𝑥 ∣ ∃𝑢 ∈ (Fmla‘𝑦)(∃𝑣 ∈ (Fmla‘𝑦)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)})))
71 elun 4056 . . . . . . . 8 (∅ ∈ ((Fmla‘𝑦) ∪ {𝑥 ∣ ∃𝑢 ∈ (Fmla‘𝑦)(∃𝑣 ∈ (Fmla‘𝑦)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)}) ↔ (∅ ∈ (Fmla‘𝑦) ∨ ∅ ∈ {𝑥 ∣ ∃𝑢 ∈ (Fmla‘𝑦)(∃𝑣 ∈ (Fmla‘𝑦)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)}))
72 eqeq1 2762 . . . . . . . . . . . . 13 (𝑥 = ∅ → (𝑥 = (𝑢𝑔𝑣) ↔ ∅ = (𝑢𝑔𝑣)))
7372rexbidv 3221 . . . . . . . . . . . 12 (𝑥 = ∅ → (∃𝑣 ∈ (Fmla‘𝑦)𝑥 = (𝑢𝑔𝑣) ↔ ∃𝑣 ∈ (Fmla‘𝑦)∅ = (𝑢𝑔𝑣)))
74 eqeq1 2762 . . . . . . . . . . . . 13 (𝑥 = ∅ → (𝑥 = ∀𝑔𝑖𝑢 ↔ ∅ = ∀𝑔𝑖𝑢))
7574rexbidv 3221 . . . . . . . . . . . 12 (𝑥 = ∅ → (∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢 ↔ ∃𝑖 ∈ ω ∅ = ∀𝑔𝑖𝑢))
7673, 75orbi12d 916 . . . . . . . . . . 11 (𝑥 = ∅ → ((∃𝑣 ∈ (Fmla‘𝑦)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) ↔ (∃𝑣 ∈ (Fmla‘𝑦)∅ = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω ∅ = ∀𝑔𝑖𝑢)))
7776rexbidv 3221 . . . . . . . . . 10 (𝑥 = ∅ → (∃𝑢 ∈ (Fmla‘𝑦)(∃𝑣 ∈ (Fmla‘𝑦)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) ↔ ∃𝑢 ∈ (Fmla‘𝑦)(∃𝑣 ∈ (Fmla‘𝑦)∅ = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω ∅ = ∀𝑔𝑖𝑢)))
7813, 77elab 3590 . . . . . . . . 9 (∅ ∈ {𝑥 ∣ ∃𝑢 ∈ (Fmla‘𝑦)(∃𝑣 ∈ (Fmla‘𝑦)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)} ↔ ∃𝑢 ∈ (Fmla‘𝑦)(∃𝑣 ∈ (Fmla‘𝑦)∅ = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω ∅ = ∀𝑔𝑖𝑢))
7978orbi2i 910 . . . . . . . 8 ((∅ ∈ (Fmla‘𝑦) ∨ ∅ ∈ {𝑥 ∣ ∃𝑢 ∈ (Fmla‘𝑦)(∃𝑣 ∈ (Fmla‘𝑦)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)}) ↔ (∅ ∈ (Fmla‘𝑦) ∨ ∃𝑢 ∈ (Fmla‘𝑦)(∃𝑣 ∈ (Fmla‘𝑦)∅ = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω ∅ = ∀𝑔𝑖𝑢)))
8071, 79bitri 278 . . . . . . 7 (∅ ∈ ((Fmla‘𝑦) ∪ {𝑥 ∣ ∃𝑢 ∈ (Fmla‘𝑦)(∃𝑣 ∈ (Fmla‘𝑦)𝑥 = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)}) ↔ (∅ ∈ (Fmla‘𝑦) ∨ ∃𝑢 ∈ (Fmla‘𝑦)(∃𝑣 ∈ (Fmla‘𝑦)∅ = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω ∅ = ∀𝑔𝑖𝑢)))
8170, 80bitrdi 290 . . . . . 6 (𝑦 ∈ ω → (∅ ∈ (Fmla‘suc 𝑦) ↔ (∅ ∈ (Fmla‘𝑦) ∨ ∃𝑢 ∈ (Fmla‘𝑦)(∃𝑣 ∈ (Fmla‘𝑦)∅ = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω ∅ = ∀𝑔𝑖𝑢))))
8281adantr 484 . . . . 5 ((𝑦 ∈ ω ∧ ¬ ∅ ∈ (Fmla‘𝑦)) → (∅ ∈ (Fmla‘suc 𝑦) ↔ (∅ ∈ (Fmla‘𝑦) ∨ ∃𝑢 ∈ (Fmla‘𝑦)(∃𝑣 ∈ (Fmla‘𝑦)∅ = (𝑢𝑔𝑣) ∨ ∃𝑖 ∈ ω ∅ = ∀𝑔𝑖𝑢))))
8368, 82mtbird 328 . . . 4 ((𝑦 ∈ ω ∧ ¬ ∅ ∈ (Fmla‘𝑦)) → ¬ ∅ ∈ (Fmla‘suc 𝑦))
8483ex 416 . . 3 (𝑦 ∈ ω → (¬ ∅ ∈ (Fmla‘𝑦) → ¬ ∅ ∈ (Fmla‘suc 𝑦)))
853, 6, 9, 12, 35, 84finds 7614 . 2 (𝑁 ∈ ω → ¬ ∅ ∈ (Fmla‘𝑁))
86 df-nel 3056 . 2 (∅ ∉ (Fmla‘𝑁) ↔ ¬ ∅ ∈ (Fmla‘𝑁))
8785, 86sylibr 237 1 (𝑁 ∈ ω → ∅ ∉ (Fmla‘𝑁))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844   = wceq 1538   ∈ wcel 2111  {cab 2735   ≠ wne 2951   ∉ wnel 3055  ∀wral 3070  ∃wrex 3071  {crab 3074  Vcvv 3409   ∪ cun 3858  ∅c0 4227  ⟨cop 4531  suc csuc 6176  ‘cfv 6340  (class class class)co 7156  ωcom 7585  1oc1o 8111  2oc2o 8112  ∈𝑔cgoe 32823  ⊼𝑔cgna 32824  ∀𝑔cgol 32825  Fmlacfmla 32827 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-rep 5160  ax-sep 5173  ax-nul 5180  ax-pow 5238  ax-pr 5302  ax-un 7465  ax-inf2 9150 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-nel 3056  df-ral 3075  df-rex 3076  df-reu 3077  df-rab 3079  df-v 3411  df-sbc 3699  df-csb 3808  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-pss 3879  df-nul 4228  df-if 4424  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-iun 4888  df-br 5037  df-opab 5099  df-mpt 5117  df-tr 5143  df-id 5434  df-eprel 5439  df-po 5447  df-so 5448  df-fr 5487  df-we 5489  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-res 5540  df-ima 5541  df-pred 6131  df-ord 6177  df-on 6178  df-lim 6179  df-suc 6180  df-iota 6299  df-fun 6342  df-fn 6343  df-f 6344  df-f1 6345  df-fo 6346  df-f1o 6347  df-fv 6348  df-ov 7159  df-oprab 7160  df-mpo 7161  df-om 7586  df-1st 7699  df-2nd 7700  df-wrecs 7963  df-recs 8024  df-rdg 8062  df-1o 8118  df-2o 8119  df-map 8424  df-goel 32830  df-gona 32831  df-goal 32832  df-sat 32833  df-fmla 32835 This theorem is referenced by:  fmlan0  32881  gonan0  32882
 Copyright terms: Public domain W3C validator