Metamath Proof Explorer


Theorem goalrlem

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

Ref Expression
Assertion goalrlem ( 𝑁 ∈ ω → ( ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc 𝑁 ) → 𝑎 ∈ ( Fmla ‘ suc 𝑁 ) ) → ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc suc 𝑁 ) → 𝑎 ∈ ( Fmla ‘ suc suc 𝑁 ) ) ) )

Proof

Step Hyp Ref Expression
1 peano2 ( 𝑁 ∈ ω → suc 𝑁 ∈ ω )
2 df-goal 𝑔 𝑖 𝑎 = ⟨ 2o , ⟨ 𝑖 , 𝑎 ⟩ ⟩
3 opex ⟨ 2o , ⟨ 𝑖 , 𝑎 ⟩ ⟩ ∈ V
4 2 3 eqeltri 𝑔 𝑖 𝑎 ∈ V
5 isfmlasuc ( ( suc 𝑁 ∈ ω ∧ ∀𝑔 𝑖 𝑎 ∈ V ) → ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc suc 𝑁 ) ↔ ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc 𝑁 ) ∨ ∃ 𝑢 ∈ ( Fmla ‘ suc 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) ∀𝑔 𝑖 𝑎 = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑗 ∈ ω ∀𝑔 𝑖 𝑎 = ∀𝑔 𝑗 𝑢 ) ) ) )
6 1 4 5 sylancl ( 𝑁 ∈ ω → ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc suc 𝑁 ) ↔ ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc 𝑁 ) ∨ ∃ 𝑢 ∈ ( Fmla ‘ suc 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) ∀𝑔 𝑖 𝑎 = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑗 ∈ ω ∀𝑔 𝑖 𝑎 = ∀𝑔 𝑗 𝑢 ) ) ) )
7 6 adantr ( ( 𝑁 ∈ ω ∧ ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc 𝑁 ) → 𝑎 ∈ ( Fmla ‘ suc 𝑁 ) ) ) → ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc suc 𝑁 ) ↔ ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc 𝑁 ) ∨ ∃ 𝑢 ∈ ( Fmla ‘ suc 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) ∀𝑔 𝑖 𝑎 = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑗 ∈ ω ∀𝑔 𝑖 𝑎 = ∀𝑔 𝑗 𝑢 ) ) ) )
8 fmlasssuc ( suc 𝑁 ∈ ω → ( Fmla ‘ suc 𝑁 ) ⊆ ( Fmla ‘ suc suc 𝑁 ) )
9 1 8 syl ( 𝑁 ∈ ω → ( Fmla ‘ suc 𝑁 ) ⊆ ( Fmla ‘ suc suc 𝑁 ) )
10 9 sseld ( 𝑁 ∈ ω → ( 𝑎 ∈ ( Fmla ‘ suc 𝑁 ) → 𝑎 ∈ ( Fmla ‘ suc suc 𝑁 ) ) )
11 10 com12 ( 𝑎 ∈ ( Fmla ‘ suc 𝑁 ) → ( 𝑁 ∈ ω → 𝑎 ∈ ( Fmla ‘ suc suc 𝑁 ) ) )
12 11 imim2i ( ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc 𝑁 ) → 𝑎 ∈ ( Fmla ‘ suc 𝑁 ) ) → ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc 𝑁 ) → ( 𝑁 ∈ ω → 𝑎 ∈ ( Fmla ‘ suc suc 𝑁 ) ) ) )
13 12 com23 ( ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc 𝑁 ) → 𝑎 ∈ ( Fmla ‘ suc 𝑁 ) ) → ( 𝑁 ∈ ω → ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc 𝑁 ) → 𝑎 ∈ ( Fmla ‘ suc suc 𝑁 ) ) ) )
14 13 impcom ( ( 𝑁 ∈ ω ∧ ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc 𝑁 ) → 𝑎 ∈ ( Fmla ‘ suc 𝑁 ) ) ) → ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc 𝑁 ) → 𝑎 ∈ ( Fmla ‘ suc suc 𝑁 ) ) )
15 gonanegoal ( 𝑢𝑔 𝑣 ) ≠ ∀𝑔 𝑖 𝑎
16 eqneqall ( ( 𝑢𝑔 𝑣 ) = ∀𝑔 𝑖 𝑎 → ( ( 𝑢𝑔 𝑣 ) ≠ ∀𝑔 𝑖 𝑎𝑎 ∈ ( Fmla ‘ suc suc 𝑁 ) ) )
17 15 16 mpi ( ( 𝑢𝑔 𝑣 ) = ∀𝑔 𝑖 𝑎𝑎 ∈ ( Fmla ‘ suc suc 𝑁 ) )
18 17 eqcoms ( ∀𝑔 𝑖 𝑎 = ( 𝑢𝑔 𝑣 ) → 𝑎 ∈ ( Fmla ‘ suc suc 𝑁 ) )
19 18 a1i ( ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ suc 𝑁 ) ) ∧ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) ) → ( ∀𝑔 𝑖 𝑎 = ( 𝑢𝑔 𝑣 ) → 𝑎 ∈ ( Fmla ‘ suc suc 𝑁 ) ) )
20 19 rexlimdva ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ suc 𝑁 ) ) → ( ∃ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) ∀𝑔 𝑖 𝑎 = ( 𝑢𝑔 𝑣 ) → 𝑎 ∈ ( Fmla ‘ suc suc 𝑁 ) ) )
21 df-goal 𝑔 𝑗 𝑢 = ⟨ 2o , ⟨ 𝑗 , 𝑢 ⟩ ⟩
22 2 21 eqeq12i ( ∀𝑔 𝑖 𝑎 = ∀𝑔 𝑗 𝑢 ↔ ⟨ 2o , ⟨ 𝑖 , 𝑎 ⟩ ⟩ = ⟨ 2o , ⟨ 𝑗 , 𝑢 ⟩ ⟩ )
23 2oex 2o ∈ V
24 opex 𝑖 , 𝑎 ⟩ ∈ V
25 23 24 opth ( ⟨ 2o , ⟨ 𝑖 , 𝑎 ⟩ ⟩ = ⟨ 2o , ⟨ 𝑗 , 𝑢 ⟩ ⟩ ↔ ( 2o = 2o ∧ ⟨ 𝑖 , 𝑎 ⟩ = ⟨ 𝑗 , 𝑢 ⟩ ) )
26 22 25 bitri ( ∀𝑔 𝑖 𝑎 = ∀𝑔 𝑗 𝑢 ↔ ( 2o = 2o ∧ ⟨ 𝑖 , 𝑎 ⟩ = ⟨ 𝑗 , 𝑢 ⟩ ) )
27 vex 𝑖 ∈ V
28 vex 𝑎 ∈ V
29 27 28 opth ( ⟨ 𝑖 , 𝑎 ⟩ = ⟨ 𝑗 , 𝑢 ⟩ ↔ ( 𝑖 = 𝑗𝑎 = 𝑢 ) )
30 eleq1w ( 𝑢 = 𝑎 → ( 𝑢 ∈ ( Fmla ‘ suc 𝑁 ) ↔ 𝑎 ∈ ( Fmla ‘ suc 𝑁 ) ) )
31 30 eqcoms ( 𝑎 = 𝑢 → ( 𝑢 ∈ ( Fmla ‘ suc 𝑁 ) ↔ 𝑎 ∈ ( Fmla ‘ suc 𝑁 ) ) )
32 31 11 syl6bi ( 𝑎 = 𝑢 → ( 𝑢 ∈ ( Fmla ‘ suc 𝑁 ) → ( 𝑁 ∈ ω → 𝑎 ∈ ( Fmla ‘ suc suc 𝑁 ) ) ) )
33 32 impcomd ( 𝑎 = 𝑢 → ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ suc 𝑁 ) ) → 𝑎 ∈ ( Fmla ‘ suc suc 𝑁 ) ) )
34 29 33 simplbiim ( ⟨ 𝑖 , 𝑎 ⟩ = ⟨ 𝑗 , 𝑢 ⟩ → ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ suc 𝑁 ) ) → 𝑎 ∈ ( Fmla ‘ suc suc 𝑁 ) ) )
35 26 34 simplbiim ( ∀𝑔 𝑖 𝑎 = ∀𝑔 𝑗 𝑢 → ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ suc 𝑁 ) ) → 𝑎 ∈ ( Fmla ‘ suc suc 𝑁 ) ) )
36 35 com12 ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ suc 𝑁 ) ) → ( ∀𝑔 𝑖 𝑎 = ∀𝑔 𝑗 𝑢𝑎 ∈ ( Fmla ‘ suc suc 𝑁 ) ) )
37 36 adantr ( ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ suc 𝑁 ) ) ∧ 𝑗 ∈ ω ) → ( ∀𝑔 𝑖 𝑎 = ∀𝑔 𝑗 𝑢𝑎 ∈ ( Fmla ‘ suc suc 𝑁 ) ) )
38 37 rexlimdva ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ suc 𝑁 ) ) → ( ∃ 𝑗 ∈ ω ∀𝑔 𝑖 𝑎 = ∀𝑔 𝑗 𝑢𝑎 ∈ ( Fmla ‘ suc suc 𝑁 ) ) )
39 20 38 jaod ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ suc 𝑁 ) ) → ( ( ∃ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) ∀𝑔 𝑖 𝑎 = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑗 ∈ ω ∀𝑔 𝑖 𝑎 = ∀𝑔 𝑗 𝑢 ) → 𝑎 ∈ ( Fmla ‘ suc suc 𝑁 ) ) )
40 39 rexlimdva ( 𝑁 ∈ ω → ( ∃ 𝑢 ∈ ( Fmla ‘ suc 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) ∀𝑔 𝑖 𝑎 = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑗 ∈ ω ∀𝑔 𝑖 𝑎 = ∀𝑔 𝑗 𝑢 ) → 𝑎 ∈ ( Fmla ‘ suc suc 𝑁 ) ) )
41 40 adantr ( ( 𝑁 ∈ ω ∧ ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc 𝑁 ) → 𝑎 ∈ ( Fmla ‘ suc 𝑁 ) ) ) → ( ∃ 𝑢 ∈ ( Fmla ‘ suc 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) ∀𝑔 𝑖 𝑎 = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑗 ∈ ω ∀𝑔 𝑖 𝑎 = ∀𝑔 𝑗 𝑢 ) → 𝑎 ∈ ( Fmla ‘ suc suc 𝑁 ) ) )
42 14 41 jaod ( ( 𝑁 ∈ ω ∧ ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc 𝑁 ) → 𝑎 ∈ ( Fmla ‘ suc 𝑁 ) ) ) → ( ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc 𝑁 ) ∨ ∃ 𝑢 ∈ ( Fmla ‘ suc 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ suc 𝑁 ) ∀𝑔 𝑖 𝑎 = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑗 ∈ ω ∀𝑔 𝑖 𝑎 = ∀𝑔 𝑗 𝑢 ) ) → 𝑎 ∈ ( Fmla ‘ suc suc 𝑁 ) ) )
43 7 42 sylbid ( ( 𝑁 ∈ ω ∧ ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc 𝑁 ) → 𝑎 ∈ ( Fmla ‘ suc 𝑁 ) ) ) → ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc suc 𝑁 ) → 𝑎 ∈ ( Fmla ‘ suc suc 𝑁 ) ) )
44 43 ex ( 𝑁 ∈ ω → ( ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc 𝑁 ) → 𝑎 ∈ ( Fmla ‘ suc 𝑁 ) ) → ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc suc 𝑁 ) → 𝑎 ∈ ( Fmla ‘ suc suc 𝑁 ) ) ) )