Metamath Proof Explorer


Theorem gonarlem

Description: Lemma for gonar (induction step). (Contributed by AV, 21-Oct-2023)

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

Proof

Step Hyp Ref Expression
1 peano2 ( 𝑁 ∈ ω → suc 𝑁 ∈ ω )
2 ovexd ( 𝑁 ∈ ω → ( 𝑎𝑔 𝑏 ) ∈ V )
3 isfmlasuc ( ( suc 𝑁 ∈ ω ∧ ( 𝑎𝑔 𝑏 ) ∈ V ) → ( ( 𝑎𝑔 𝑏 ) ∈ ( Fmla ‘ suc suc 𝑁 ) ↔ ( ( 𝑎𝑔 𝑏 ) ∈ ( Fmla ‘ suc 𝑁 ) ∨ ∃ 𝑢 ∈ ( Fmla ‘ suc 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) ( 𝑎𝑔 𝑏 ) = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω ( 𝑎𝑔 𝑏 ) = ∀𝑔 𝑖 𝑢 ) ) ) )
4 1 2 3 syl2anc ( 𝑁 ∈ ω → ( ( 𝑎𝑔 𝑏 ) ∈ ( Fmla ‘ suc suc 𝑁 ) ↔ ( ( 𝑎𝑔 𝑏 ) ∈ ( Fmla ‘ suc 𝑁 ) ∨ ∃ 𝑢 ∈ ( Fmla ‘ suc 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) ( 𝑎𝑔 𝑏 ) = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω ( 𝑎𝑔 𝑏 ) = ∀𝑔 𝑖 𝑢 ) ) ) )
5 4 adantr ( ( 𝑁 ∈ ω ∧ ( ( 𝑎𝑔 𝑏 ) ∈ ( Fmla ‘ suc 𝑁 ) → ( 𝑎 ∈ ( Fmla ‘ suc 𝑁 ) ∧ 𝑏 ∈ ( Fmla ‘ suc 𝑁 ) ) ) ) → ( ( 𝑎𝑔 𝑏 ) ∈ ( Fmla ‘ suc suc 𝑁 ) ↔ ( ( 𝑎𝑔 𝑏 ) ∈ ( Fmla ‘ suc 𝑁 ) ∨ ∃ 𝑢 ∈ ( Fmla ‘ suc 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) ( 𝑎𝑔 𝑏 ) = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω ( 𝑎𝑔 𝑏 ) = ∀𝑔 𝑖 𝑢 ) ) ) )
6 fmlasssuc ( suc 𝑁 ∈ ω → ( Fmla ‘ suc 𝑁 ) ⊆ ( Fmla ‘ suc suc 𝑁 ) )
7 1 6 syl ( 𝑁 ∈ ω → ( Fmla ‘ suc 𝑁 ) ⊆ ( Fmla ‘ suc suc 𝑁 ) )
8 7 sseld ( 𝑁 ∈ ω → ( 𝑎 ∈ ( Fmla ‘ suc 𝑁 ) → 𝑎 ∈ ( Fmla ‘ suc suc 𝑁 ) ) )
9 7 sseld ( 𝑁 ∈ ω → ( 𝑏 ∈ ( Fmla ‘ suc 𝑁 ) → 𝑏 ∈ ( Fmla ‘ suc suc 𝑁 ) ) )
10 8 9 anim12d ( 𝑁 ∈ ω → ( ( 𝑎 ∈ ( Fmla ‘ suc 𝑁 ) ∧ 𝑏 ∈ ( Fmla ‘ suc 𝑁 ) ) → ( 𝑎 ∈ ( Fmla ‘ suc suc 𝑁 ) ∧ 𝑏 ∈ ( Fmla ‘ suc suc 𝑁 ) ) ) )
11 10 com12 ( ( 𝑎 ∈ ( Fmla ‘ suc 𝑁 ) ∧ 𝑏 ∈ ( Fmla ‘ suc 𝑁 ) ) → ( 𝑁 ∈ ω → ( 𝑎 ∈ ( Fmla ‘ suc suc 𝑁 ) ∧ 𝑏 ∈ ( Fmla ‘ suc suc 𝑁 ) ) ) )
12 11 imim2i ( ( ( 𝑎𝑔 𝑏 ) ∈ ( Fmla ‘ suc 𝑁 ) → ( 𝑎 ∈ ( Fmla ‘ suc 𝑁 ) ∧ 𝑏 ∈ ( Fmla ‘ suc 𝑁 ) ) ) → ( ( 𝑎𝑔 𝑏 ) ∈ ( Fmla ‘ suc 𝑁 ) → ( 𝑁 ∈ ω → ( 𝑎 ∈ ( Fmla ‘ suc suc 𝑁 ) ∧ 𝑏 ∈ ( Fmla ‘ suc suc 𝑁 ) ) ) ) )
13 12 com23 ( ( ( 𝑎𝑔 𝑏 ) ∈ ( Fmla ‘ suc 𝑁 ) → ( 𝑎 ∈ ( Fmla ‘ suc 𝑁 ) ∧ 𝑏 ∈ ( Fmla ‘ suc 𝑁 ) ) ) → ( 𝑁 ∈ ω → ( ( 𝑎𝑔 𝑏 ) ∈ ( Fmla ‘ suc 𝑁 ) → ( 𝑎 ∈ ( Fmla ‘ suc suc 𝑁 ) ∧ 𝑏 ∈ ( Fmla ‘ suc suc 𝑁 ) ) ) ) )
14 13 impcom ( ( 𝑁 ∈ ω ∧ ( ( 𝑎𝑔 𝑏 ) ∈ ( Fmla ‘ suc 𝑁 ) → ( 𝑎 ∈ ( Fmla ‘ suc 𝑁 ) ∧ 𝑏 ∈ ( Fmla ‘ suc 𝑁 ) ) ) ) → ( ( 𝑎𝑔 𝑏 ) ∈ ( Fmla ‘ suc 𝑁 ) → ( 𝑎 ∈ ( Fmla ‘ suc suc 𝑁 ) ∧ 𝑏 ∈ ( Fmla ‘ suc suc 𝑁 ) ) ) )
15 gonafv ( ( 𝑎 ∈ V ∧ 𝑏 ∈ V ) → ( 𝑎𝑔 𝑏 ) = ⟨ 1o , ⟨ 𝑎 , 𝑏 ⟩ ⟩ )
16 15 el2v ( 𝑎𝑔 𝑏 ) = ⟨ 1o , ⟨ 𝑎 , 𝑏 ⟩ ⟩
17 16 a1i ( ( 𝑢 ∈ ( Fmla ‘ suc 𝑁 ) ∧ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) ) → ( 𝑎𝑔 𝑏 ) = ⟨ 1o , ⟨ 𝑎 , 𝑏 ⟩ ⟩ )
18 gonafv ( ( 𝑢 ∈ ( Fmla ‘ suc 𝑁 ) ∧ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) ) → ( 𝑢𝑔 𝑣 ) = ⟨ 1o , ⟨ 𝑢 , 𝑣 ⟩ ⟩ )
19 17 18 eqeq12d ( ( 𝑢 ∈ ( Fmla ‘ suc 𝑁 ) ∧ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) ) → ( ( 𝑎𝑔 𝑏 ) = ( 𝑢𝑔 𝑣 ) ↔ ⟨ 1o , ⟨ 𝑎 , 𝑏 ⟩ ⟩ = ⟨ 1o , ⟨ 𝑢 , 𝑣 ⟩ ⟩ ) )
20 1oex 1o ∈ V
21 opex 𝑎 , 𝑏 ⟩ ∈ V
22 20 21 opth ( ⟨ 1o , ⟨ 𝑎 , 𝑏 ⟩ ⟩ = ⟨ 1o , ⟨ 𝑢 , 𝑣 ⟩ ⟩ ↔ ( 1o = 1o ∧ ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑢 , 𝑣 ⟩ ) )
23 19 22 bitrdi ( ( 𝑢 ∈ ( Fmla ‘ suc 𝑁 ) ∧ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) ) → ( ( 𝑎𝑔 𝑏 ) = ( 𝑢𝑔 𝑣 ) ↔ ( 1o = 1o ∧ ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑢 , 𝑣 ⟩ ) ) )
24 23 adantll ( ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ suc 𝑁 ) ) ∧ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) ) → ( ( 𝑎𝑔 𝑏 ) = ( 𝑢𝑔 𝑣 ) ↔ ( 1o = 1o ∧ ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑢 , 𝑣 ⟩ ) ) )
25 vex 𝑎 ∈ V
26 vex 𝑏 ∈ V
27 25 26 opth ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑢 , 𝑣 ⟩ ↔ ( 𝑎 = 𝑢𝑏 = 𝑣 ) )
28 eleq1w ( 𝑢 = 𝑎 → ( 𝑢 ∈ ( Fmla ‘ suc 𝑁 ) ↔ 𝑎 ∈ ( Fmla ‘ suc 𝑁 ) ) )
29 28 equcoms ( 𝑎 = 𝑢 → ( 𝑢 ∈ ( Fmla ‘ suc 𝑁 ) ↔ 𝑎 ∈ ( Fmla ‘ suc 𝑁 ) ) )
30 eleq1w ( 𝑣 = 𝑏 → ( 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) ↔ 𝑏 ∈ ( Fmla ‘ suc 𝑁 ) ) )
31 30 equcoms ( 𝑏 = 𝑣 → ( 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) ↔ 𝑏 ∈ ( Fmla ‘ suc 𝑁 ) ) )
32 29 31 bi2anan9 ( ( 𝑎 = 𝑢𝑏 = 𝑣 ) → ( ( 𝑢 ∈ ( Fmla ‘ suc 𝑁 ) ∧ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) ) ↔ ( 𝑎 ∈ ( Fmla ‘ suc 𝑁 ) ∧ 𝑏 ∈ ( Fmla ‘ suc 𝑁 ) ) ) )
33 32 11 syl6bi ( ( 𝑎 = 𝑢𝑏 = 𝑣 ) → ( ( 𝑢 ∈ ( Fmla ‘ suc 𝑁 ) ∧ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) ) → ( 𝑁 ∈ ω → ( 𝑎 ∈ ( Fmla ‘ suc suc 𝑁 ) ∧ 𝑏 ∈ ( Fmla ‘ suc suc 𝑁 ) ) ) ) )
34 27 33 sylbi ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑢 , 𝑣 ⟩ → ( ( 𝑢 ∈ ( Fmla ‘ suc 𝑁 ) ∧ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) ) → ( 𝑁 ∈ ω → ( 𝑎 ∈ ( Fmla ‘ suc suc 𝑁 ) ∧ 𝑏 ∈ ( Fmla ‘ suc suc 𝑁 ) ) ) ) )
35 34 adantl ( ( 1o = 1o ∧ ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑢 , 𝑣 ⟩ ) → ( ( 𝑢 ∈ ( Fmla ‘ suc 𝑁 ) ∧ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) ) → ( 𝑁 ∈ ω → ( 𝑎 ∈ ( Fmla ‘ suc suc 𝑁 ) ∧ 𝑏 ∈ ( Fmla ‘ suc suc 𝑁 ) ) ) ) )
36 35 com13 ( 𝑁 ∈ ω → ( ( 𝑢 ∈ ( Fmla ‘ suc 𝑁 ) ∧ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) ) → ( ( 1o = 1o ∧ ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑢 , 𝑣 ⟩ ) → ( 𝑎 ∈ ( Fmla ‘ suc suc 𝑁 ) ∧ 𝑏 ∈ ( Fmla ‘ suc suc 𝑁 ) ) ) ) )
37 36 impl ( ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ suc 𝑁 ) ) ∧ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) ) → ( ( 1o = 1o ∧ ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑢 , 𝑣 ⟩ ) → ( 𝑎 ∈ ( Fmla ‘ suc suc 𝑁 ) ∧ 𝑏 ∈ ( Fmla ‘ suc suc 𝑁 ) ) ) )
38 24 37 sylbid ( ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ suc 𝑁 ) ) ∧ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) ) → ( ( 𝑎𝑔 𝑏 ) = ( 𝑢𝑔 𝑣 ) → ( 𝑎 ∈ ( Fmla ‘ suc suc 𝑁 ) ∧ 𝑏 ∈ ( Fmla ‘ suc suc 𝑁 ) ) ) )
39 38 rexlimdva ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ suc 𝑁 ) ) → ( ∃ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) ( 𝑎𝑔 𝑏 ) = ( 𝑢𝑔 𝑣 ) → ( 𝑎 ∈ ( Fmla ‘ suc suc 𝑁 ) ∧ 𝑏 ∈ ( Fmla ‘ suc suc 𝑁 ) ) ) )
40 gonanegoal ( 𝑎𝑔 𝑏 ) ≠ ∀𝑔 𝑖 𝑢
41 eqneqall ( ( 𝑎𝑔 𝑏 ) = ∀𝑔 𝑖 𝑢 → ( ( 𝑎𝑔 𝑏 ) ≠ ∀𝑔 𝑖 𝑢 → ( 𝑎 ∈ ( Fmla ‘ suc suc 𝑁 ) ∧ 𝑏 ∈ ( Fmla ‘ suc suc 𝑁 ) ) ) )
42 40 41 mpi ( ( 𝑎𝑔 𝑏 ) = ∀𝑔 𝑖 𝑢 → ( 𝑎 ∈ ( Fmla ‘ suc suc 𝑁 ) ∧ 𝑏 ∈ ( Fmla ‘ suc suc 𝑁 ) ) )
43 42 a1i ( ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ suc 𝑁 ) ) ∧ 𝑖 ∈ ω ) → ( ( 𝑎𝑔 𝑏 ) = ∀𝑔 𝑖 𝑢 → ( 𝑎 ∈ ( Fmla ‘ suc suc 𝑁 ) ∧ 𝑏 ∈ ( Fmla ‘ suc suc 𝑁 ) ) ) )
44 43 rexlimdva ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ suc 𝑁 ) ) → ( ∃ 𝑖 ∈ ω ( 𝑎𝑔 𝑏 ) = ∀𝑔 𝑖 𝑢 → ( 𝑎 ∈ ( Fmla ‘ suc suc 𝑁 ) ∧ 𝑏 ∈ ( Fmla ‘ suc suc 𝑁 ) ) ) )
45 39 44 jaod ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ suc 𝑁 ) ) → ( ( ∃ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) ( 𝑎𝑔 𝑏 ) = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω ( 𝑎𝑔 𝑏 ) = ∀𝑔 𝑖 𝑢 ) → ( 𝑎 ∈ ( Fmla ‘ suc suc 𝑁 ) ∧ 𝑏 ∈ ( Fmla ‘ suc suc 𝑁 ) ) ) )
46 45 rexlimdva ( 𝑁 ∈ ω → ( ∃ 𝑢 ∈ ( Fmla ‘ suc 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) ( 𝑎𝑔 𝑏 ) = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω ( 𝑎𝑔 𝑏 ) = ∀𝑔 𝑖 𝑢 ) → ( 𝑎 ∈ ( Fmla ‘ suc suc 𝑁 ) ∧ 𝑏 ∈ ( Fmla ‘ suc suc 𝑁 ) ) ) )
47 46 adantr ( ( 𝑁 ∈ ω ∧ ( ( 𝑎𝑔 𝑏 ) ∈ ( Fmla ‘ suc 𝑁 ) → ( 𝑎 ∈ ( Fmla ‘ suc 𝑁 ) ∧ 𝑏 ∈ ( Fmla ‘ suc 𝑁 ) ) ) ) → ( ∃ 𝑢 ∈ ( Fmla ‘ suc 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) ( 𝑎𝑔 𝑏 ) = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω ( 𝑎𝑔 𝑏 ) = ∀𝑔 𝑖 𝑢 ) → ( 𝑎 ∈ ( Fmla ‘ suc suc 𝑁 ) ∧ 𝑏 ∈ ( Fmla ‘ suc suc 𝑁 ) ) ) )
48 14 47 jaod ( ( 𝑁 ∈ ω ∧ ( ( 𝑎𝑔 𝑏 ) ∈ ( Fmla ‘ suc 𝑁 ) → ( 𝑎 ∈ ( Fmla ‘ suc 𝑁 ) ∧ 𝑏 ∈ ( Fmla ‘ suc 𝑁 ) ) ) ) → ( ( ( 𝑎𝑔 𝑏 ) ∈ ( Fmla ‘ suc 𝑁 ) ∨ ∃ 𝑢 ∈ ( Fmla ‘ suc 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) ( 𝑎𝑔 𝑏 ) = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω ( 𝑎𝑔 𝑏 ) = ∀𝑔 𝑖 𝑢 ) ) → ( 𝑎 ∈ ( Fmla ‘ suc suc 𝑁 ) ∧ 𝑏 ∈ ( Fmla ‘ suc suc 𝑁 ) ) ) )
49 5 48 sylbid ( ( 𝑁 ∈ ω ∧ ( ( 𝑎𝑔 𝑏 ) ∈ ( Fmla ‘ suc 𝑁 ) → ( 𝑎 ∈ ( Fmla ‘ suc 𝑁 ) ∧ 𝑏 ∈ ( Fmla ‘ suc 𝑁 ) ) ) ) → ( ( 𝑎𝑔 𝑏 ) ∈ ( Fmla ‘ suc suc 𝑁 ) → ( 𝑎 ∈ ( Fmla ‘ suc suc 𝑁 ) ∧ 𝑏 ∈ ( Fmla ‘ suc suc 𝑁 ) ) ) )
50 49 ex ( 𝑁 ∈ ω → ( ( ( 𝑎𝑔 𝑏 ) ∈ ( Fmla ‘ suc 𝑁 ) → ( 𝑎 ∈ ( Fmla ‘ suc 𝑁 ) ∧ 𝑏 ∈ ( Fmla ‘ suc 𝑁 ) ) ) → ( ( 𝑎𝑔 𝑏 ) ∈ ( Fmla ‘ suc suc 𝑁 ) → ( 𝑎 ∈ ( Fmla ‘ suc suc 𝑁 ) ∧ 𝑏 ∈ ( Fmla ‘ suc suc 𝑁 ) ) ) ) )