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

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 biimtrdi ⊢ ( ( 𝑎 = 𝑢 ∧ 𝑏 = 𝑣 ) → ( ( 𝑢 ∈ ( 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 𝑁 ) ) ) ) )