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

Metamath Proof Explorer

Theorem goalrlem

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

Ref Expression
Assertion goalrlem 
|- ( N e. _om -> ( ( A.g i a e. ( Fmla ` suc N ) -> a e. ( Fmla ` suc N ) ) -> ( A.g i a e. ( Fmla ` suc suc N ) -> a e. ( Fmla ` suc suc N ) ) ) )

Proof

Step Hyp Ref Expression
1 peano2 
 |-  ( N e. _om -> suc N e. _om )
2 df-goal 
 |-  A.g i a = <. 2o , <. i , a >. >.
3 opex 
 |-  <. 2o , <. i , a >. >. e. _V
4 2 3 eqeltri 
 |-  A.g i a e. _V
5 isfmlasuc 
 |-  ( ( suc N e. _om /\ A.g i a e. _V ) -> ( A.g i a e. ( Fmla ` suc suc N ) <-> ( A.g i a e. ( Fmla ` suc N ) \/ E. u e. ( Fmla ` suc N ) ( E. v e. ( Fmla ` suc N ) A.g i a = ( u |g v ) \/ E. j e. _om A.g i a = A.g j u ) ) ) )
6 1 4 5 sylancl 
 |-  ( N e. _om -> ( A.g i a e. ( Fmla ` suc suc N ) <-> ( A.g i a e. ( Fmla ` suc N ) \/ E. u e. ( Fmla ` suc N ) ( E. v e. ( Fmla ` suc N ) A.g i a = ( u |g v ) \/ E. j e. _om A.g i a = A.g j u ) ) ) )
7 6 adantr 
 |-  ( ( N e. _om /\ ( A.g i a e. ( Fmla ` suc N ) -> a e. ( Fmla ` suc N ) ) ) -> ( A.g i a e. ( Fmla ` suc suc N ) <-> ( A.g i a e. ( Fmla ` suc N ) \/ E. u e. ( Fmla ` suc N ) ( E. v e. ( Fmla ` suc N ) A.g i a = ( u |g v ) \/ E. j e. _om A.g i a = A.g j u ) ) ) )
8 fmlasssuc 
 |-  ( suc N e. _om -> ( Fmla ` suc N ) C_ ( Fmla ` suc suc N ) )
9 1 8 syl 
 |-  ( N e. _om -> ( Fmla ` suc N ) C_ ( Fmla ` suc suc N ) )
10 9 sseld 
 |-  ( N e. _om -> ( a e. ( Fmla ` suc N ) -> a e. ( Fmla ` suc suc N ) ) )
11 10 com12 
 |-  ( a e. ( Fmla ` suc N ) -> ( N e. _om -> a e. ( Fmla ` suc suc N ) ) )
12 11 imim2i 
 |-  ( ( A.g i a e. ( Fmla ` suc N ) -> a e. ( Fmla ` suc N ) ) -> ( A.g i a e. ( Fmla ` suc N ) -> ( N e. _om -> a e. ( Fmla ` suc suc N ) ) ) )
13 12 com23 
 |-  ( ( A.g i a e. ( Fmla ` suc N ) -> a e. ( Fmla ` suc N ) ) -> ( N e. _om -> ( A.g i a e. ( Fmla ` suc N ) -> a e. ( Fmla ` suc suc N ) ) ) )
14 13 impcom 
 |-  ( ( N e. _om /\ ( A.g i a e. ( Fmla ` suc N ) -> a e. ( Fmla ` suc N ) ) ) -> ( A.g i a e. ( Fmla ` suc N ) -> a e. ( Fmla ` suc suc N ) ) )
15 gonanegoal 
 |-  ( u |g v ) =/= A.g i a
16 eqneqall 
 |-  ( ( u |g v ) = A.g i a -> ( ( u |g v ) =/= A.g i a -> a e. ( Fmla ` suc suc N ) ) )
17 15 16 mpi 
 |-  ( ( u |g v ) = A.g i a -> a e. ( Fmla ` suc suc N ) )
18 17 eqcoms 
 |-  ( A.g i a = ( u |g v ) -> a e. ( Fmla ` suc suc N ) )
19 18 a1i 
 |-  ( ( ( N e. _om /\ u e. ( Fmla ` suc N ) ) /\ v e. ( Fmla ` suc N ) ) -> ( A.g i a = ( u |g v ) -> a e. ( Fmla ` suc suc N ) ) )
20 19 rexlimdva 
 |-  ( ( N e. _om /\ u e. ( Fmla ` suc N ) ) -> ( E. v e. ( Fmla ` suc N ) A.g i a = ( u |g v ) -> a e. ( Fmla ` suc suc N ) ) )
21 df-goal 
 |-  A.g j u = <. 2o , <. j , u >. >.
22 2 21 eqeq12i 
 |-  ( A.g i a = A.g j u <-> <. 2o , <. i , a >. >. = <. 2o , <. j , u >. >. )
23 2oex 
 |-  2o e. _V
24 opex 
 |-  <. i , a >. e. _V
25 23 24 opth 
 |-  ( <. 2o , <. i , a >. >. = <. 2o , <. j , u >. >. <-> ( 2o = 2o /\ <. i , a >. = <. j , u >. ) )
26 22 25 bitri 
 |-  ( A.g i a = A.g j u <-> ( 2o = 2o /\ <. i , a >. = <. j , u >. ) )
27 vex 
 |-  i e. _V
28 vex 
 |-  a e. _V
29 27 28 opth 
 |-  ( <. i , a >. = <. j , u >. <-> ( i = j /\ a = u ) )
30 eleq1w 
 |-  ( u = a -> ( u e. ( Fmla ` suc N ) <-> a e. ( Fmla ` suc N ) ) )
31 30 eqcoms 
 |-  ( a = u -> ( u e. ( Fmla ` suc N ) <-> a e. ( Fmla ` suc N ) ) )
32 31 11 biimtrdi 
 |-  ( a = u -> ( u e. ( Fmla ` suc N ) -> ( N e. _om -> a e. ( Fmla ` suc suc N ) ) ) )
33 32 impcomd 
 |-  ( a = u -> ( ( N e. _om /\ u e. ( Fmla ` suc N ) ) -> a e. ( Fmla ` suc suc N ) ) )
34 29 33 simplbiim 
 |-  ( <. i , a >. = <. j , u >. -> ( ( N e. _om /\ u e. ( Fmla ` suc N ) ) -> a e. ( Fmla ` suc suc N ) ) )
35 26 34 simplbiim 
 |-  ( A.g i a = A.g j u -> ( ( N e. _om /\ u e. ( Fmla ` suc N ) ) -> a e. ( Fmla ` suc suc N ) ) )
36 35 com12 
 |-  ( ( N e. _om /\ u e. ( Fmla ` suc N ) ) -> ( A.g i a = A.g j u -> a e. ( Fmla ` suc suc N ) ) )
37 36 adantr 
 |-  ( ( ( N e. _om /\ u e. ( Fmla ` suc N ) ) /\ j e. _om ) -> ( A.g i a = A.g j u -> a e. ( Fmla ` suc suc N ) ) )
38 37 rexlimdva 
 |-  ( ( N e. _om /\ u e. ( Fmla ` suc N ) ) -> ( E. j e. _om A.g i a = A.g j u -> a e. ( Fmla ` suc suc N ) ) )
39 20 38 jaod 
 |-  ( ( N e. _om /\ u e. ( Fmla ` suc N ) ) -> ( ( E. v e. ( Fmla ` suc N ) A.g i a = ( u |g v ) \/ E. j e. _om A.g i a = A.g j u ) -> a e. ( Fmla ` suc suc N ) ) )
40 39 rexlimdva 
 |-  ( N e. _om -> ( E. u e. ( Fmla ` suc N ) ( E. v e. ( Fmla ` suc N ) A.g i a = ( u |g v ) \/ E. j e. _om A.g i a = A.g j u ) -> a e. ( Fmla ` suc suc N ) ) )
41 40 adantr 
 |-  ( ( N e. _om /\ ( A.g i a e. ( Fmla ` suc N ) -> a e. ( Fmla ` suc N ) ) ) -> ( E. u e. ( Fmla ` suc N ) ( E. v e. ( Fmla ` suc N ) A.g i a = ( u |g v ) \/ E. j e. _om A.g i a = A.g j u ) -> a e. ( Fmla ` suc suc N ) ) )
42 14 41 jaod 
 |-  ( ( N e. _om /\ ( A.g i a e. ( Fmla ` suc N ) -> a e. ( Fmla ` suc N ) ) ) -> ( ( A.g i a e. ( Fmla ` suc N ) \/ E. u e. ( Fmla ` suc N ) ( E. v e. ( Fmla ` suc N ) A.g i a = ( u |g v ) \/ E. j e. _om A.g i a = A.g j u ) ) -> a e. ( Fmla ` suc suc N ) ) )
43 7 42 sylbid 
 |-  ( ( N e. _om /\ ( A.g i a e. ( Fmla ` suc N ) -> a e. ( Fmla ` suc N ) ) ) -> ( A.g i a e. ( Fmla ` suc suc N ) -> a e. ( Fmla ` suc suc N ) ) )
44 43 ex 
 |-  ( N e. _om -> ( ( A.g i a e. ( Fmla ` suc N ) -> a e. ( Fmla ` suc N ) ) -> ( A.g i a e. ( Fmla ` suc suc N ) -> a e. ( Fmla ` suc suc N ) ) ) )