Metamath Proof Explorer


Theorem gonarlem

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

Ref Expression
Assertion gonarlem N ω a 𝑔 b Fmla suc N a Fmla suc N b Fmla suc N a 𝑔 b Fmla suc suc N a Fmla suc suc N b Fmla suc suc N

Proof

Step Hyp Ref Expression
1 peano2 N ω suc N ω
2 ovexd N ω a 𝑔 b V
3 isfmlasuc suc N ω a 𝑔 b V a 𝑔 b Fmla suc suc N a 𝑔 b Fmla suc N u Fmla suc N v Fmla suc N a 𝑔 b = u 𝑔 v i ω a 𝑔 b = 𝑔 i u
4 1 2 3 syl2anc N ω a 𝑔 b Fmla suc suc N a 𝑔 b Fmla suc N u Fmla suc N v Fmla suc N a 𝑔 b = u 𝑔 v i ω a 𝑔 b = 𝑔 i u
5 4 adantr N ω a 𝑔 b Fmla suc N a Fmla suc N b Fmla suc N a 𝑔 b Fmla suc suc N a 𝑔 b Fmla suc N u Fmla suc N v Fmla suc N a 𝑔 b = u 𝑔 v i ω a 𝑔 b = 𝑔 i u
6 fmlasssuc suc N ω Fmla suc N Fmla suc suc N
7 1 6 syl N ω Fmla suc N Fmla suc suc N
8 7 sseld N ω a Fmla suc N a Fmla suc suc N
9 7 sseld N ω b Fmla suc N b Fmla suc suc N
10 8 9 anim12d N ω a Fmla suc N b Fmla suc N a Fmla suc suc N b Fmla suc suc N
11 10 com12 a Fmla suc N b Fmla suc N N ω a Fmla suc suc N b Fmla suc suc N
12 11 imim2i a 𝑔 b Fmla suc N a Fmla suc N b Fmla suc N a 𝑔 b Fmla suc N N ω a Fmla suc suc N b Fmla suc suc N
13 12 com23 a 𝑔 b Fmla suc N a Fmla suc N b Fmla suc N N ω a 𝑔 b Fmla suc N a Fmla suc suc N b Fmla suc suc N
14 13 impcom N ω a 𝑔 b Fmla suc N a Fmla suc N b Fmla suc N a 𝑔 b Fmla suc N a Fmla suc suc N b Fmla suc suc N
15 gonafv a V b V a 𝑔 b = 1 𝑜 a b
16 15 el2v a 𝑔 b = 1 𝑜 a b
17 16 a1i u Fmla suc N v Fmla suc N a 𝑔 b = 1 𝑜 a b
18 gonafv u Fmla suc N v Fmla suc N u 𝑔 v = 1 𝑜 u v
19 17 18 eqeq12d u Fmla suc N v Fmla suc N a 𝑔 b = u 𝑔 v 1 𝑜 a b = 1 𝑜 u v
20 1oex 1 𝑜 V
21 opex a b V
22 20 21 opth 1 𝑜 a b = 1 𝑜 u v 1 𝑜 = 1 𝑜 a b = u v
23 19 22 bitrdi u Fmla suc N v Fmla suc N a 𝑔 b = u 𝑔 v 1 𝑜 = 1 𝑜 a b = u v
24 23 adantll N ω u Fmla suc N v Fmla suc N a 𝑔 b = u 𝑔 v 1 𝑜 = 1 𝑜 a b = u v
25 vex a V
26 vex b V
27 25 26 opth a b = u v a = u b = v
28 eleq1w u = a u Fmla suc N a Fmla suc N
29 28 equcoms a = u u Fmla suc N a Fmla suc N
30 eleq1w v = b v Fmla suc N b Fmla suc N
31 30 equcoms b = v v Fmla suc N b Fmla suc N
32 29 31 bi2anan9 a = u b = v u Fmla suc N v Fmla suc N a Fmla suc N b Fmla suc N
33 32 11 syl6bi a = u b = v u Fmla suc N v Fmla suc N N ω a Fmla suc suc N b Fmla suc suc N
34 27 33 sylbi a b = u v u Fmla suc N v Fmla suc N N ω a Fmla suc suc N b Fmla suc suc N
35 34 adantl 1 𝑜 = 1 𝑜 a b = u v u Fmla suc N v Fmla suc N N ω a Fmla suc suc N b Fmla suc suc N
36 35 com13 N ω u Fmla suc N v Fmla suc N 1 𝑜 = 1 𝑜 a b = u v a Fmla suc suc N b Fmla suc suc N
37 36 impl N ω u Fmla suc N v Fmla suc N 1 𝑜 = 1 𝑜 a b = u v a Fmla suc suc N b Fmla suc suc N
38 24 37 sylbid N ω u Fmla suc N v Fmla suc N a 𝑔 b = u 𝑔 v a Fmla suc suc N b Fmla suc suc N
39 38 rexlimdva N ω u Fmla suc N v Fmla suc N a 𝑔 b = u 𝑔 v a Fmla suc suc N b Fmla suc suc N
40 gonanegoal a 𝑔 b 𝑔 i u
41 eqneqall a 𝑔 b = 𝑔 i u a 𝑔 b 𝑔 i u a Fmla suc suc N b Fmla suc suc N
42 40 41 mpi a 𝑔 b = 𝑔 i u a Fmla suc suc N b Fmla suc suc N
43 42 a1i N ω u Fmla suc N i ω a 𝑔 b = 𝑔 i u a Fmla suc suc N b Fmla suc suc N
44 43 rexlimdva N ω u Fmla suc N i ω a 𝑔 b = 𝑔 i u a Fmla suc suc N b Fmla suc suc N
45 39 44 jaod N ω u Fmla suc N v Fmla suc N a 𝑔 b = u 𝑔 v i ω a 𝑔 b = 𝑔 i u a Fmla suc suc N b Fmla suc suc N
46 45 rexlimdva N ω u Fmla suc N v Fmla suc N a 𝑔 b = u 𝑔 v i ω a 𝑔 b = 𝑔 i u a Fmla suc suc N b Fmla suc suc N
47 46 adantr N ω a 𝑔 b Fmla suc N a Fmla suc N b Fmla suc N u Fmla suc N v Fmla suc N a 𝑔 b = u 𝑔 v i ω a 𝑔 b = 𝑔 i u a Fmla suc suc N b Fmla suc suc N
48 14 47 jaod N ω a 𝑔 b Fmla suc N a Fmla suc N b Fmla suc N a 𝑔 b Fmla suc N u Fmla suc N v Fmla suc N a 𝑔 b = u 𝑔 v i ω a 𝑔 b = 𝑔 i u a Fmla suc suc N b Fmla suc suc N
49 5 48 sylbid N ω a 𝑔 b Fmla suc N a Fmla suc N b Fmla suc N a 𝑔 b Fmla suc suc N a Fmla suc suc N b Fmla suc suc N
50 49 ex N ω a 𝑔 b Fmla suc N a Fmla suc N b Fmla suc N a 𝑔 b Fmla suc suc N a Fmla suc suc N b Fmla suc suc N