This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem goalr

Description: If the "Godel-set of universal quantification" applied to a class is a Godel formula, the class is also a Godel formula. Remark: The reverse is not valid for A being of the same height as the "Godel-set of universal quantification". (Contributed by AV, 22-Oct-2023)

Ref Expression
Assertion goalr ( ( 𝑁 ∈ ω ∧ ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ 𝑁 ) ) → 𝑎 ∈ ( Fmla ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 goaln0 ⊢ ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ 𝑁 ) → 𝑁 ≠ ∅ )
2 1 adantl ⊢ ( ( 𝑁 ∈ ω ∧ ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ 𝑁 ) ) → 𝑁 ≠ ∅ )
3 nnsuc ⊢ ( ( 𝑁 ∈ ω ∧ 𝑁 ≠ ∅ ) → ∃ 𝑛 ∈ ω 𝑁 = suc 𝑛 )
4 suceq ⊢ ( 𝑥 = ∅ → suc 𝑥 = suc ∅ )
5 4 fveq2d ⊢ ( 𝑥 = ∅ → ( Fmla ‘ suc 𝑥 ) = ( Fmla ‘ suc ∅ ) )
6 5 eleq2d ⊢ ( 𝑥 = ∅ → ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc 𝑥 ) ↔ ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc ∅ ) ) )
7 5 eleq2d ⊢ ( 𝑥 = ∅ → ( 𝑎 ∈ ( Fmla ‘ suc 𝑥 ) ↔ 𝑎 ∈ ( Fmla ‘ suc ∅ ) ) )
8 6 7 imbi12d ⊢ ( 𝑥 = ∅ → ( ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc 𝑥 ) → 𝑎 ∈ ( Fmla ‘ suc 𝑥 ) ) ↔ ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc ∅ ) → 𝑎 ∈ ( Fmla ‘ suc ∅ ) ) ) )
9 suceq ⊢ ( 𝑥 = 𝑦 → suc 𝑥 = suc 𝑦 )
10 9 fveq2d ⊢ ( 𝑥 = 𝑦 → ( Fmla ‘ suc 𝑥 ) = ( Fmla ‘ suc 𝑦 ) )
11 10 eleq2d ⊢ ( 𝑥 = 𝑦 → ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc 𝑥 ) ↔ ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc 𝑦 ) ) )
12 10 eleq2d ⊢ ( 𝑥 = 𝑦 → ( 𝑎 ∈ ( Fmla ‘ suc 𝑥 ) ↔ 𝑎 ∈ ( Fmla ‘ suc 𝑦 ) ) )
13 11 12 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc 𝑥 ) → 𝑎 ∈ ( Fmla ‘ suc 𝑥 ) ) ↔ ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc 𝑦 ) → 𝑎 ∈ ( Fmla ‘ suc 𝑦 ) ) ) )
14 suceq ⊢ ( 𝑥 = suc 𝑦 → suc 𝑥 = suc suc 𝑦 )
15 14 fveq2d ⊢ ( 𝑥 = suc 𝑦 → ( Fmla ‘ suc 𝑥 ) = ( Fmla ‘ suc suc 𝑦 ) )
16 15 eleq2d ⊢ ( 𝑥 = suc 𝑦 → ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc 𝑥 ) ↔ ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc suc 𝑦 ) ) )
17 15 eleq2d ⊢ ( 𝑥 = suc 𝑦 → ( 𝑎 ∈ ( Fmla ‘ suc 𝑥 ) ↔ 𝑎 ∈ ( Fmla ‘ suc suc 𝑦 ) ) )
18 16 17 imbi12d ⊢ ( 𝑥 = suc 𝑦 → ( ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc 𝑥 ) → 𝑎 ∈ ( Fmla ‘ suc 𝑥 ) ) ↔ ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc suc 𝑦 ) → 𝑎 ∈ ( Fmla ‘ suc suc 𝑦 ) ) ) )
19 suceq ⊢ ( 𝑥 = 𝑛 → suc 𝑥 = suc 𝑛 )
20 19 fveq2d ⊢ ( 𝑥 = 𝑛 → ( Fmla ‘ suc 𝑥 ) = ( Fmla ‘ suc 𝑛 ) )
21 20 eleq2d ⊢ ( 𝑥 = 𝑛 → ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc 𝑥 ) ↔ ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc 𝑛 ) ) )
22 20 eleq2d ⊢ ( 𝑥 = 𝑛 → ( 𝑎 ∈ ( Fmla ‘ suc 𝑥 ) ↔ 𝑎 ∈ ( Fmla ‘ suc 𝑛 ) ) )
23 21 22 imbi12d ⊢ ( 𝑥 = 𝑛 → ( ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc 𝑥 ) → 𝑎 ∈ ( Fmla ‘ suc 𝑥 ) ) ↔ ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc 𝑛 ) → 𝑎 ∈ ( Fmla ‘ suc 𝑛 ) ) ) )
24 peano1 ⊢ ∅ ∈ ω
25 df-goal ⊢ ∀𝑔 𝑖 𝑎 = ⟨ 2o , ⟨ 𝑖 , 𝑎 ⟩ ⟩
26 opex ⊢ ⟨ 2o , ⟨ 𝑖 , 𝑎 ⟩ ⟩ ∈ V
27 25 26 eqeltri ⊢ ∀𝑔 𝑖 𝑎 ∈ V
28 isfmlasuc ⊢ ( ( ∅ ∈ ω ∧ ∀𝑔 𝑖 𝑎 ∈ V ) → ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc ∅ ) ↔ ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ ∅ ) ∨ ∃ 𝑢 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) ∀𝑔 𝑖 𝑎 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑘 ∈ ω ∀𝑔 𝑖 𝑎 = ∀𝑔 𝑘 𝑢 ) ) ) )
29 24 27 28 mp2an ⊢ ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc ∅ ) ↔ ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ ∅ ) ∨ ∃ 𝑢 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) ∀𝑔 𝑖 𝑎 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑘 ∈ ω ∀𝑔 𝑖 𝑎 = ∀𝑔 𝑘 𝑢 ) ) )
30 eqeq1 ⊢ ( 𝑥 = ∀𝑔 𝑖 𝑎 → ( 𝑥 = ( 𝑘 ∈𝑔 𝑗 ) ↔ ∀𝑔 𝑖 𝑎 = ( 𝑘 ∈𝑔 𝑗 ) ) )
31 30 2rexbidv ⊢ ( 𝑥 = ∀𝑔 𝑖 𝑎 → ( ∃ 𝑘 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑘 ∈𝑔 𝑗 ) ↔ ∃ 𝑘 ∈ ω ∃ 𝑗 ∈ ω ∀𝑔 𝑖 𝑎 = ( 𝑘 ∈𝑔 𝑗 ) ) )
32 fmla0 ⊢ ( Fmla ‘ ∅ ) = { 𝑥 ∈ V ∣ ∃ 𝑘 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑘 ∈𝑔 𝑗 ) }
33 31 32 elrab2 ⊢ ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ ∅ ) ↔ ( ∀𝑔 𝑖 𝑎 ∈ V ∧ ∃ 𝑘 ∈ ω ∃ 𝑗 ∈ ω ∀𝑔 𝑖 𝑎 = ( 𝑘 ∈𝑔 𝑗 ) ) )
34 25 a1i ⊢ ( ( 𝑘 ∈ ω ∧ 𝑗 ∈ ω ) → ∀𝑔 𝑖 𝑎 = ⟨ 2o , ⟨ 𝑖 , 𝑎 ⟩ ⟩ )
35 goel ⊢ ( ( 𝑘 ∈ ω ∧ 𝑗 ∈ ω ) → ( 𝑘 ∈𝑔 𝑗 ) = ⟨ ∅ , ⟨ 𝑘 , 𝑗 ⟩ ⟩ )
36 34 35 eqeq12d ⊢ ( ( 𝑘 ∈ ω ∧ 𝑗 ∈ ω ) → ( ∀𝑔 𝑖 𝑎 = ( 𝑘 ∈𝑔 𝑗 ) ↔ ⟨ 2o , ⟨ 𝑖 , 𝑎 ⟩ ⟩ = ⟨ ∅ , ⟨ 𝑘 , 𝑗 ⟩ ⟩ ) )
37 2oex ⊢ 2o ∈ V
38 opex ⊢ ⟨ 𝑖 , 𝑎 ⟩ ∈ V
39 37 38 opth ⊢ ( ⟨ 2o , ⟨ 𝑖 , 𝑎 ⟩ ⟩ = ⟨ ∅ , ⟨ 𝑘 , 𝑗 ⟩ ⟩ ↔ ( 2o = ∅ ∧ ⟨ 𝑖 , 𝑎 ⟩ = ⟨ 𝑘 , 𝑗 ⟩ ) )
40 2on0 ⊢ 2o ≠ ∅
41 eqneqall ⊢ ( 2o = ∅ → ( 2o ≠ ∅ → 𝑎 ∈ ( Fmla ‘ suc ∅ ) ) )
42 40 41 mpi ⊢ ( 2o = ∅ → 𝑎 ∈ ( Fmla ‘ suc ∅ ) )
43 42 adantr ⊢ ( ( 2o = ∅ ∧ ⟨ 𝑖 , 𝑎 ⟩ = ⟨ 𝑘 , 𝑗 ⟩ ) → 𝑎 ∈ ( Fmla ‘ suc ∅ ) )
44 39 43 sylbi ⊢ ( ⟨ 2o , ⟨ 𝑖 , 𝑎 ⟩ ⟩ = ⟨ ∅ , ⟨ 𝑘 , 𝑗 ⟩ ⟩ → 𝑎 ∈ ( Fmla ‘ suc ∅ ) )
45 36 44 biimtrdi ⊢ ( ( 𝑘 ∈ ω ∧ 𝑗 ∈ ω ) → ( ∀𝑔 𝑖 𝑎 = ( 𝑘 ∈𝑔 𝑗 ) → 𝑎 ∈ ( Fmla ‘ suc ∅ ) ) )
46 45 rexlimdva ⊢ ( 𝑘 ∈ ω → ( ∃ 𝑗 ∈ ω ∀𝑔 𝑖 𝑎 = ( 𝑘 ∈𝑔 𝑗 ) → 𝑎 ∈ ( Fmla ‘ suc ∅ ) ) )
47 46 rexlimiv ⊢ ( ∃ 𝑘 ∈ ω ∃ 𝑗 ∈ ω ∀𝑔 𝑖 𝑎 = ( 𝑘 ∈𝑔 𝑗 ) → 𝑎 ∈ ( Fmla ‘ suc ∅ ) )
48 33 47 simplbiim ⊢ ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ ∅ ) → 𝑎 ∈ ( Fmla ‘ suc ∅ ) )
49 gonanegoal ⊢ ( 𝑢 ⊼𝑔 𝑣 ) ≠ ∀𝑔 𝑖 𝑎
50 eqneqall ⊢ ( ( 𝑢 ⊼𝑔 𝑣 ) = ∀𝑔 𝑖 𝑎 → ( ( 𝑢 ⊼𝑔 𝑣 ) ≠ ∀𝑔 𝑖 𝑎 → 𝑎 ∈ ( Fmla ‘ suc ∅ ) ) )
51 49 50 mpi ⊢ ( ( 𝑢 ⊼𝑔 𝑣 ) = ∀𝑔 𝑖 𝑎 → 𝑎 ∈ ( Fmla ‘ suc ∅ ) )
52 51 eqcoms ⊢ ( ∀𝑔 𝑖 𝑎 = ( 𝑢 ⊼𝑔 𝑣 ) → 𝑎 ∈ ( Fmla ‘ suc ∅ ) )
53 52 a1i ⊢ ( ( 𝑢 ∈ ( Fmla ‘ ∅ ) ∧ 𝑣 ∈ ( Fmla ‘ ∅ ) ) → ( ∀𝑔 𝑖 𝑎 = ( 𝑢 ⊼𝑔 𝑣 ) → 𝑎 ∈ ( Fmla ‘ suc ∅ ) ) )
54 53 rexlimdva ⊢ ( 𝑢 ∈ ( Fmla ‘ ∅ ) → ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) ∀𝑔 𝑖 𝑎 = ( 𝑢 ⊼𝑔 𝑣 ) → 𝑎 ∈ ( Fmla ‘ suc ∅ ) ) )
55 df-goal ⊢ ∀𝑔 𝑘 𝑢 = ⟨ 2o , ⟨ 𝑘 , 𝑢 ⟩ ⟩
56 25 55 eqeq12i ⊢ ( ∀𝑔 𝑖 𝑎 = ∀𝑔 𝑘 𝑢 ↔ ⟨ 2o , ⟨ 𝑖 , 𝑎 ⟩ ⟩ = ⟨ 2o , ⟨ 𝑘 , 𝑢 ⟩ ⟩ )
57 37 38 opth ⊢ ( ⟨ 2o , ⟨ 𝑖 , 𝑎 ⟩ ⟩ = ⟨ 2o , ⟨ 𝑘 , 𝑢 ⟩ ⟩ ↔ ( 2o = 2o ∧ ⟨ 𝑖 , 𝑎 ⟩ = ⟨ 𝑘 , 𝑢 ⟩ ) )
58 vex ⊢ 𝑖 ∈ V
59 vex ⊢ 𝑎 ∈ V
60 58 59 opth ⊢ ( ⟨ 𝑖 , 𝑎 ⟩ = ⟨ 𝑘 , 𝑢 ⟩ ↔ ( 𝑖 = 𝑘 ∧ 𝑎 = 𝑢 ) )
61 eleq1w ⊢ ( 𝑢 = 𝑎 → ( 𝑢 ∈ ( Fmla ‘ ∅ ) ↔ 𝑎 ∈ ( Fmla ‘ ∅ ) ) )
62 fmlasssuc ⊢ ( ∅ ∈ ω → ( Fmla ‘ ∅ ) ⊆ ( Fmla ‘ suc ∅ ) )
63 24 62 ax-mp ⊢ ( Fmla ‘ ∅ ) ⊆ ( Fmla ‘ suc ∅ )
64 63 sseli ⊢ ( 𝑎 ∈ ( Fmla ‘ ∅ ) → 𝑎 ∈ ( Fmla ‘ suc ∅ ) )
65 61 64 biimtrdi ⊢ ( 𝑢 = 𝑎 → ( 𝑢 ∈ ( Fmla ‘ ∅ ) → 𝑎 ∈ ( Fmla ‘ suc ∅ ) ) )
66 65 eqcoms ⊢ ( 𝑎 = 𝑢 → ( 𝑢 ∈ ( Fmla ‘ ∅ ) → 𝑎 ∈ ( Fmla ‘ suc ∅ ) ) )
67 60 66 simplbiim ⊢ ( ⟨ 𝑖 , 𝑎 ⟩ = ⟨ 𝑘 , 𝑢 ⟩ → ( 𝑢 ∈ ( Fmla ‘ ∅ ) → 𝑎 ∈ ( Fmla ‘ suc ∅ ) ) )
68 57 67 simplbiim ⊢ ( ⟨ 2o , ⟨ 𝑖 , 𝑎 ⟩ ⟩ = ⟨ 2o , ⟨ 𝑘 , 𝑢 ⟩ ⟩ → ( 𝑢 ∈ ( Fmla ‘ ∅ ) → 𝑎 ∈ ( Fmla ‘ suc ∅ ) ) )
69 68 com12 ⊢ ( 𝑢 ∈ ( Fmla ‘ ∅ ) → ( ⟨ 2o , ⟨ 𝑖 , 𝑎 ⟩ ⟩ = ⟨ 2o , ⟨ 𝑘 , 𝑢 ⟩ ⟩ → 𝑎 ∈ ( Fmla ‘ suc ∅ ) ) )
70 69 adantr ⊢ ( ( 𝑢 ∈ ( Fmla ‘ ∅ ) ∧ 𝑘 ∈ ω ) → ( ⟨ 2o , ⟨ 𝑖 , 𝑎 ⟩ ⟩ = ⟨ 2o , ⟨ 𝑘 , 𝑢 ⟩ ⟩ → 𝑎 ∈ ( Fmla ‘ suc ∅ ) ) )
71 56 70 biimtrid ⊢ ( ( 𝑢 ∈ ( Fmla ‘ ∅ ) ∧ 𝑘 ∈ ω ) → ( ∀𝑔 𝑖 𝑎 = ∀𝑔 𝑘 𝑢 → 𝑎 ∈ ( Fmla ‘ suc ∅ ) ) )
72 71 rexlimdva ⊢ ( 𝑢 ∈ ( Fmla ‘ ∅ ) → ( ∃ 𝑘 ∈ ω ∀𝑔 𝑖 𝑎 = ∀𝑔 𝑘 𝑢 → 𝑎 ∈ ( Fmla ‘ suc ∅ ) ) )
73 54 72 jaod ⊢ ( 𝑢 ∈ ( Fmla ‘ ∅ ) → ( ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) ∀𝑔 𝑖 𝑎 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑘 ∈ ω ∀𝑔 𝑖 𝑎 = ∀𝑔 𝑘 𝑢 ) → 𝑎 ∈ ( Fmla ‘ suc ∅ ) ) )
74 73 rexlimiv ⊢ ( ∃ 𝑢 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) ∀𝑔 𝑖 𝑎 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑘 ∈ ω ∀𝑔 𝑖 𝑎 = ∀𝑔 𝑘 𝑢 ) → 𝑎 ∈ ( Fmla ‘ suc ∅ ) )
75 48 74 jaoi ⊢ ( ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ ∅ ) ∨ ∃ 𝑢 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) ∀𝑔 𝑖 𝑎 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑘 ∈ ω ∀𝑔 𝑖 𝑎 = ∀𝑔 𝑘 𝑢 ) ) → 𝑎 ∈ ( Fmla ‘ suc ∅ ) )
76 29 75 sylbi ⊢ ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc ∅ ) → 𝑎 ∈ ( Fmla ‘ suc ∅ ) )
77 goalrlem ⊢ ( 𝑦 ∈ ω → ( ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc 𝑦 ) → 𝑎 ∈ ( Fmla ‘ suc 𝑦 ) ) → ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc suc 𝑦 ) → 𝑎 ∈ ( Fmla ‘ suc suc 𝑦 ) ) ) )
78 8 13 18 23 76 77 finds ⊢ ( 𝑛 ∈ ω → ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc 𝑛 ) → 𝑎 ∈ ( Fmla ‘ suc 𝑛 ) ) )
79 78 adantr ⊢ ( ( 𝑛 ∈ ω ∧ 𝑁 = suc 𝑛 ) → ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc 𝑛 ) → 𝑎 ∈ ( Fmla ‘ suc 𝑛 ) ) )
80 fveq2 ⊢ ( 𝑁 = suc 𝑛 → ( Fmla ‘ 𝑁 ) = ( Fmla ‘ suc 𝑛 ) )
81 80 eleq2d ⊢ ( 𝑁 = suc 𝑛 → ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ 𝑁 ) ↔ ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc 𝑛 ) ) )
82 80 eleq2d ⊢ ( 𝑁 = suc 𝑛 → ( 𝑎 ∈ ( Fmla ‘ 𝑁 ) ↔ 𝑎 ∈ ( Fmla ‘ suc 𝑛 ) ) )
83 81 82 imbi12d ⊢ ( 𝑁 = suc 𝑛 → ( ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ 𝑁 ) → 𝑎 ∈ ( Fmla ‘ 𝑁 ) ) ↔ ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc 𝑛 ) → 𝑎 ∈ ( Fmla ‘ suc 𝑛 ) ) ) )
84 83 adantl ⊢ ( ( 𝑛 ∈ ω ∧ 𝑁 = suc 𝑛 ) → ( ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ 𝑁 ) → 𝑎 ∈ ( Fmla ‘ 𝑁 ) ) ↔ ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc 𝑛 ) → 𝑎 ∈ ( Fmla ‘ suc 𝑛 ) ) ) )
85 79 84 mpbird ⊢ ( ( 𝑛 ∈ ω ∧ 𝑁 = suc 𝑛 ) → ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ 𝑁 ) → 𝑎 ∈ ( Fmla ‘ 𝑁 ) ) )
86 85 rexlimiva ⊢ ( ∃ 𝑛 ∈ ω 𝑁 = suc 𝑛 → ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ 𝑁 ) → 𝑎 ∈ ( Fmla ‘ 𝑁 ) ) )
87 3 86 syl ⊢ ( ( 𝑁 ∈ ω ∧ 𝑁 ≠ ∅ ) → ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ 𝑁 ) → 𝑎 ∈ ( Fmla ‘ 𝑁 ) ) )
88 87 impancom ⊢ ( ( 𝑁 ∈ ω ∧ ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ 𝑁 ) ) → ( 𝑁 ≠ ∅ → 𝑎 ∈ ( Fmla ‘ 𝑁 ) ) )
89 2 88 mpd ⊢ ( ( 𝑁 ∈ ω ∧ ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ 𝑁 ) ) → 𝑎 ∈ ( Fmla ‘ 𝑁 ) )