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