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

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 biimtrdi ⊢ ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → ( ( 𝑎 ⊼𝑔 𝑏 ) = ( 𝑖 ∈𝑔 𝑗 ) → ( 𝑎 ∈ ( 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 biimtrdi ⊢ ( ⟨ 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 ‘ 𝑁 ) ) )