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