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 syl6bi
 |-  ( 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 ) ) ) )