Metamath Proof Explorer

Theorem fmlaomn0

Description: The empty set is not a Godel formula of any height. (Contributed by AV, 21-Oct-2023)

Ref Expression
Assertion fmlaomn0 ( 𝑁 ∈ ω → ∅ ∉ ( Fmla ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ ( 𝑥 = ∅ → ( Fmla ‘ 𝑥 ) = ( Fmla ‘ ∅ ) )
2 1 eleq2d ⊢ ( 𝑥 = ∅ → ( ∅ ∈ ( Fmla ‘ 𝑥 ) ↔ ∅ ∈ ( Fmla ‘ ∅ ) ) )
3 2 notbid ⊢ ( 𝑥 = ∅ → ( ¬ ∅ ∈ ( Fmla ‘ 𝑥 ) ↔ ¬ ∅ ∈ ( Fmla ‘ ∅ ) ) )
4 fveq2 ⊢ ( 𝑥 = 𝑦 → ( Fmla ‘ 𝑥 ) = ( Fmla ‘ 𝑦 ) )
5 4 eleq2d ⊢ ( 𝑥 = 𝑦 → ( ∅ ∈ ( Fmla ‘ 𝑥 ) ↔ ∅ ∈ ( Fmla ‘ 𝑦 ) ) )
6 5 notbid ⊢ ( 𝑥 = 𝑦 → ( ¬ ∅ ∈ ( Fmla ‘ 𝑥 ) ↔ ¬ ∅ ∈ ( Fmla ‘ 𝑦 ) ) )
7 fveq2 ⊢ ( 𝑥 = suc 𝑦 → ( Fmla ‘ 𝑥 ) = ( Fmla ‘ suc 𝑦 ) )
8 7 eleq2d ⊢ ( 𝑥 = suc 𝑦 → ( ∅ ∈ ( Fmla ‘ 𝑥 ) ↔ ∅ ∈ ( Fmla ‘ suc 𝑦 ) ) )
9 8 notbid ⊢ ( 𝑥 = suc 𝑦 → ( ¬ ∅ ∈ ( Fmla ‘ 𝑥 ) ↔ ¬ ∅ ∈ ( Fmla ‘ suc 𝑦 ) ) )
10 fveq2 ⊢ ( 𝑥 = 𝑁 → ( Fmla ‘ 𝑥 ) = ( Fmla ‘ 𝑁 ) )
11 10 eleq2d ⊢ ( 𝑥 = 𝑁 → ( ∅ ∈ ( Fmla ‘ 𝑥 ) ↔ ∅ ∈ ( Fmla ‘ 𝑁 ) ) )
12 11 notbid ⊢ ( 𝑥 = 𝑁 → ( ¬ ∅ ∈ ( Fmla ‘ 𝑥 ) ↔ ¬ ∅ ∈ ( Fmla ‘ 𝑁 ) ) )
13 0ex ⊢ ∅ ∈ V
14 opex ⊢ ⟨ 𝑖 , 𝑗 ⟩ ∈ V
15 13 14 pm3.2i ⊢ ( ∅ ∈ V ∧ ⟨ 𝑖 , 𝑗 ⟩ ∈ V )
16 15 a1i ⊢ ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → ( ∅ ∈ V ∧ ⟨ 𝑖 , 𝑗 ⟩ ∈ V ) )
17 necom ⊢ ( ∅ ≠ ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ ↔ ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ ≠ ∅ )
18 opnz ⊢ ( ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ ≠ ∅ ↔ ( ∅ ∈ V ∧ ⟨ 𝑖 , 𝑗 ⟩ ∈ V ) )
19 17 18 bitri ⊢ ( ∅ ≠ ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ ↔ ( ∅ ∈ V ∧ ⟨ 𝑖 , 𝑗 ⟩ ∈ V ) )
20 16 19 sylibr ⊢ ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → ∅ ≠ ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ )
21 20 neneqd ⊢ ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → ¬ ∅ = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ )
22 goel ⊢ ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → ( 𝑖 ∈𝑔 𝑗 ) = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ )
23 22 eqeq2d ⊢ ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → ( ∅ = ( 𝑖 ∈𝑔 𝑗 ) ↔ ∅ = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ ) )
24 21 23 mtbird ⊢ ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → ¬ ∅ = ( 𝑖 ∈𝑔 𝑗 ) )
25 24 rgen2 ⊢ ∀ 𝑖 ∈ ω ∀ 𝑗 ∈ ω ¬ ∅ = ( 𝑖 ∈𝑔 𝑗 )
26 ralnex2 ⊢ ( ∀ 𝑖 ∈ ω ∀ 𝑗 ∈ ω ¬ ∅ = ( 𝑖 ∈𝑔 𝑗 ) ↔ ¬ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ∅ = ( 𝑖 ∈𝑔 𝑗 ) )
27 25 26 mpbi ⊢ ¬ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ∅ = ( 𝑖 ∈𝑔 𝑗 )
28 27 intnan ⊢ ¬ ( ∅ ∈ V ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ∅ = ( 𝑖 ∈𝑔 𝑗 ) )
29 fmla0 ⊢ ( Fmla ‘ ∅ ) = { 𝑥 ∈ V ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) }
30 29 eleq2i ⊢ ( ∅ ∈ ( Fmla ‘ ∅ ) ↔ ∅ ∈ { 𝑥 ∈ V ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) } )
31 eqeq1 ⊢ ( 𝑥 = ∅ → ( 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ↔ ∅ = ( 𝑖 ∈𝑔 𝑗 ) ) )
32 31 2rexbidv ⊢ ( 𝑥 = ∅ → ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ↔ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ∅ = ( 𝑖 ∈𝑔 𝑗 ) ) )
33 32 elrab ⊢ ( ∅ ∈ { 𝑥 ∈ V ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) } ↔ ( ∅ ∈ V ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ∅ = ( 𝑖 ∈𝑔 𝑗 ) ) )
34 30 33 bitri ⊢ ( ∅ ∈ ( Fmla ‘ ∅ ) ↔ ( ∅ ∈ V ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ∅ = ( 𝑖 ∈𝑔 𝑗 ) ) )
35 28 34 mtbir ⊢ ¬ ∅ ∈ ( Fmla ‘ ∅ )
36 simpr ⊢ ( ( 𝑦 ∈ ω ∧ ¬ ∅ ∈ ( Fmla ‘ 𝑦 ) ) → ¬ ∅ ∈ ( Fmla ‘ 𝑦 ) )
37 1oex ⊢ 1o ∈ V
38 opex ⊢ ⟨ 𝑢 , 𝑣 ⟩ ∈ V
39 37 38 opnzi ⊢ ⟨ 1o , ⟨ 𝑢 , 𝑣 ⟩ ⟩ ≠ ∅
40 39 nesymi ⊢ ¬ ∅ = ⟨ 1o , ⟨ 𝑢 , 𝑣 ⟩ ⟩
41 gonafv ⊢ ( ( 𝑢 ∈ ( Fmla ‘ 𝑦 ) ∧ 𝑣 ∈ ( Fmla ‘ 𝑦 ) ) → ( 𝑢 ⊼𝑔 𝑣 ) = ⟨ 1o , ⟨ 𝑢 , 𝑣 ⟩ ⟩ )
42 41 adantll ⊢ ( ( ( 𝑦 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ 𝑦 ) ) ∧ 𝑣 ∈ ( Fmla ‘ 𝑦 ) ) → ( 𝑢 ⊼𝑔 𝑣 ) = ⟨ 1o , ⟨ 𝑢 , 𝑣 ⟩ ⟩ )
43 42 eqeq2d ⊢ ( ( ( 𝑦 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ 𝑦 ) ) ∧ 𝑣 ∈ ( Fmla ‘ 𝑦 ) ) → ( ∅ = ( 𝑢 ⊼𝑔 𝑣 ) ↔ ∅ = ⟨ 1o , ⟨ 𝑢 , 𝑣 ⟩ ⟩ ) )
44 40 43 mtbiri ⊢ ( ( ( 𝑦 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ 𝑦 ) ) ∧ 𝑣 ∈ ( Fmla ‘ 𝑦 ) ) → ¬ ∅ = ( 𝑢 ⊼𝑔 𝑣 ) )
45 44 ralrimiva ⊢ ( ( 𝑦 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ 𝑦 ) ) → ∀ 𝑣 ∈ ( Fmla ‘ 𝑦 ) ¬ ∅ = ( 𝑢 ⊼𝑔 𝑣 ) )
46 2oex ⊢ 2o ∈ V
47 opex ⊢ ⟨ 𝑖 , 𝑢 ⟩ ∈ V
48 46 47 opnzi ⊢ ⟨ 2o , ⟨ 𝑖 , 𝑢 ⟩ ⟩ ≠ ∅
49 48 nesymi ⊢ ¬ ∅ = ⟨ 2o , ⟨ 𝑖 , 𝑢 ⟩ ⟩
50 df-goal ⊢ ∀𝑔 𝑖 𝑢 = ⟨ 2o , ⟨ 𝑖 , 𝑢 ⟩ ⟩
51 50 eqeq2i ⊢ ( ∅ = ∀𝑔 𝑖 𝑢 ↔ ∅ = ⟨ 2o , ⟨ 𝑖 , 𝑢 ⟩ ⟩ )
52 49 51 mtbir ⊢ ¬ ∅ = ∀𝑔 𝑖 𝑢
53 52 a1i ⊢ ( ( ( 𝑦 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ 𝑦 ) ) ∧ 𝑖 ∈ ω ) → ¬ ∅ = ∀𝑔 𝑖 𝑢 )
54 53 ralrimiva ⊢ ( ( 𝑦 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ 𝑦 ) ) → ∀ 𝑖 ∈ ω ¬ ∅ = ∀𝑔 𝑖 𝑢 )
55 45 54 jca ⊢ ( ( 𝑦 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ 𝑦 ) ) → ( ∀ 𝑣 ∈ ( Fmla ‘ 𝑦 ) ¬ ∅ = ( 𝑢 ⊼𝑔 𝑣 ) ∧ ∀ 𝑖 ∈ ω ¬ ∅ = ∀𝑔 𝑖 𝑢 ) )
56 55 ralrimiva ⊢ ( 𝑦 ∈ ω → ∀ 𝑢 ∈ ( Fmla ‘ 𝑦 ) ( ∀ 𝑣 ∈ ( Fmla ‘ 𝑦 ) ¬ ∅ = ( 𝑢 ⊼𝑔 𝑣 ) ∧ ∀ 𝑖 ∈ ω ¬ ∅ = ∀𝑔 𝑖 𝑢 ) )
57 56 adantr ⊢ ( ( 𝑦 ∈ ω ∧ ¬ ∅ ∈ ( Fmla ‘ 𝑦 ) ) → ∀ 𝑢 ∈ ( Fmla ‘ 𝑦 ) ( ∀ 𝑣 ∈ ( Fmla ‘ 𝑦 ) ¬ ∅ = ( 𝑢 ⊼𝑔 𝑣 ) ∧ ∀ 𝑖 ∈ ω ¬ ∅ = ∀𝑔 𝑖 𝑢 ) )
58 ralnex ⊢ ( ∀ 𝑣 ∈ ( Fmla ‘ 𝑦 ) ¬ ∅ = ( 𝑢 ⊼𝑔 𝑣 ) ↔ ¬ ∃ 𝑣 ∈ ( Fmla ‘ 𝑦 ) ∅ = ( 𝑢 ⊼𝑔 𝑣 ) )
59 ralnex ⊢ ( ∀ 𝑖 ∈ ω ¬ ∅ = ∀𝑔 𝑖 𝑢 ↔ ¬ ∃ 𝑖 ∈ ω ∅ = ∀𝑔 𝑖 𝑢 )
60 58 59 anbi12i ⊢ ( ( ∀ 𝑣 ∈ ( Fmla ‘ 𝑦 ) ¬ ∅ = ( 𝑢 ⊼𝑔 𝑣 ) ∧ ∀ 𝑖 ∈ ω ¬ ∅ = ∀𝑔 𝑖 𝑢 ) ↔ ( ¬ ∃ 𝑣 ∈ ( Fmla ‘ 𝑦 ) ∅ = ( 𝑢 ⊼𝑔 𝑣 ) ∧ ¬ ∃ 𝑖 ∈ ω ∅ = ∀𝑔 𝑖 𝑢 ) )
61 ioran ⊢ ( ¬ ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑦 ) ∅ = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω ∅ = ∀𝑔 𝑖 𝑢 ) ↔ ( ¬ ∃ 𝑣 ∈ ( Fmla ‘ 𝑦 ) ∅ = ( 𝑢 ⊼𝑔 𝑣 ) ∧ ¬ ∃ 𝑖 ∈ ω ∅ = ∀𝑔 𝑖 𝑢 ) )
62 60 61 bitr4i ⊢ ( ( ∀ 𝑣 ∈ ( Fmla ‘ 𝑦 ) ¬ ∅ = ( 𝑢 ⊼𝑔 𝑣 ) ∧ ∀ 𝑖 ∈ ω ¬ ∅ = ∀𝑔 𝑖 𝑢 ) ↔ ¬ ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑦 ) ∅ = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω ∅ = ∀𝑔 𝑖 𝑢 ) )
63 62 ralbii ⊢ ( ∀ 𝑢 ∈ ( Fmla ‘ 𝑦 ) ( ∀ 𝑣 ∈ ( Fmla ‘ 𝑦 ) ¬ ∅ = ( 𝑢 ⊼𝑔 𝑣 ) ∧ ∀ 𝑖 ∈ ω ¬ ∅ = ∀𝑔 𝑖 𝑢 ) ↔ ∀ 𝑢 ∈ ( Fmla ‘ 𝑦 ) ¬ ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑦 ) ∅ = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω ∅ = ∀𝑔 𝑖 𝑢 ) )
64 ralnex ⊢ ( ∀ 𝑢 ∈ ( Fmla ‘ 𝑦 ) ¬ ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑦 ) ∅ = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω ∅ = ∀𝑔 𝑖 𝑢 ) ↔ ¬ ∃ 𝑢 ∈ ( Fmla ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑦 ) ∅ = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω ∅ = ∀𝑔 𝑖 𝑢 ) )
65 63 64 bitri ⊢ ( ∀ 𝑢 ∈ ( Fmla ‘ 𝑦 ) ( ∀ 𝑣 ∈ ( Fmla ‘ 𝑦 ) ¬ ∅ = ( 𝑢 ⊼𝑔 𝑣 ) ∧ ∀ 𝑖 ∈ ω ¬ ∅ = ∀𝑔 𝑖 𝑢 ) ↔ ¬ ∃ 𝑢 ∈ ( Fmla ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑦 ) ∅ = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω ∅ = ∀𝑔 𝑖 𝑢 ) )
66 57 65 sylib ⊢ ( ( 𝑦 ∈ ω ∧ ¬ ∅ ∈ ( Fmla ‘ 𝑦 ) ) → ¬ ∃ 𝑢 ∈ ( Fmla ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑦 ) ∅ = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω ∅ = ∀𝑔 𝑖 𝑢 ) )
67 ioran ⊢ ( ¬ ( ∅ ∈ ( Fmla ‘ 𝑦 ) ∨ ∃ 𝑢 ∈ ( Fmla ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑦 ) ∅ = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω ∅ = ∀𝑔 𝑖 𝑢 ) ) ↔ ( ¬ ∅ ∈ ( Fmla ‘ 𝑦 ) ∧ ¬ ∃ 𝑢 ∈ ( Fmla ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑦 ) ∅ = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω ∅ = ∀𝑔 𝑖 𝑢 ) ) )
68 36 66 67 sylanbrc ⊢ ( ( 𝑦 ∈ ω ∧ ¬ ∅ ∈ ( Fmla ‘ 𝑦 ) ) → ¬ ( ∅ ∈ ( Fmla ‘ 𝑦 ) ∨ ∃ 𝑢 ∈ ( Fmla ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑦 ) ∅ = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω ∅ = ∀𝑔 𝑖 𝑢 ) ) )
69 fmlasuc ⊢ ( 𝑦 ∈ ω → ( Fmla ‘ suc 𝑦 ) = ( ( Fmla ‘ 𝑦 ) ∪ { 𝑥 ∣ ∃ 𝑢 ∈ ( Fmla ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑦 ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) } ) )
70 69 eleq2d ⊢ ( 𝑦 ∈ ω → ( ∅ ∈ ( Fmla ‘ suc 𝑦 ) ↔ ∅ ∈ ( ( Fmla ‘ 𝑦 ) ∪ { 𝑥 ∣ ∃ 𝑢 ∈ ( Fmla ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑦 ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) } ) ) )
71 elun ⊢ ( ∅ ∈ ( ( Fmla ‘ 𝑦 ) ∪ { 𝑥 ∣ ∃ 𝑢 ∈ ( Fmla ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑦 ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) } ) ↔ ( ∅ ∈ ( Fmla ‘ 𝑦 ) ∨ ∅ ∈ { 𝑥 ∣ ∃ 𝑢 ∈ ( Fmla ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑦 ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) } ) )
72 eqeq1 ⊢ ( 𝑥 = ∅ → ( 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ↔ ∅ = ( 𝑢 ⊼𝑔 𝑣 ) ) )
73 72 rexbidv ⊢ ( 𝑥 = ∅ → ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑦 ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ↔ ∃ 𝑣 ∈ ( Fmla ‘ 𝑦 ) ∅ = ( 𝑢 ⊼𝑔 𝑣 ) ) )
74 eqeq1 ⊢ ( 𝑥 = ∅ → ( 𝑥 = ∀𝑔 𝑖 𝑢 ↔ ∅ = ∀𝑔 𝑖 𝑢 ) )
75 74 rexbidv ⊢ ( 𝑥 = ∅ → ( ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ↔ ∃ 𝑖 ∈ ω ∅ = ∀𝑔 𝑖 𝑢 ) )
76 73 75 orbi12d ⊢ ( 𝑥 = ∅ → ( ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑦 ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ↔ ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑦 ) ∅ = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω ∅ = ∀𝑔 𝑖 𝑢 ) ) )
77 76 rexbidv ⊢ ( 𝑥 = ∅ → ( ∃ 𝑢 ∈ ( Fmla ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑦 ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ↔ ∃ 𝑢 ∈ ( Fmla ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑦 ) ∅ = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω ∅ = ∀𝑔 𝑖 𝑢 ) ) )
78 13 77 elab ⊢ ( ∅ ∈ { 𝑥 ∣ ∃ 𝑢 ∈ ( Fmla ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑦 ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) } ↔ ∃ 𝑢 ∈ ( Fmla ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑦 ) ∅ = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω ∅ = ∀𝑔 𝑖 𝑢 ) )
79 78 orbi2i ⊢ ( ( ∅ ∈ ( Fmla ‘ 𝑦 ) ∨ ∅ ∈ { 𝑥 ∣ ∃ 𝑢 ∈ ( Fmla ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑦 ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) } ) ↔ ( ∅ ∈ ( Fmla ‘ 𝑦 ) ∨ ∃ 𝑢 ∈ ( Fmla ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑦 ) ∅ = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω ∅ = ∀𝑔 𝑖 𝑢 ) ) )
80 71 79 bitri ⊢ ( ∅ ∈ ( ( Fmla ‘ 𝑦 ) ∪ { 𝑥 ∣ ∃ 𝑢 ∈ ( Fmla ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑦 ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) } ) ↔ ( ∅ ∈ ( Fmla ‘ 𝑦 ) ∨ ∃ 𝑢 ∈ ( Fmla ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑦 ) ∅ = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω ∅ = ∀𝑔 𝑖 𝑢 ) ) )
81 70 80 bitrdi ⊢ ( 𝑦 ∈ ω → ( ∅ ∈ ( Fmla ‘ suc 𝑦 ) ↔ ( ∅ ∈ ( Fmla ‘ 𝑦 ) ∨ ∃ 𝑢 ∈ ( Fmla ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑦 ) ∅ = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω ∅ = ∀𝑔 𝑖 𝑢 ) ) ) )
82 81 adantr ⊢ ( ( 𝑦 ∈ ω ∧ ¬ ∅ ∈ ( Fmla ‘ 𝑦 ) ) → ( ∅ ∈ ( Fmla ‘ suc 𝑦 ) ↔ ( ∅ ∈ ( Fmla ‘ 𝑦 ) ∨ ∃ 𝑢 ∈ ( Fmla ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑦 ) ∅ = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω ∅ = ∀𝑔 𝑖 𝑢 ) ) ) )
83 68 82 mtbird ⊢ ( ( 𝑦 ∈ ω ∧ ¬ ∅ ∈ ( Fmla ‘ 𝑦 ) ) → ¬ ∅ ∈ ( Fmla ‘ suc 𝑦 ) )
84 83 ex ⊢ ( 𝑦 ∈ ω → ( ¬ ∅ ∈ ( Fmla ‘ 𝑦 ) → ¬ ∅ ∈ ( Fmla ‘ suc 𝑦 ) ) )
85 3 6 9 12 35 84 finds ⊢ ( 𝑁 ∈ ω → ¬ ∅ ∈ ( Fmla ‘ 𝑁 ) )
86 df-nel ⊢ ( ∅ ∉ ( Fmla ‘ 𝑁 ) ↔ ¬ ∅ ∈ ( Fmla ‘ 𝑁 ) )
87 85 86 sylibr ⊢ ( 𝑁 ∈ ω → ∅ ∉ ( Fmla ‘ 𝑁 ) )