Metamath Proof Explorer


Theorem gonar

Description: If the "Godel-set of NAND" applied to classes is a Godel formula, the classes are also Godel formulas. Remark: The reverse is not valid for A or B being of the same height as the "Godel-set of NAND". (Contributed by AV, 21-Oct-2023)

Ref Expression
Assertion gonar ( ( 𝑁 ∈ ω ∧ ( 𝑎𝑔 𝑏 ) ∈ ( Fmla ‘ 𝑁 ) ) → ( 𝑎 ∈ ( Fmla ‘ 𝑁 ) ∧ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 gonan0 ( ( 𝑎𝑔 𝑏 ) ∈ ( 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 5 eleq2d ( 𝑑 = ∅ → ( 𝑏 ∈ ( Fmla ‘ suc 𝑑 ) ↔ 𝑏 ∈ ( Fmla ‘ suc ∅ ) ) )
9 7 8 anbi12d ( 𝑑 = ∅ → ( ( 𝑎 ∈ ( Fmla ‘ suc 𝑑 ) ∧ 𝑏 ∈ ( Fmla ‘ suc 𝑑 ) ) ↔ ( 𝑎 ∈ ( Fmla ‘ suc ∅ ) ∧ 𝑏 ∈ ( Fmla ‘ suc ∅ ) ) ) )
10 6 9 imbi12d ( 𝑑 = ∅ → ( ( ( 𝑎𝑔 𝑏 ) ∈ ( Fmla ‘ suc 𝑑 ) → ( 𝑎 ∈ ( Fmla ‘ suc 𝑑 ) ∧ 𝑏 ∈ ( Fmla ‘ suc 𝑑 ) ) ) ↔ ( ( 𝑎𝑔 𝑏 ) ∈ ( Fmla ‘ suc ∅ ) → ( 𝑎 ∈ ( Fmla ‘ suc ∅ ) ∧ 𝑏 ∈ ( Fmla ‘ suc ∅ ) ) ) ) )
11 suceq ( 𝑑 = 𝑐 → suc 𝑑 = suc 𝑐 )
12 11 fveq2d ( 𝑑 = 𝑐 → ( Fmla ‘ suc 𝑑 ) = ( Fmla ‘ suc 𝑐 ) )
13 12 eleq2d ( 𝑑 = 𝑐 → ( ( 𝑎𝑔 𝑏 ) ∈ ( Fmla ‘ suc 𝑑 ) ↔ ( 𝑎𝑔 𝑏 ) ∈ ( Fmla ‘ suc 𝑐 ) ) )
14 12 eleq2d ( 𝑑 = 𝑐 → ( 𝑎 ∈ ( Fmla ‘ suc 𝑑 ) ↔ 𝑎 ∈ ( Fmla ‘ suc 𝑐 ) ) )
15 12 eleq2d ( 𝑑 = 𝑐 → ( 𝑏 ∈ ( Fmla ‘ suc 𝑑 ) ↔ 𝑏 ∈ ( Fmla ‘ suc 𝑐 ) ) )
16 14 15 anbi12d ( 𝑑 = 𝑐 → ( ( 𝑎 ∈ ( Fmla ‘ suc 𝑑 ) ∧ 𝑏 ∈ ( Fmla ‘ suc 𝑑 ) ) ↔ ( 𝑎 ∈ ( Fmla ‘ suc 𝑐 ) ∧ 𝑏 ∈ ( Fmla ‘ suc 𝑐 ) ) ) )
17 13 16 imbi12d ( 𝑑 = 𝑐 → ( ( ( 𝑎𝑔 𝑏 ) ∈ ( Fmla ‘ suc 𝑑 ) → ( 𝑎 ∈ ( Fmla ‘ suc 𝑑 ) ∧ 𝑏 ∈ ( Fmla ‘ suc 𝑑 ) ) ) ↔ ( ( 𝑎𝑔 𝑏 ) ∈ ( Fmla ‘ suc 𝑐 ) → ( 𝑎 ∈ ( Fmla ‘ suc 𝑐 ) ∧ 𝑏 ∈ ( Fmla ‘ suc 𝑐 ) ) ) ) )
18 suceq ( 𝑑 = suc 𝑐 → suc 𝑑 = suc suc 𝑐 )
19 18 fveq2d ( 𝑑 = suc 𝑐 → ( Fmla ‘ suc 𝑑 ) = ( Fmla ‘ suc suc 𝑐 ) )
20 19 eleq2d ( 𝑑 = suc 𝑐 → ( ( 𝑎𝑔 𝑏 ) ∈ ( Fmla ‘ suc 𝑑 ) ↔ ( 𝑎𝑔 𝑏 ) ∈ ( Fmla ‘ suc suc 𝑐 ) ) )
21 19 eleq2d ( 𝑑 = suc 𝑐 → ( 𝑎 ∈ ( Fmla ‘ suc 𝑑 ) ↔ 𝑎 ∈ ( Fmla ‘ suc suc 𝑐 ) ) )
22 19 eleq2d ( 𝑑 = suc 𝑐 → ( 𝑏 ∈ ( Fmla ‘ suc 𝑑 ) ↔ 𝑏 ∈ ( Fmla ‘ suc suc 𝑐 ) ) )
23 21 22 anbi12d ( 𝑑 = suc 𝑐 → ( ( 𝑎 ∈ ( Fmla ‘ suc 𝑑 ) ∧ 𝑏 ∈ ( Fmla ‘ suc 𝑑 ) ) ↔ ( 𝑎 ∈ ( Fmla ‘ suc suc 𝑐 ) ∧ 𝑏 ∈ ( Fmla ‘ suc suc 𝑐 ) ) ) )
24 20 23 imbi12d ( 𝑑 = suc 𝑐 → ( ( ( 𝑎𝑔 𝑏 ) ∈ ( Fmla ‘ suc 𝑑 ) → ( 𝑎 ∈ ( Fmla ‘ suc 𝑑 ) ∧ 𝑏 ∈ ( Fmla ‘ suc 𝑑 ) ) ) ↔ ( ( 𝑎𝑔 𝑏 ) ∈ ( Fmla ‘ suc suc 𝑐 ) → ( 𝑎 ∈ ( Fmla ‘ suc suc 𝑐 ) ∧ 𝑏 ∈ ( Fmla ‘ suc suc 𝑐 ) ) ) ) )
25 suceq ( 𝑑 = 𝑥 → suc 𝑑 = suc 𝑥 )
26 25 fveq2d ( 𝑑 = 𝑥 → ( Fmla ‘ suc 𝑑 ) = ( Fmla ‘ suc 𝑥 ) )
27 26 eleq2d ( 𝑑 = 𝑥 → ( ( 𝑎𝑔 𝑏 ) ∈ ( Fmla ‘ suc 𝑑 ) ↔ ( 𝑎𝑔 𝑏 ) ∈ ( Fmla ‘ suc 𝑥 ) ) )
28 26 eleq2d ( 𝑑 = 𝑥 → ( 𝑎 ∈ ( Fmla ‘ suc 𝑑 ) ↔ 𝑎 ∈ ( Fmla ‘ suc 𝑥 ) ) )
29 26 eleq2d ( 𝑑 = 𝑥 → ( 𝑏 ∈ ( Fmla ‘ suc 𝑑 ) ↔ 𝑏 ∈ ( Fmla ‘ suc 𝑥 ) ) )
30 28 29 anbi12d ( 𝑑 = 𝑥 → ( ( 𝑎 ∈ ( Fmla ‘ suc 𝑑 ) ∧ 𝑏 ∈ ( Fmla ‘ suc 𝑑 ) ) ↔ ( 𝑎 ∈ ( Fmla ‘ suc 𝑥 ) ∧ 𝑏 ∈ ( Fmla ‘ suc 𝑥 ) ) ) )
31 27 30 imbi12d ( 𝑑 = 𝑥 → ( ( ( 𝑎𝑔 𝑏 ) ∈ ( Fmla ‘ suc 𝑑 ) → ( 𝑎 ∈ ( Fmla ‘ suc 𝑑 ) ∧ 𝑏 ∈ ( Fmla ‘ suc 𝑑 ) ) ) ↔ ( ( 𝑎𝑔 𝑏 ) ∈ ( Fmla ‘ suc 𝑥 ) → ( 𝑎 ∈ ( Fmla ‘ suc 𝑥 ) ∧ 𝑏 ∈ ( Fmla ‘ suc 𝑥 ) ) ) ) )
32 peano1 ∅ ∈ ω
33 ovex ( 𝑎𝑔 𝑏 ) ∈ V
34 isfmlasuc ( ( ∅ ∈ ω ∧ ( 𝑎𝑔 𝑏 ) ∈ V ) → ( ( 𝑎𝑔 𝑏 ) ∈ ( Fmla ‘ suc ∅ ) ↔ ( ( 𝑎𝑔 𝑏 ) ∈ ( Fmla ‘ ∅ ) ∨ ∃ 𝑢 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) ( 𝑎𝑔 𝑏 ) = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω ( 𝑎𝑔 𝑏 ) = ∀𝑔 𝑖 𝑢 ) ) ) )
35 32 33 34 mp2an ( ( 𝑎𝑔 𝑏 ) ∈ ( Fmla ‘ suc ∅ ) ↔ ( ( 𝑎𝑔 𝑏 ) ∈ ( Fmla ‘ ∅ ) ∨ ∃ 𝑢 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) ( 𝑎𝑔 𝑏 ) = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω ( 𝑎𝑔 𝑏 ) = ∀𝑔 𝑖 𝑢 ) ) )
36 eqeq1 ( 𝑥 = ( 𝑎𝑔 𝑏 ) → ( 𝑥 = ( 𝑖𝑔 𝑗 ) ↔ ( 𝑎𝑔 𝑏 ) = ( 𝑖𝑔 𝑗 ) ) )
37 36 2rexbidv ( 𝑥 = ( 𝑎𝑔 𝑏 ) → ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖𝑔 𝑗 ) ↔ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑎𝑔 𝑏 ) = ( 𝑖𝑔 𝑗 ) ) )
38 fmla0 ( Fmla ‘ ∅ ) = { 𝑥 ∈ V ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖𝑔 𝑗 ) }
39 37 38 elrab2 ( ( 𝑎𝑔 𝑏 ) ∈ ( Fmla ‘ ∅ ) ↔ ( ( 𝑎𝑔 𝑏 ) ∈ V ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑎𝑔 𝑏 ) = ( 𝑖𝑔 𝑗 ) ) )
40 gonafv ( ( 𝑎 ∈ V ∧ 𝑏 ∈ V ) → ( 𝑎𝑔 𝑏 ) = ⟨ 1o , ⟨ 𝑎 , 𝑏 ⟩ ⟩ )
41 40 el2v ( 𝑎𝑔 𝑏 ) = ⟨ 1o , ⟨ 𝑎 , 𝑏 ⟩ ⟩
42 41 a1i ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → ( 𝑎𝑔 𝑏 ) = ⟨ 1o , ⟨ 𝑎 , 𝑏 ⟩ ⟩ )
43 goel ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → ( 𝑖𝑔 𝑗 ) = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ )
44 42 43 eqeq12d ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → ( ( 𝑎𝑔 𝑏 ) = ( 𝑖𝑔 𝑗 ) ↔ ⟨ 1o , ⟨ 𝑎 , 𝑏 ⟩ ⟩ = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ ) )
45 1oex 1o ∈ V
46 opex 𝑎 , 𝑏 ⟩ ∈ V
47 45 46 opth ( ⟨ 1o , ⟨ 𝑎 , 𝑏 ⟩ ⟩ = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ ↔ ( 1o = ∅ ∧ ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑖 , 𝑗 ⟩ ) )
48 1n0 1o ≠ ∅
49 eqneqall ( 1o = ∅ → ( 1o ≠ ∅ → ( 𝑎 ∈ ( Fmla ‘ suc ∅ ) ∧ 𝑏 ∈ ( Fmla ‘ suc ∅ ) ) ) )
50 48 49 mpi ( 1o = ∅ → ( 𝑎 ∈ ( Fmla ‘ suc ∅ ) ∧ 𝑏 ∈ ( Fmla ‘ suc ∅ ) ) )
51 50 adantr ( ( 1o = ∅ ∧ ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑖 , 𝑗 ⟩ ) → ( 𝑎 ∈ ( Fmla ‘ suc ∅ ) ∧ 𝑏 ∈ ( Fmla ‘ suc ∅ ) ) )
52 47 51 sylbi ( ⟨ 1o , ⟨ 𝑎 , 𝑏 ⟩ ⟩ = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ → ( 𝑎 ∈ ( Fmla ‘ suc ∅ ) ∧ 𝑏 ∈ ( Fmla ‘ suc ∅ ) ) )
53 44 52 syl6bi ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → ( ( 𝑎𝑔 𝑏 ) = ( 𝑖𝑔 𝑗 ) → ( 𝑎 ∈ ( Fmla ‘ suc ∅ ) ∧ 𝑏 ∈ ( Fmla ‘ suc ∅ ) ) ) )
54 53 rexlimdva ( 𝑖 ∈ ω → ( ∃ 𝑗 ∈ ω ( 𝑎𝑔 𝑏 ) = ( 𝑖𝑔 𝑗 ) → ( 𝑎 ∈ ( Fmla ‘ suc ∅ ) ∧ 𝑏 ∈ ( Fmla ‘ suc ∅ ) ) ) )
55 54 rexlimiv ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑎𝑔 𝑏 ) = ( 𝑖𝑔 𝑗 ) → ( 𝑎 ∈ ( Fmla ‘ suc ∅ ) ∧ 𝑏 ∈ ( Fmla ‘ suc ∅ ) ) )
56 55 adantl ( ( ( 𝑎𝑔 𝑏 ) ∈ V ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑎𝑔 𝑏 ) = ( 𝑖𝑔 𝑗 ) ) → ( 𝑎 ∈ ( Fmla ‘ suc ∅ ) ∧ 𝑏 ∈ ( Fmla ‘ suc ∅ ) ) )
57 39 56 sylbi ( ( 𝑎𝑔 𝑏 ) ∈ ( Fmla ‘ ∅ ) → ( 𝑎 ∈ ( Fmla ‘ suc ∅ ) ∧ 𝑏 ∈ ( Fmla ‘ suc ∅ ) ) )
58 41 a1i ( ( 𝑢 ∈ ( Fmla ‘ ∅ ) ∧ 𝑣 ∈ ( Fmla ‘ ∅ ) ) → ( 𝑎𝑔 𝑏 ) = ⟨ 1o , ⟨ 𝑎 , 𝑏 ⟩ ⟩ )
59 gonafv ( ( 𝑢 ∈ ( Fmla ‘ ∅ ) ∧ 𝑣 ∈ ( Fmla ‘ ∅ ) ) → ( 𝑢𝑔 𝑣 ) = ⟨ 1o , ⟨ 𝑢 , 𝑣 ⟩ ⟩ )
60 58 59 eqeq12d ( ( 𝑢 ∈ ( Fmla ‘ ∅ ) ∧ 𝑣 ∈ ( Fmla ‘ ∅ ) ) → ( ( 𝑎𝑔 𝑏 ) = ( 𝑢𝑔 𝑣 ) ↔ ⟨ 1o , ⟨ 𝑎 , 𝑏 ⟩ ⟩ = ⟨ 1o , ⟨ 𝑢 , 𝑣 ⟩ ⟩ ) )
61 45 46 opth ( ⟨ 1o , ⟨ 𝑎 , 𝑏 ⟩ ⟩ = ⟨ 1o , ⟨ 𝑢 , 𝑣 ⟩ ⟩ ↔ ( 1o = 1o ∧ ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑢 , 𝑣 ⟩ ) )
62 vex 𝑎 ∈ V
63 vex 𝑏 ∈ V
64 62 63 opth ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑢 , 𝑣 ⟩ ↔ ( 𝑎 = 𝑢𝑏 = 𝑣 ) )
65 simpl ( ( 𝑎 = 𝑢𝑏 = 𝑣 ) → 𝑎 = 𝑢 )
66 65 equcomd ( ( 𝑎 = 𝑢𝑏 = 𝑣 ) → 𝑢 = 𝑎 )
67 66 eleq1d ( ( 𝑎 = 𝑢𝑏 = 𝑣 ) → ( 𝑢 ∈ ( Fmla ‘ ∅ ) ↔ 𝑎 ∈ ( Fmla ‘ ∅ ) ) )
68 simpr ( ( 𝑎 = 𝑢𝑏 = 𝑣 ) → 𝑏 = 𝑣 )
69 68 equcomd ( ( 𝑎 = 𝑢𝑏 = 𝑣 ) → 𝑣 = 𝑏 )
70 69 eleq1d ( ( 𝑎 = 𝑢𝑏 = 𝑣 ) → ( 𝑣 ∈ ( Fmla ‘ ∅ ) ↔ 𝑏 ∈ ( Fmla ‘ ∅ ) ) )
71 67 70 anbi12d ( ( 𝑎 = 𝑢𝑏 = 𝑣 ) → ( ( 𝑢 ∈ ( Fmla ‘ ∅ ) ∧ 𝑣 ∈ ( Fmla ‘ ∅ ) ) ↔ ( 𝑎 ∈ ( Fmla ‘ ∅ ) ∧ 𝑏 ∈ ( Fmla ‘ ∅ ) ) ) )
72 64 71 sylbi ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑢 , 𝑣 ⟩ → ( ( 𝑢 ∈ ( Fmla ‘ ∅ ) ∧ 𝑣 ∈ ( Fmla ‘ ∅ ) ) ↔ ( 𝑎 ∈ ( Fmla ‘ ∅ ) ∧ 𝑏 ∈ ( Fmla ‘ ∅ ) ) ) )
73 72 adantl ( ( 1o = 1o ∧ ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑢 , 𝑣 ⟩ ) → ( ( 𝑢 ∈ ( Fmla ‘ ∅ ) ∧ 𝑣 ∈ ( Fmla ‘ ∅ ) ) ↔ ( 𝑎 ∈ ( Fmla ‘ ∅ ) ∧ 𝑏 ∈ ( Fmla ‘ ∅ ) ) ) )
74 61 73 sylbi ( ⟨ 1o , ⟨ 𝑎 , 𝑏 ⟩ ⟩ = ⟨ 1o , ⟨ 𝑢 , 𝑣 ⟩ ⟩ → ( ( 𝑢 ∈ ( Fmla ‘ ∅ ) ∧ 𝑣 ∈ ( Fmla ‘ ∅ ) ) ↔ ( 𝑎 ∈ ( Fmla ‘ ∅ ) ∧ 𝑏 ∈ ( Fmla ‘ ∅ ) ) ) )
75 fmlasssuc ( ∅ ∈ ω → ( Fmla ‘ ∅ ) ⊆ ( Fmla ‘ suc ∅ ) )
76 32 75 ax-mp ( Fmla ‘ ∅ ) ⊆ ( Fmla ‘ suc ∅ )
77 76 sseli ( 𝑎 ∈ ( Fmla ‘ ∅ ) → 𝑎 ∈ ( Fmla ‘ suc ∅ ) )
78 76 sseli ( 𝑏 ∈ ( Fmla ‘ ∅ ) → 𝑏 ∈ ( Fmla ‘ suc ∅ ) )
79 77 78 anim12i ( ( 𝑎 ∈ ( Fmla ‘ ∅ ) ∧ 𝑏 ∈ ( Fmla ‘ ∅ ) ) → ( 𝑎 ∈ ( Fmla ‘ suc ∅ ) ∧ 𝑏 ∈ ( Fmla ‘ suc ∅ ) ) )
80 74 79 syl6bi ( ⟨ 1o , ⟨ 𝑎 , 𝑏 ⟩ ⟩ = ⟨ 1o , ⟨ 𝑢 , 𝑣 ⟩ ⟩ → ( ( 𝑢 ∈ ( Fmla ‘ ∅ ) ∧ 𝑣 ∈ ( Fmla ‘ ∅ ) ) → ( 𝑎 ∈ ( Fmla ‘ suc ∅ ) ∧ 𝑏 ∈ ( Fmla ‘ suc ∅ ) ) ) )
81 80 com12 ( ( 𝑢 ∈ ( Fmla ‘ ∅ ) ∧ 𝑣 ∈ ( Fmla ‘ ∅ ) ) → ( ⟨ 1o , ⟨ 𝑎 , 𝑏 ⟩ ⟩ = ⟨ 1o , ⟨ 𝑢 , 𝑣 ⟩ ⟩ → ( 𝑎 ∈ ( Fmla ‘ suc ∅ ) ∧ 𝑏 ∈ ( Fmla ‘ suc ∅ ) ) ) )
82 60 81 sylbid ( ( 𝑢 ∈ ( Fmla ‘ ∅ ) ∧ 𝑣 ∈ ( Fmla ‘ ∅ ) ) → ( ( 𝑎𝑔 𝑏 ) = ( 𝑢𝑔 𝑣 ) → ( 𝑎 ∈ ( Fmla ‘ suc ∅ ) ∧ 𝑏 ∈ ( Fmla ‘ suc ∅ ) ) ) )
83 82 rexlimdva ( 𝑢 ∈ ( Fmla ‘ ∅ ) → ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) ( 𝑎𝑔 𝑏 ) = ( 𝑢𝑔 𝑣 ) → ( 𝑎 ∈ ( Fmla ‘ suc ∅ ) ∧ 𝑏 ∈ ( Fmla ‘ suc ∅ ) ) ) )
84 gonanegoal ( 𝑎𝑔 𝑏 ) ≠ ∀𝑔 𝑖 𝑢
85 eqneqall ( ( 𝑎𝑔 𝑏 ) = ∀𝑔 𝑖 𝑢 → ( ( 𝑎𝑔 𝑏 ) ≠ ∀𝑔 𝑖 𝑢 → ( 𝑎 ∈ ( Fmla ‘ suc ∅ ) ∧ 𝑏 ∈ ( Fmla ‘ suc ∅ ) ) ) )
86 84 85 mpi ( ( 𝑎𝑔 𝑏 ) = ∀𝑔 𝑖 𝑢 → ( 𝑎 ∈ ( Fmla ‘ suc ∅ ) ∧ 𝑏 ∈ ( Fmla ‘ suc ∅ ) ) )
87 86 a1i ( ( 𝑢 ∈ ( Fmla ‘ ∅ ) ∧ 𝑖 ∈ ω ) → ( ( 𝑎𝑔 𝑏 ) = ∀𝑔 𝑖 𝑢 → ( 𝑎 ∈ ( Fmla ‘ suc ∅ ) ∧ 𝑏 ∈ ( Fmla ‘ suc ∅ ) ) ) )
88 87 rexlimdva ( 𝑢 ∈ ( Fmla ‘ ∅ ) → ( ∃ 𝑖 ∈ ω ( 𝑎𝑔 𝑏 ) = ∀𝑔 𝑖 𝑢 → ( 𝑎 ∈ ( Fmla ‘ suc ∅ ) ∧ 𝑏 ∈ ( Fmla ‘ suc ∅ ) ) ) )
89 83 88 jaod ( 𝑢 ∈ ( Fmla ‘ ∅ ) → ( ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) ( 𝑎𝑔 𝑏 ) = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω ( 𝑎𝑔 𝑏 ) = ∀𝑔 𝑖 𝑢 ) → ( 𝑎 ∈ ( Fmla ‘ suc ∅ ) ∧ 𝑏 ∈ ( Fmla ‘ suc ∅ ) ) ) )
90 89 rexlimiv ( ∃ 𝑢 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) ( 𝑎𝑔 𝑏 ) = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω ( 𝑎𝑔 𝑏 ) = ∀𝑔 𝑖 𝑢 ) → ( 𝑎 ∈ ( Fmla ‘ suc ∅ ) ∧ 𝑏 ∈ ( Fmla ‘ suc ∅ ) ) )
91 57 90 jaoi ( ( ( 𝑎𝑔 𝑏 ) ∈ ( Fmla ‘ ∅ ) ∨ ∃ 𝑢 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) ( 𝑎𝑔 𝑏 ) = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω ( 𝑎𝑔 𝑏 ) = ∀𝑔 𝑖 𝑢 ) ) → ( 𝑎 ∈ ( Fmla ‘ suc ∅ ) ∧ 𝑏 ∈ ( Fmla ‘ suc ∅ ) ) )
92 35 91 sylbi ( ( 𝑎𝑔 𝑏 ) ∈ ( Fmla ‘ suc ∅ ) → ( 𝑎 ∈ ( Fmla ‘ suc ∅ ) ∧ 𝑏 ∈ ( Fmla ‘ suc ∅ ) ) )
93 gonarlem ( 𝑐 ∈ ω → ( ( ( 𝑎𝑔 𝑏 ) ∈ ( Fmla ‘ suc 𝑐 ) → ( 𝑎 ∈ ( Fmla ‘ suc 𝑐 ) ∧ 𝑏 ∈ ( Fmla ‘ suc 𝑐 ) ) ) → ( ( 𝑎𝑔 𝑏 ) ∈ ( Fmla ‘ suc suc 𝑐 ) → ( 𝑎 ∈ ( Fmla ‘ suc suc 𝑐 ) ∧ 𝑏 ∈ ( Fmla ‘ suc suc 𝑐 ) ) ) ) )
94 10 17 24 31 92 93 finds ( 𝑥 ∈ ω → ( ( 𝑎𝑔 𝑏 ) ∈ ( Fmla ‘ suc 𝑥 ) → ( 𝑎 ∈ ( Fmla ‘ suc 𝑥 ) ∧ 𝑏 ∈ ( Fmla ‘ suc 𝑥 ) ) ) )
95 94 adantr ( ( 𝑥 ∈ ω ∧ 𝑁 = suc 𝑥 ) → ( ( 𝑎𝑔 𝑏 ) ∈ ( Fmla ‘ suc 𝑥 ) → ( 𝑎 ∈ ( Fmla ‘ suc 𝑥 ) ∧ 𝑏 ∈ ( Fmla ‘ suc 𝑥 ) ) ) )
96 fveq2 ( 𝑁 = suc 𝑥 → ( Fmla ‘ 𝑁 ) = ( Fmla ‘ suc 𝑥 ) )
97 96 eleq2d ( 𝑁 = suc 𝑥 → ( ( 𝑎𝑔 𝑏 ) ∈ ( Fmla ‘ 𝑁 ) ↔ ( 𝑎𝑔 𝑏 ) ∈ ( Fmla ‘ suc 𝑥 ) ) )
98 96 eleq2d ( 𝑁 = suc 𝑥 → ( 𝑎 ∈ ( Fmla ‘ 𝑁 ) ↔ 𝑎 ∈ ( Fmla ‘ suc 𝑥 ) ) )
99 96 eleq2d ( 𝑁 = suc 𝑥 → ( 𝑏 ∈ ( Fmla ‘ 𝑁 ) ↔ 𝑏 ∈ ( Fmla ‘ suc 𝑥 ) ) )
100 98 99 anbi12d ( 𝑁 = suc 𝑥 → ( ( 𝑎 ∈ ( Fmla ‘ 𝑁 ) ∧ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ) ↔ ( 𝑎 ∈ ( Fmla ‘ suc 𝑥 ) ∧ 𝑏 ∈ ( Fmla ‘ suc 𝑥 ) ) ) )
101 97 100 imbi12d ( 𝑁 = suc 𝑥 → ( ( ( 𝑎𝑔 𝑏 ) ∈ ( Fmla ‘ 𝑁 ) → ( 𝑎 ∈ ( Fmla ‘ 𝑁 ) ∧ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ) ) ↔ ( ( 𝑎𝑔 𝑏 ) ∈ ( Fmla ‘ suc 𝑥 ) → ( 𝑎 ∈ ( Fmla ‘ suc 𝑥 ) ∧ 𝑏 ∈ ( Fmla ‘ suc 𝑥 ) ) ) ) )
102 101 adantl ( ( 𝑥 ∈ ω ∧ 𝑁 = suc 𝑥 ) → ( ( ( 𝑎𝑔 𝑏 ) ∈ ( Fmla ‘ 𝑁 ) → ( 𝑎 ∈ ( Fmla ‘ 𝑁 ) ∧ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ) ) ↔ ( ( 𝑎𝑔 𝑏 ) ∈ ( Fmla ‘ suc 𝑥 ) → ( 𝑎 ∈ ( Fmla ‘ suc 𝑥 ) ∧ 𝑏 ∈ ( Fmla ‘ suc 𝑥 ) ) ) ) )
103 95 102 mpbird ( ( 𝑥 ∈ ω ∧ 𝑁 = suc 𝑥 ) → ( ( 𝑎𝑔 𝑏 ) ∈ ( Fmla ‘ 𝑁 ) → ( 𝑎 ∈ ( Fmla ‘ 𝑁 ) ∧ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ) ) )
104 103 rexlimiva ( ∃ 𝑥 ∈ ω 𝑁 = suc 𝑥 → ( ( 𝑎𝑔 𝑏 ) ∈ ( Fmla ‘ 𝑁 ) → ( 𝑎 ∈ ( Fmla ‘ 𝑁 ) ∧ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ) ) )
105 3 104 syl ( ( 𝑁 ∈ ω ∧ 𝑁 ≠ ∅ ) → ( ( 𝑎𝑔 𝑏 ) ∈ ( Fmla ‘ 𝑁 ) → ( 𝑎 ∈ ( Fmla ‘ 𝑁 ) ∧ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ) ) )
106 105 impancom ( ( 𝑁 ∈ ω ∧ ( 𝑎𝑔 𝑏 ) ∈ ( Fmla ‘ 𝑁 ) ) → ( 𝑁 ≠ ∅ → ( 𝑎 ∈ ( Fmla ‘ 𝑁 ) ∧ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ) ) )
107 2 106 mpd ( ( 𝑁 ∈ ω ∧ ( 𝑎𝑔 𝑏 ) ∈ ( Fmla ‘ 𝑁 ) ) → ( 𝑎 ∈ ( Fmla ‘ 𝑁 ) ∧ 𝑏 ∈ ( Fmla ‘ 𝑁 ) ) )