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 
|- ( N e. _om -> ( ( ( a |g b ) e. ( Fmla ` suc N ) -> ( a e. ( Fmla ` suc N ) /\ b e. ( Fmla ` suc N ) ) ) -> ( ( a |g b ) e. ( Fmla ` suc suc N ) -> ( a e. ( Fmla ` suc suc N ) /\ b e. ( Fmla ` suc suc N ) ) ) ) )

Proof

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