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

Metamath Proof Explorer

Theorem satffunlem2lem1

Description: Lemma 1 for satffunlem2 . (Contributed by AV, 28-Oct-2023)

Ref Expression
Hypotheses satffunlem2lem1.s 
|- S = ( M Sat E )
satffunlem2lem1.a 
|- A = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) )
satffunlem2lem1.b 
|- B = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) }
Assertion satffunlem2lem1 
|- ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) -> Fun { <. x , y >. | ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) } )

Proof

Step Hyp Ref Expression
1 satffunlem2lem1.s 
 |-  S = ( M Sat E )
2 satffunlem2lem1.a 
 |-  A = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) )
3 satffunlem2lem1.b 
 |-  B = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) }
4 simpl 
 |-  ( ( u = s /\ v = r ) -> u = s )
5 4 fveq2d 
 |-  ( ( u = s /\ v = r ) -> ( 1st ` u ) = ( 1st ` s ) )
6 simpr 
 |-  ( ( u = s /\ v = r ) -> v = r )
7 6 fveq2d 
 |-  ( ( u = s /\ v = r ) -> ( 1st ` v ) = ( 1st ` r ) )
8 5 7 oveq12d 
 |-  ( ( u = s /\ v = r ) -> ( ( 1st ` u ) |g ( 1st ` v ) ) = ( ( 1st ` s ) |g ( 1st ` r ) ) )
9 8 eqeq2d 
 |-  ( ( u = s /\ v = r ) -> ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) <-> x = ( ( 1st ` s ) |g ( 1st ` r ) ) ) )
10 4 fveq2d 
 |-  ( ( u = s /\ v = r ) -> ( 2nd ` u ) = ( 2nd ` s ) )
11 6 fveq2d 
 |-  ( ( u = s /\ v = r ) -> ( 2nd ` v ) = ( 2nd ` r ) )
12 10 11 ineq12d 
 |-  ( ( u = s /\ v = r ) -> ( ( 2nd ` u ) i^i ( 2nd ` v ) ) = ( ( 2nd ` s ) i^i ( 2nd ` r ) ) )
13 12 difeq2d 
 |-  ( ( u = s /\ v = r ) -> ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) )
14 2 13 eqtrid 
 |-  ( ( u = s /\ v = r ) -> A = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) )
15 14 eqeq2d 
 |-  ( ( u = s /\ v = r ) -> ( y = A <-> y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) )
16 9 15 anbi12d 
 |-  ( ( u = s /\ v = r ) -> ( ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) <-> ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) ) )
17 16 cbvrexdva 
 |-  ( u = s -> ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) <-> E. r e. ( S ` suc N ) ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) ) )
18 simpr 
 |-  ( ( u = s /\ i = j ) -> i = j )
19 fveq2 
 |-  ( u = s -> ( 1st ` u ) = ( 1st ` s ) )
20 19 adantr 
 |-  ( ( u = s /\ i = j ) -> ( 1st ` u ) = ( 1st ` s ) )
21 18 20 goaleq12d 
 |-  ( ( u = s /\ i = j ) -> A.g i ( 1st ` u ) = A.g j ( 1st ` s ) )
22 21 eqeq2d 
 |-  ( ( u = s /\ i = j ) -> ( x = A.g i ( 1st ` u ) <-> x = A.g j ( 1st ` s ) ) )
23 3 eqeq2i 
 |-  ( y = B <-> y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } )
24 opeq1 
 |-  ( i = j -> <. i , z >. = <. j , z >. )
25 24 sneqd 
 |-  ( i = j -> { <. i , z >. } = { <. j , z >. } )
26 sneq 
 |-  ( i = j -> { i } = { j } )
27 26 difeq2d 
 |-  ( i = j -> ( _om \ { i } ) = ( _om \ { j } ) )
28 27 reseq2d 
 |-  ( i = j -> ( a |` ( _om \ { i } ) ) = ( a |` ( _om \ { j } ) ) )
29 25 28 uneq12d 
 |-  ( i = j -> ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) = ( { <. j , z >. } u. ( a |` ( _om \ { j } ) ) ) )
30 29 adantl 
 |-  ( ( u = s /\ i = j ) -> ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) = ( { <. j , z >. } u. ( a |` ( _om \ { j } ) ) ) )
31 fveq2 
 |-  ( u = s -> ( 2nd ` u ) = ( 2nd ` s ) )
32 31 adantr 
 |-  ( ( u = s /\ i = j ) -> ( 2nd ` u ) = ( 2nd ` s ) )
33 30 32 eleq12d 
 |-  ( ( u = s /\ i = j ) -> ( ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) <-> ( { <. j , z >. } u. ( a |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) ) )
34 33 ralbidv 
 |-  ( ( u = s /\ i = j ) -> ( A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) <-> A. z e. M ( { <. j , z >. } u. ( a |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) ) )
35 34 rabbidv 
 |-  ( ( u = s /\ i = j ) -> { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } = { a e. ( M ^m _om ) | A. z e. M ( { <. j , z >. } u. ( a |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } )
36 35 eqeq2d 
 |-  ( ( u = s /\ i = j ) -> ( y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } <-> y = { a e. ( M ^m _om ) | A. z e. M ( { <. j , z >. } u. ( a |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } ) )
37 23 36 bitrid 
 |-  ( ( u = s /\ i = j ) -> ( y = B <-> y = { a e. ( M ^m _om ) | A. z e. M ( { <. j , z >. } u. ( a |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } ) )
38 22 37 anbi12d 
 |-  ( ( u = s /\ i = j ) -> ( ( x = A.g i ( 1st ` u ) /\ y = B ) <-> ( x = A.g j ( 1st ` s ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. j , z >. } u. ( a |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } ) ) )
39 38 cbvrexdva 
 |-  ( u = s -> ( E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) <-> E. j e. _om ( x = A.g j ( 1st ` s ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. j , z >. } u. ( a |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } ) ) )
40 17 39 orbi12d 
 |-  ( u = s -> ( ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) <-> ( E. r e. ( S ` suc N ) ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) \/ E. j e. _om ( x = A.g j ( 1st ` s ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. j , z >. } u. ( a |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } ) ) ) )
41 40 cbvrexvw 
 |-  ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) <-> E. s e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. r e. ( S ` suc N ) ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) \/ E. j e. _om ( x = A.g j ( 1st ` s ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. j , z >. } u. ( a |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } ) ) )
42 fveq2 
 |-  ( v = r -> ( 1st ` v ) = ( 1st ` r ) )
43 19 42 oveqan12d 
 |-  ( ( u = s /\ v = r ) -> ( ( 1st ` u ) |g ( 1st ` v ) ) = ( ( 1st ` s ) |g ( 1st ` r ) ) )
44 43 eqeq2d 
 |-  ( ( u = s /\ v = r ) -> ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) <-> x = ( ( 1st ` s ) |g ( 1st ` r ) ) ) )
45 2 eqeq2i 
 |-  ( y = A <-> y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) )
46 fveq2 
 |-  ( v = r -> ( 2nd ` v ) = ( 2nd ` r ) )
47 31 46 ineqan12d 
 |-  ( ( u = s /\ v = r ) -> ( ( 2nd ` u ) i^i ( 2nd ` v ) ) = ( ( 2nd ` s ) i^i ( 2nd ` r ) ) )
48 47 difeq2d 
 |-  ( ( u = s /\ v = r ) -> ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) )
49 48 eqeq2d 
 |-  ( ( u = s /\ v = r ) -> ( y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) <-> y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) )
50 45 49 bitrid 
 |-  ( ( u = s /\ v = r ) -> ( y = A <-> y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) )
51 44 50 anbi12d 
 |-  ( ( u = s /\ v = r ) -> ( ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) <-> ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) ) )
52 51 cbvrexdva 
 |-  ( u = s -> ( E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) <-> E. r e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) ) )
53 52 cbvrexvw 
 |-  ( E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) <-> E. s e. ( S ` N ) E. r e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) )
54 41 53 orbi12i 
 |-  ( ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) <-> ( E. s e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. r e. ( S ` suc N ) ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) \/ E. j e. _om ( x = A.g j ( 1st ` s ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. j , z >. } u. ( a |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } ) ) \/ E. s e. ( S ` N ) E. r e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) ) )
55 simp-5l 
 |-  ( ( ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ s e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ r e. ( S ` suc N ) ) /\ u e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ v e. ( S ` suc N ) ) -> Fun ( S ` suc N ) )
56 eldifi 
 |-  ( s e. ( ( S ` suc N ) \ ( S ` N ) ) -> s e. ( S ` suc N ) )
57 56 adantl 
 |-  ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ s e. ( ( S ` suc N ) \ ( S ` N ) ) ) -> s e. ( S ` suc N ) )
58 57 anim1i 
 |-  ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ s e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ r e. ( S ` suc N ) ) -> ( s e. ( S ` suc N ) /\ r e. ( S ` suc N ) ) )
59 58 ad2antrr 
 |-  ( ( ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ s e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ r e. ( S ` suc N ) ) /\ u e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ v e. ( S ` suc N ) ) -> ( s e. ( S ` suc N ) /\ r e. ( S ` suc N ) ) )
60 eldifi 
 |-  ( u e. ( ( S ` suc N ) \ ( S ` N ) ) -> u e. ( S ` suc N ) )
61 60 adantl 
 |-  ( ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ s e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ r e. ( S ` suc N ) ) /\ u e. ( ( S ` suc N ) \ ( S ` N ) ) ) -> u e. ( S ` suc N ) )
62 61 anim1i 
 |-  ( ( ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ s e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ r e. ( S ` suc N ) ) /\ u e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ v e. ( S ` suc N ) ) -> ( u e. ( S ` suc N ) /\ v e. ( S ` suc N ) ) )
63 55 59 62 3jca 
 |-  ( ( ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ s e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ r e. ( S ` suc N ) ) /\ u e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ v e. ( S ` suc N ) ) -> ( Fun ( S ` suc N ) /\ ( s e. ( S ` suc N ) /\ r e. ( S ` suc N ) ) /\ ( u e. ( S ` suc N ) /\ v e. ( S ` suc N ) ) ) )
64 id 
 |-  ( ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) -> ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) )
65 2 eqeq2i 
 |-  ( w = A <-> w = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) )
66 65 biimpi 
 |-  ( w = A -> w = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) )
67 66 anim2i 
 |-  ( ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) -> ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) )
68 satffunlem 
 |-  ( ( ( Fun ( S ` suc N ) /\ ( s e. ( S ` suc N ) /\ r e. ( S ` suc N ) ) /\ ( u e. ( S ` suc N ) /\ v e. ( S ` suc N ) ) ) /\ ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) /\ ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) ) -> y = w )
69 63 64 67 68 syl3an 
 |-  ( ( ( ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ s e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ r e. ( S ` suc N ) ) /\ u e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ v e. ( S ` suc N ) ) /\ ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) /\ ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) ) -> y = w )
70 69 3exp 
 |-  ( ( ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ s e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ r e. ( S ` suc N ) ) /\ u e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ v e. ( S ` suc N ) ) -> ( ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) -> ( ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) -> y = w ) ) )
71 70 com23 
 |-  ( ( ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ s e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ r e. ( S ` suc N ) ) /\ u e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ v e. ( S ` suc N ) ) -> ( ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) -> ( ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) -> y = w ) ) )
72 71 rexlimdva 
 |-  ( ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ s e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ r e. ( S ` suc N ) ) /\ u e. ( ( S ` suc N ) \ ( S ` N ) ) ) -> ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) -> ( ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) -> y = w ) ) )
73 eqeq1 
 |-  ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) -> ( x = A.g i ( 1st ` u ) <-> ( ( 1st ` s ) |g ( 1st ` r ) ) = A.g i ( 1st ` u ) ) )
74 fvex 
 |-  ( 1st ` s ) e. _V
75 fvex 
 |-  ( 1st ` r ) e. _V
76 gonafv 
 |-  ( ( ( 1st ` s ) e. _V /\ ( 1st ` r ) e. _V ) -> ( ( 1st ` s ) |g ( 1st ` r ) ) = <. 1o , <. ( 1st ` s ) , ( 1st ` r ) >. >. )
77 74 75 76 mp2an 
 |-  ( ( 1st ` s ) |g ( 1st ` r ) ) = <. 1o , <. ( 1st ` s ) , ( 1st ` r ) >. >.
78 df-goal 
 |-  A.g i ( 1st ` u ) = <. 2o , <. i , ( 1st ` u ) >. >.
79 77 78 eqeq12i 
 |-  ( ( ( 1st ` s ) |g ( 1st ` r ) ) = A.g i ( 1st ` u ) <-> <. 1o , <. ( 1st ` s ) , ( 1st ` r ) >. >. = <. 2o , <. i , ( 1st ` u ) >. >. )
80 1oex 
 |-  1o e. _V
81 opex 
 |-  <. ( 1st ` s ) , ( 1st ` r ) >. e. _V
82 80 81 opth 
 |-  ( <. 1o , <. ( 1st ` s ) , ( 1st ` r ) >. >. = <. 2o , <. i , ( 1st ` u ) >. >. <-> ( 1o = 2o /\ <. ( 1st ` s ) , ( 1st ` r ) >. = <. i , ( 1st ` u ) >. ) )
83 1one2o 
 |-  1o =/= 2o
84 df-ne 
 |-  ( 1o =/= 2o <-> -. 1o = 2o )
85 pm2.21 
 |-  ( -. 1o = 2o -> ( 1o = 2o -> y = w ) )
86 84 85 sylbi 
 |-  ( 1o =/= 2o -> ( 1o = 2o -> y = w ) )
87 83 86 ax-mp 
 |-  ( 1o = 2o -> y = w )
88 87 adantr 
 |-  ( ( 1o = 2o /\ <. ( 1st ` s ) , ( 1st ` r ) >. = <. i , ( 1st ` u ) >. ) -> y = w )
89 82 88 sylbi 
 |-  ( <. 1o , <. ( 1st ` s ) , ( 1st ` r ) >. >. = <. 2o , <. i , ( 1st ` u ) >. >. -> y = w )
90 79 89 sylbi 
 |-  ( ( ( 1st ` s ) |g ( 1st ` r ) ) = A.g i ( 1st ` u ) -> y = w )
91 73 90 biimtrdi 
 |-  ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) -> ( x = A.g i ( 1st ` u ) -> y = w ) )
92 91 adantr 
 |-  ( ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) -> ( x = A.g i ( 1st ` u ) -> y = w ) )
93 92 com12 
 |-  ( x = A.g i ( 1st ` u ) -> ( ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) -> y = w ) )
94 93 adantr 
 |-  ( ( x = A.g i ( 1st ` u ) /\ w = B ) -> ( ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) -> y = w ) )
95 94 a1i 
 |-  ( ( ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ s e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ r e. ( S ` suc N ) ) /\ u e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ i e. _om ) -> ( ( x = A.g i ( 1st ` u ) /\ w = B ) -> ( ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) -> y = w ) ) )
96 95 rexlimdva 
 |-  ( ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ s e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ r e. ( S ` suc N ) ) /\ u e. ( ( S ` suc N ) \ ( S ` N ) ) ) -> ( E. i e. _om ( x = A.g i ( 1st ` u ) /\ w = B ) -> ( ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) -> y = w ) ) )
97 72 96 jaod 
 |-  ( ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ s e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ r e. ( S ` suc N ) ) /\ u e. ( ( S ` suc N ) \ ( S ` N ) ) ) -> ( ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ w = B ) ) -> ( ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) -> y = w ) ) )
98 97 rexlimdva 
 |-  ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ s e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ r e. ( S ` suc N ) ) -> ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ w = B ) ) -> ( ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) -> y = w ) ) )
99 simp-4l 
 |-  ( ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ s e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ r e. ( S ` suc N ) ) /\ ( u e. ( S ` N ) /\ v e. ( ( S ` suc N ) \ ( S ` N ) ) ) ) -> Fun ( S ` suc N ) )
100 58 adantr 
 |-  ( ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ s e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ r e. ( S ` suc N ) ) /\ ( u e. ( S ` N ) /\ v e. ( ( S ` suc N ) \ ( S ` N ) ) ) ) -> ( s e. ( S ` suc N ) /\ r e. ( S ` suc N ) ) )
101 ssel 
 |-  ( ( S ` N ) C_ ( S ` suc N ) -> ( u e. ( S ` N ) -> u e. ( S ` suc N ) ) )
102 101 ad3antlr 
 |-  ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ s e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ r e. ( S ` suc N ) ) -> ( u e. ( S ` N ) -> u e. ( S ` suc N ) ) )
103 102 com12 
 |-  ( u e. ( S ` N ) -> ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ s e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ r e. ( S ` suc N ) ) -> u e. ( S ` suc N ) ) )
104 103 adantr 
 |-  ( ( u e. ( S ` N ) /\ v e. ( ( S ` suc N ) \ ( S ` N ) ) ) -> ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ s e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ r e. ( S ` suc N ) ) -> u e. ( S ` suc N ) ) )
105 104 impcom 
 |-  ( ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ s e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ r e. ( S ` suc N ) ) /\ ( u e. ( S ` N ) /\ v e. ( ( S ` suc N ) \ ( S ` N ) ) ) ) -> u e. ( S ` suc N ) )
106 eldifi 
 |-  ( v e. ( ( S ` suc N ) \ ( S ` N ) ) -> v e. ( S ` suc N ) )
107 106 ad2antll 
 |-  ( ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ s e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ r e. ( S ` suc N ) ) /\ ( u e. ( S ` N ) /\ v e. ( ( S ` suc N ) \ ( S ` N ) ) ) ) -> v e. ( S ` suc N ) )
108 105 107 jca 
 |-  ( ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ s e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ r e. ( S ` suc N ) ) /\ ( u e. ( S ` N ) /\ v e. ( ( S ` suc N ) \ ( S ` N ) ) ) ) -> ( u e. ( S ` suc N ) /\ v e. ( S ` suc N ) ) )
109 99 100 108 3jca 
 |-  ( ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ s e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ r e. ( S ` suc N ) ) /\ ( u e. ( S ` N ) /\ v e. ( ( S ` suc N ) \ ( S ` N ) ) ) ) -> ( Fun ( S ` suc N ) /\ ( s e. ( S ` suc N ) /\ r e. ( S ` suc N ) ) /\ ( u e. ( S ` suc N ) /\ v e. ( S ` suc N ) ) ) )
110 109 64 67 68 syl3an 
 |-  ( ( ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ s e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ r e. ( S ` suc N ) ) /\ ( u e. ( S ` N ) /\ v e. ( ( S ` suc N ) \ ( S ` N ) ) ) ) /\ ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) /\ ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) ) -> y = w )
111 110 3exp 
 |-  ( ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ s e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ r e. ( S ` suc N ) ) /\ ( u e. ( S ` N ) /\ v e. ( ( S ` suc N ) \ ( S ` N ) ) ) ) -> ( ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) -> ( ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) -> y = w ) ) )
112 111 com23 
 |-  ( ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ s e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ r e. ( S ` suc N ) ) /\ ( u e. ( S ` N ) /\ v e. ( ( S ` suc N ) \ ( S ` N ) ) ) ) -> ( ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) -> ( ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) -> y = w ) ) )
113 112 rexlimdvva 
 |-  ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ s e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ r e. ( S ` suc N ) ) -> ( E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) -> ( ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) -> y = w ) ) )
114 98 113 jaod 
 |-  ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ s e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ r e. ( S ` suc N ) ) -> ( ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ w = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) ) -> ( ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) -> y = w ) ) )
115 114 com23 
 |-  ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ s e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ r e. ( S ` suc N ) ) -> ( ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) -> ( ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ w = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) ) -> y = w ) ) )
116 115 rexlimdva 
 |-  ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ s e. ( ( S ` suc N ) \ ( S ` N ) ) ) -> ( E. r e. ( S ` suc N ) ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) -> ( ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ w = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) ) -> y = w ) ) )
117 eqeq1 
 |-  ( x = A.g j ( 1st ` s ) -> ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) <-> A.g j ( 1st ` s ) = ( ( 1st ` u ) |g ( 1st ` v ) ) ) )
118 df-goal 
 |-  A.g j ( 1st ` s ) = <. 2o , <. j , ( 1st ` s ) >. >.
119 fvex 
 |-  ( 1st ` u ) e. _V
120 fvex 
 |-  ( 1st ` v ) e. _V
121 gonafv 
 |-  ( ( ( 1st ` u ) e. _V /\ ( 1st ` v ) e. _V ) -> ( ( 1st ` u ) |g ( 1st ` v ) ) = <. 1o , <. ( 1st ` u ) , ( 1st ` v ) >. >. )
122 119 120 121 mp2an 
 |-  ( ( 1st ` u ) |g ( 1st ` v ) ) = <. 1o , <. ( 1st ` u ) , ( 1st ` v ) >. >.
123 118 122 eqeq12i 
 |-  ( A.g j ( 1st ` s ) = ( ( 1st ` u ) |g ( 1st ` v ) ) <-> <. 2o , <. j , ( 1st ` s ) >. >. = <. 1o , <. ( 1st ` u ) , ( 1st ` v ) >. >. )
124 2oex 
 |-  2o e. _V
125 opex 
 |-  <. j , ( 1st ` s ) >. e. _V
126 124 125 opth 
 |-  ( <. 2o , <. j , ( 1st ` s ) >. >. = <. 1o , <. ( 1st ` u ) , ( 1st ` v ) >. >. <-> ( 2o = 1o /\ <. j , ( 1st ` s ) >. = <. ( 1st ` u ) , ( 1st ` v ) >. ) )
127 87 eqcoms 
 |-  ( 2o = 1o -> y = w )
128 127 adantr 
 |-  ( ( 2o = 1o /\ <. j , ( 1st ` s ) >. = <. ( 1st ` u ) , ( 1st ` v ) >. ) -> y = w )
129 126 128 sylbi 
 |-  ( <. 2o , <. j , ( 1st ` s ) >. >. = <. 1o , <. ( 1st ` u ) , ( 1st ` v ) >. >. -> y = w )
130 123 129 sylbi 
 |-  ( A.g j ( 1st ` s ) = ( ( 1st ` u ) |g ( 1st ` v ) ) -> y = w )
131 117 130 biimtrdi 
 |-  ( x = A.g j ( 1st ` s ) -> ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) -> y = w ) )
132 131 adantr 
 |-  ( ( x = A.g j ( 1st ` s ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. j , z >. } u. ( a |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } ) -> ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) -> y = w ) )
133 132 com12 
 |-  ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) -> ( ( x = A.g j ( 1st ` s ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. j , z >. } u. ( a |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } ) -> y = w ) )
134 133 adantr 
 |-  ( ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) -> ( ( x = A.g j ( 1st ` s ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. j , z >. } u. ( a |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } ) -> y = w ) )
135 134 rexlimivw 
 |-  ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) -> ( ( x = A.g j ( 1st ` s ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. j , z >. } u. ( a |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } ) -> y = w ) )
136 135 a1i 
 |-  ( ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ s e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ j e. _om ) /\ u e. ( ( S ` suc N ) \ ( S ` N ) ) ) -> ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) -> ( ( x = A.g j ( 1st ` s ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. j , z >. } u. ( a |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } ) -> y = w ) ) )
137 eqeq1 
 |-  ( x = A.g i ( 1st ` u ) -> ( x = A.g j ( 1st ` s ) <-> A.g i ( 1st ` u ) = A.g j ( 1st ` s ) ) )
138 78 118 eqeq12i 
 |-  ( A.g i ( 1st ` u ) = A.g j ( 1st ` s ) <-> <. 2o , <. i , ( 1st ` u ) >. >. = <. 2o , <. j , ( 1st ` s ) >. >. )
139 opex 
 |-  <. i , ( 1st ` u ) >. e. _V
140 124 139 opth 
 |-  ( <. 2o , <. i , ( 1st ` u ) >. >. = <. 2o , <. j , ( 1st ` s ) >. >. <-> ( 2o = 2o /\ <. i , ( 1st ` u ) >. = <. j , ( 1st ` s ) >. ) )
141 vex 
 |-  i e. _V
142 141 119 opth 
 |-  ( <. i , ( 1st ` u ) >. = <. j , ( 1st ` s ) >. <-> ( i = j /\ ( 1st ` u ) = ( 1st ` s ) ) )
143 142 anbi2i 
 |-  ( ( 2o = 2o /\ <. i , ( 1st ` u ) >. = <. j , ( 1st ` s ) >. ) <-> ( 2o = 2o /\ ( i = j /\ ( 1st ` u ) = ( 1st ` s ) ) ) )
144 138 140 143 3bitri 
 |-  ( A.g i ( 1st ` u ) = A.g j ( 1st ` s ) <-> ( 2o = 2o /\ ( i = j /\ ( 1st ` u ) = ( 1st ` s ) ) ) )
145 137 144 bitrdi 
 |-  ( x = A.g i ( 1st ` u ) -> ( x = A.g j ( 1st ` s ) <-> ( 2o = 2o /\ ( i = j /\ ( 1st ` u ) = ( 1st ` s ) ) ) ) )
146 145 adantl 
 |-  ( ( ( ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ s e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ j e. _om ) /\ u e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ i e. _om ) /\ x = A.g i ( 1st ` u ) ) -> ( x = A.g j ( 1st ` s ) <-> ( 2o = 2o /\ ( i = j /\ ( 1st ` u ) = ( 1st ` s ) ) ) ) )
147 56 a1i 
 |-  ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) -> ( s e. ( ( S ` suc N ) \ ( S ` N ) ) -> s e. ( S ` suc N ) ) )
148 funfv1st2nd 
 |-  ( ( Fun ( S ` suc N ) /\ s e. ( S ` suc N ) ) -> ( ( S ` suc N ) ` ( 1st ` s ) ) = ( 2nd ` s ) )
149 148 ex 
 |-  ( Fun ( S ` suc N ) -> ( s e. ( S ` suc N ) -> ( ( S ` suc N ) ` ( 1st ` s ) ) = ( 2nd ` s ) ) )
150 149 adantr 
 |-  ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) -> ( s e. ( S ` suc N ) -> ( ( S ` suc N ) ` ( 1st ` s ) ) = ( 2nd ` s ) ) )
151 funfv1st2nd 
 |-  ( ( Fun ( S ` suc N ) /\ u e. ( S ` suc N ) ) -> ( ( S ` suc N ) ` ( 1st ` u ) ) = ( 2nd ` u ) )
152 151 ex 
 |-  ( Fun ( S ` suc N ) -> ( u e. ( S ` suc N ) -> ( ( S ` suc N ) ` ( 1st ` u ) ) = ( 2nd ` u ) ) )
153 152 adantr 
 |-  ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) -> ( u e. ( S ` suc N ) -> ( ( S ` suc N ) ` ( 1st ` u ) ) = ( 2nd ` u ) ) )
154 fveqeq2 
 |-  ( ( 1st ` u ) = ( 1st ` s ) -> ( ( ( S ` suc N ) ` ( 1st ` u ) ) = ( 2nd ` u ) <-> ( ( S ` suc N ) ` ( 1st ` s ) ) = ( 2nd ` u ) ) )
155 eqtr2 
 |-  ( ( ( ( S ` suc N ) ` ( 1st ` s ) ) = ( 2nd ` u ) /\ ( ( S ` suc N ) ` ( 1st ` s ) ) = ( 2nd ` s ) ) -> ( 2nd ` u ) = ( 2nd ` s ) )
156 29 eqcomd 
 |-  ( i = j -> ( { <. j , z >. } u. ( a |` ( _om \ { j } ) ) ) = ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) )
157 156 adantl 
 |-  ( ( ( 2nd ` u ) = ( 2nd ` s ) /\ i = j ) -> ( { <. j , z >. } u. ( a |` ( _om \ { j } ) ) ) = ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) )
158 simpl 
 |-  ( ( ( 2nd ` u ) = ( 2nd ` s ) /\ i = j ) -> ( 2nd ` u ) = ( 2nd ` s ) )
159 158 eqcomd 
 |-  ( ( ( 2nd ` u ) = ( 2nd ` s ) /\ i = j ) -> ( 2nd ` s ) = ( 2nd ` u ) )
160 157 159 eleq12d 
 |-  ( ( ( 2nd ` u ) = ( 2nd ` s ) /\ i = j ) -> ( ( { <. j , z >. } u. ( a |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) <-> ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) ) )
161 160 ralbidv 
 |-  ( ( ( 2nd ` u ) = ( 2nd ` s ) /\ i = j ) -> ( A. z e. M ( { <. j , z >. } u. ( a |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) <-> A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) ) )
162 161 rabbidv 
 |-  ( ( ( 2nd ` u ) = ( 2nd ` s ) /\ i = j ) -> { a e. ( M ^m _om ) | A. z e. M ( { <. j , z >. } u. ( a |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } )
163 162 3 eqtr4di 
 |-  ( ( ( 2nd ` u ) = ( 2nd ` s ) /\ i = j ) -> { a e. ( M ^m _om ) | A. z e. M ( { <. j , z >. } u. ( a |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } = B )
164 eqeq12 
 |-  ( ( y = { a e. ( M ^m _om ) | A. z e. M ( { <. j , z >. } u. ( a |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } /\ w = B ) -> ( y = w <-> { a e. ( M ^m _om ) | A. z e. M ( { <. j , z >. } u. ( a |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } = B ) )
165 163 164 syl5ibrcom 
 |-  ( ( ( 2nd ` u ) = ( 2nd ` s ) /\ i = j ) -> ( ( y = { a e. ( M ^m _om ) | A. z e. M ( { <. j , z >. } u. ( a |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } /\ w = B ) -> y = w ) )
166 165 exp4b 
 |-  ( ( 2nd ` u ) = ( 2nd ` s ) -> ( i = j -> ( y = { a e. ( M ^m _om ) | A. z e. M ( { <. j , z >. } u. ( a |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } -> ( w = B -> y = w ) ) ) )
167 155 166 syl 
 |-  ( ( ( ( S ` suc N ) ` ( 1st ` s ) ) = ( 2nd ` u ) /\ ( ( S ` suc N ) ` ( 1st ` s ) ) = ( 2nd ` s ) ) -> ( i = j -> ( y = { a e. ( M ^m _om ) | A. z e. M ( { <. j , z >. } u. ( a |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } -> ( w = B -> y = w ) ) ) )
168 167 ex 
 |-  ( ( ( S ` suc N ) ` ( 1st ` s ) ) = ( 2nd ` u ) -> ( ( ( S ` suc N ) ` ( 1st ` s ) ) = ( 2nd ` s ) -> ( i = j -> ( y = { a e. ( M ^m _om ) | A. z e. M ( { <. j , z >. } u. ( a |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } -> ( w = B -> y = w ) ) ) ) )
169 154 168 biimtrdi 
 |-  ( ( 1st ` u ) = ( 1st ` s ) -> ( ( ( S ` suc N ) ` ( 1st ` u ) ) = ( 2nd ` u ) -> ( ( ( S ` suc N ) ` ( 1st ` s ) ) = ( 2nd ` s ) -> ( i = j -> ( y = { a e. ( M ^m _om ) | A. z e. M ( { <. j , z >. } u. ( a |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } -> ( w = B -> y = w ) ) ) ) ) )
170 169 com24 
 |-  ( ( 1st ` u ) = ( 1st ` s ) -> ( i = j -> ( ( ( S ` suc N ) ` ( 1st ` s ) ) = ( 2nd ` s ) -> ( ( ( S ` suc N ) ` ( 1st ` u ) ) = ( 2nd ` u ) -> ( y = { a e. ( M ^m _om ) | A. z e. M ( { <. j , z >. } u. ( a |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } -> ( w = B -> y = w ) ) ) ) ) )
171 170 impcom 
 |-  ( ( i = j /\ ( 1st ` u ) = ( 1st ` s ) ) -> ( ( ( S ` suc N ) ` ( 1st ` s ) ) = ( 2nd ` s ) -> ( ( ( S ` suc N ) ` ( 1st ` u ) ) = ( 2nd ` u ) -> ( y = { a e. ( M ^m _om ) | A. z e. M ( { <. j , z >. } u. ( a |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } -> ( w = B -> y = w ) ) ) ) )
172 171 com13 
 |-  ( ( ( S ` suc N ) ` ( 1st ` u ) ) = ( 2nd ` u ) -> ( ( ( S ` suc N ) ` ( 1st ` s ) ) = ( 2nd ` s ) -> ( ( i = j /\ ( 1st ` u ) = ( 1st ` s ) ) -> ( y = { a e. ( M ^m _om ) | A. z e. M ( { <. j , z >. } u. ( a |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } -> ( w = B -> y = w ) ) ) ) )
173 60 153 172 syl56 
 |-  ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) -> ( u e. ( ( S ` suc N ) \ ( S ` N ) ) -> ( ( ( S ` suc N ) ` ( 1st ` s ) ) = ( 2nd ` s ) -> ( ( i = j /\ ( 1st ` u ) = ( 1st ` s ) ) -> ( y = { a e. ( M ^m _om ) | A. z e. M ( { <. j , z >. } u. ( a |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } -> ( w = B -> y = w ) ) ) ) ) )
174 173 com23 
 |-  ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) -> ( ( ( S ` suc N ) ` ( 1st ` s ) ) = ( 2nd ` s ) -> ( u e. ( ( S ` suc N ) \ ( S ` N ) ) -> ( ( i = j /\ ( 1st ` u ) = ( 1st ` s ) ) -> ( y = { a e. ( M ^m _om ) | A. z e. M ( { <. j , z >. } u. ( a |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } -> ( w = B -> y = w ) ) ) ) ) )
175 147 150 174 3syld 
 |-  ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) -> ( s e. ( ( S ` suc N ) \ ( S ` N ) ) -> ( u e. ( ( S ` suc N ) \ ( S ` N ) ) -> ( ( i = j /\ ( 1st ` u ) = ( 1st ` s ) ) -> ( y = { a e. ( M ^m _om ) | A. z e. M ( { <. j , z >. } u. ( a |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } -> ( w = B -> y = w ) ) ) ) ) )
176 175 imp 
 |-  ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ s e. ( ( S ` suc N ) \ ( S ` N ) ) ) -> ( u e. ( ( S ` suc N ) \ ( S ` N ) ) -> ( ( i = j /\ ( 1st ` u ) = ( 1st ` s ) ) -> ( y = { a e. ( M ^m _om ) | A. z e. M ( { <. j , z >. } u. ( a |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } -> ( w = B -> y = w ) ) ) ) )
177 176 adantr 
 |-  ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ s e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ j e. _om ) -> ( u e. ( ( S ` suc N ) \ ( S ` N ) ) -> ( ( i = j /\ ( 1st ` u ) = ( 1st ` s ) ) -> ( y = { a e. ( M ^m _om ) | A. z e. M ( { <. j , z >. } u. ( a |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } -> ( w = B -> y = w ) ) ) ) )
178 177 imp 
 |-  ( ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ s e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ j e. _om ) /\ u e. ( ( S ` suc N ) \ ( S ` N ) ) ) -> ( ( i = j /\ ( 1st ` u ) = ( 1st ` s ) ) -> ( y = { a e. ( M ^m _om ) | A. z e. M ( { <. j , z >. } u. ( a |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } -> ( w = B -> y = w ) ) ) )
179 178 adantld 
 |-  ( ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ s e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ j e. _om ) /\ u e. ( ( S ` suc N ) \ ( S ` N ) ) ) -> ( ( 2o = 2o /\ ( i = j /\ ( 1st ` u ) = ( 1st ` s ) ) ) -> ( y = { a e. ( M ^m _om ) | A. z e. M ( { <. j , z >. } u. ( a |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } -> ( w = B -> y = w ) ) ) )
180 179 ad2antrr 
 |-  ( ( ( ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ s e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ j e. _om ) /\ u e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ i e. _om ) /\ x = A.g i ( 1st ` u ) ) -> ( ( 2o = 2o /\ ( i = j /\ ( 1st ` u ) = ( 1st ` s ) ) ) -> ( y = { a e. ( M ^m _om ) | A. z e. M ( { <. j , z >. } u. ( a |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } -> ( w = B -> y = w ) ) ) )
181 146 180 sylbid 
 |-  ( ( ( ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ s e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ j e. _om ) /\ u e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ i e. _om ) /\ x = A.g i ( 1st ` u ) ) -> ( x = A.g j ( 1st ` s ) -> ( y = { a e. ( M ^m _om ) | A. z e. M ( { <. j , z >. } u. ( a |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } -> ( w = B -> y = w ) ) ) )
182 181 impd 
 |-  ( ( ( ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ s e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ j e. _om ) /\ u e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ i e. _om ) /\ x = A.g i ( 1st ` u ) ) -> ( ( x = A.g j ( 1st ` s ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. j , z >. } u. ( a |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } ) -> ( w = B -> y = w ) ) )
183 182 ex 
 |-  ( ( ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ s e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ j e. _om ) /\ u e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ i e. _om ) -> ( x = A.g i ( 1st ` u ) -> ( ( x = A.g j ( 1st ` s ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. j , z >. } u. ( a |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } ) -> ( w = B -> y = w ) ) ) )
184 183 com34 
 |-  ( ( ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ s e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ j e. _om ) /\ u e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ i e. _om ) -> ( x = A.g i ( 1st ` u ) -> ( w = B -> ( ( x = A.g j ( 1st ` s ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. j , z >. } u. ( a |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } ) -> y = w ) ) ) )
185 184 impd 
 |-  ( ( ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ s e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ j e. _om ) /\ u e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ i e. _om ) -> ( ( x = A.g i ( 1st ` u ) /\ w = B ) -> ( ( x = A.g j ( 1st ` s ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. j , z >. } u. ( a |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } ) -> y = w ) ) )
186 185 rexlimdva 
 |-  ( ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ s e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ j e. _om ) /\ u e. ( ( S ` suc N ) \ ( S ` N ) ) ) -> ( E. i e. _om ( x = A.g i ( 1st ` u ) /\ w = B ) -> ( ( x = A.g j ( 1st ` s ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. j , z >. } u. ( a |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } ) -> y = w ) ) )
187 136 186 jaod 
 |-  ( ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ s e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ j e. _om ) /\ u e. ( ( S ` suc N ) \ ( S ` N ) ) ) -> ( ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ w = B ) ) -> ( ( x = A.g j ( 1st ` s ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. j , z >. } u. ( a |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } ) -> y = w ) ) )
188 187 rexlimdva 
 |-  ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ s e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ j e. _om ) -> ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ w = B ) ) -> ( ( x = A.g j ( 1st ` s ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. j , z >. } u. ( a |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } ) -> y = w ) ) )
189 134 a1i 
 |-  ( ( ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ s e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ j e. _om ) /\ u e. ( S ` N ) ) /\ v e. ( ( S ` suc N ) \ ( S ` N ) ) ) -> ( ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) -> ( ( x = A.g j ( 1st ` s ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. j , z >. } u. ( a |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } ) -> y = w ) ) )
190 189 rexlimdva 
 |-  ( ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ s e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ j e. _om ) /\ u e. ( S ` N ) ) -> ( E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) -> ( ( x = A.g j ( 1st ` s ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. j , z >. } u. ( a |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } ) -> y = w ) ) )
191 190 rexlimdva 
 |-  ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ s e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ j e. _om ) -> ( E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) -> ( ( x = A.g j ( 1st ` s ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. j , z >. } u. ( a |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } ) -> y = w ) ) )
192 188 191 jaod 
 |-  ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ s e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ j e. _om ) -> ( ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ w = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) ) -> ( ( x = A.g j ( 1st ` s ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. j , z >. } u. ( a |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } ) -> y = w ) ) )
193 192 com23 
 |-  ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ s e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ j e. _om ) -> ( ( x = A.g j ( 1st ` s ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. j , z >. } u. ( a |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } ) -> ( ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ w = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) ) -> y = w ) ) )
194 193 rexlimdva 
 |-  ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ s e. ( ( S ` suc N ) \ ( S ` N ) ) ) -> ( E. j e. _om ( x = A.g j ( 1st ` s ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. j , z >. } u. ( a |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } ) -> ( ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ w = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) ) -> y = w ) ) )
195 116 194 jaod 
 |-  ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ s e. ( ( S ` suc N ) \ ( S ` N ) ) ) -> ( ( E. r e. ( S ` suc N ) ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) \/ E. j e. _om ( x = A.g j ( 1st ` s ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. j , z >. } u. ( a |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } ) ) -> ( ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ w = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) ) -> y = w ) ) )
196 195 rexlimdva 
 |-  ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) -> ( E. s e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. r e. ( S ` suc N ) ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) \/ E. j e. _om ( x = A.g j ( 1st ` s ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. j , z >. } u. ( a |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } ) ) -> ( ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ w = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) ) -> y = w ) ) )
197 simplll 
 |-  ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ ( s e. ( S ` N ) /\ r e. ( ( S ` suc N ) \ ( S ` N ) ) ) ) /\ ( u e. ( ( S ` suc N ) \ ( S ` N ) ) /\ v e. ( S ` suc N ) ) ) -> Fun ( S ` suc N ) )
198 ssel 
 |-  ( ( S ` N ) C_ ( S ` suc N ) -> ( s e. ( S ` N ) -> s e. ( S ` suc N ) ) )
199 198 adantrd 
 |-  ( ( S ` N ) C_ ( S ` suc N ) -> ( ( s e. ( S ` N ) /\ r e. ( ( S ` suc N ) \ ( S ` N ) ) ) -> s e. ( S ` suc N ) ) )
200 199 adantl 
 |-  ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) -> ( ( s e. ( S ` N ) /\ r e. ( ( S ` suc N ) \ ( S ` N ) ) ) -> s e. ( S ` suc N ) ) )
201 200 imp 
 |-  ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ ( s e. ( S ` N ) /\ r e. ( ( S ` suc N ) \ ( S ` N ) ) ) ) -> s e. ( S ` suc N ) )
202 eldifi 
 |-  ( r e. ( ( S ` suc N ) \ ( S ` N ) ) -> r e. ( S ` suc N ) )
203 202 ad2antll 
 |-  ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ ( s e. ( S ` N ) /\ r e. ( ( S ` suc N ) \ ( S ` N ) ) ) ) -> r e. ( S ` suc N ) )
204 201 203 jca 
 |-  ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ ( s e. ( S ` N ) /\ r e. ( ( S ` suc N ) \ ( S ` N ) ) ) ) -> ( s e. ( S ` suc N ) /\ r e. ( S ` suc N ) ) )
205 204 adantr 
 |-  ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ ( s e. ( S ` N ) /\ r e. ( ( S ` suc N ) \ ( S ` N ) ) ) ) /\ ( u e. ( ( S ` suc N ) \ ( S ` N ) ) /\ v e. ( S ` suc N ) ) ) -> ( s e. ( S ` suc N ) /\ r e. ( S ` suc N ) ) )
206 60 anim1i 
 |-  ( ( u e. ( ( S ` suc N ) \ ( S ` N ) ) /\ v e. ( S ` suc N ) ) -> ( u e. ( S ` suc N ) /\ v e. ( S ` suc N ) ) )
207 206 adantl 
 |-  ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ ( s e. ( S ` N ) /\ r e. ( ( S ` suc N ) \ ( S ` N ) ) ) ) /\ ( u e. ( ( S ` suc N ) \ ( S ` N ) ) /\ v e. ( S ` suc N ) ) ) -> ( u e. ( S ` suc N ) /\ v e. ( S ` suc N ) ) )
208 197 205 207 3jca 
 |-  ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ ( s e. ( S ` N ) /\ r e. ( ( S ` suc N ) \ ( S ` N ) ) ) ) /\ ( u e. ( ( S ` suc N ) \ ( S ` N ) ) /\ v e. ( S ` suc N ) ) ) -> ( Fun ( S ` suc N ) /\ ( s e. ( S ` suc N ) /\ r e. ( S ` suc N ) ) /\ ( u e. ( S ` suc N ) /\ v e. ( S ` suc N ) ) ) )
209 208 adantr 
 |-  ( ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ ( s e. ( S ` N ) /\ r e. ( ( S ` suc N ) \ ( S ` N ) ) ) ) /\ ( u e. ( ( S ` suc N ) \ ( S ` N ) ) /\ v e. ( S ` suc N ) ) ) /\ ( ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) /\ ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) ) ) -> ( Fun ( S ` suc N ) /\ ( s e. ( S ` suc N ) /\ r e. ( S ` suc N ) ) /\ ( u e. ( S ` suc N ) /\ v e. ( S ` suc N ) ) ) )
210 simprl 
 |-  ( ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ ( s e. ( S ` N ) /\ r e. ( ( S ` suc N ) \ ( S ` N ) ) ) ) /\ ( u e. ( ( S ` suc N ) \ ( S ` N ) ) /\ v e. ( S ` suc N ) ) ) /\ ( ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) /\ ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) ) ) -> ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) )
211 67 ad2antll 
 |-  ( ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ ( s e. ( S ` N ) /\ r e. ( ( S ` suc N ) \ ( S ` N ) ) ) ) /\ ( u e. ( ( S ` suc N ) \ ( S ` N ) ) /\ v e. ( S ` suc N ) ) ) /\ ( ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) /\ ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) ) ) -> ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) )
212 209 210 211 68 syl3anc 
 |-  ( ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ ( s e. ( S ` N ) /\ r e. ( ( S ` suc N ) \ ( S ` N ) ) ) ) /\ ( u e. ( ( S ` suc N ) \ ( S ` N ) ) /\ v e. ( S ` suc N ) ) ) /\ ( ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) /\ ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) ) ) -> y = w )
213 212 exp32 
 |-  ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ ( s e. ( S ` N ) /\ r e. ( ( S ` suc N ) \ ( S ` N ) ) ) ) /\ ( u e. ( ( S ` suc N ) \ ( S ` N ) ) /\ v e. ( S ` suc N ) ) ) -> ( ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) -> ( ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) -> y = w ) ) )
214 213 impancom 
 |-  ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ ( s e. ( S ` N ) /\ r e. ( ( S ` suc N ) \ ( S ` N ) ) ) ) /\ ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) ) -> ( ( u e. ( ( S ` suc N ) \ ( S ` N ) ) /\ v e. ( S ` suc N ) ) -> ( ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) -> y = w ) ) )
215 214 expdimp 
 |-  ( ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ ( s e. ( S ` N ) /\ r e. ( ( S ` suc N ) \ ( S ` N ) ) ) ) /\ ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) ) /\ u e. ( ( S ` suc N ) \ ( S ` N ) ) ) -> ( v e. ( S ` suc N ) -> ( ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) -> y = w ) ) )
216 215 rexlimdv 
 |-  ( ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ ( s e. ( S ` N ) /\ r e. ( ( S ` suc N ) \ ( S ` N ) ) ) ) /\ ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) ) /\ u e. ( ( S ` suc N ) \ ( S ` N ) ) ) -> ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) -> y = w ) )
217 91 adantrd 
 |-  ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) -> ( ( x = A.g i ( 1st ` u ) /\ w = B ) -> y = w ) )
218 217 adantr 
 |-  ( ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) -> ( ( x = A.g i ( 1st ` u ) /\ w = B ) -> y = w ) )
219 218 ad3antlr 
 |-  ( ( ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ ( s e. ( S ` N ) /\ r e. ( ( S ` suc N ) \ ( S ` N ) ) ) ) /\ ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) ) /\ u e. ( ( S ` suc N ) \ ( S ` N ) ) ) /\ i e. _om ) -> ( ( x = A.g i ( 1st ` u ) /\ w = B ) -> y = w ) )
220 219 rexlimdva 
 |-  ( ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ ( s e. ( S ` N ) /\ r e. ( ( S ` suc N ) \ ( S ` N ) ) ) ) /\ ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) ) /\ u e. ( ( S ` suc N ) \ ( S ` N ) ) ) -> ( E. i e. _om ( x = A.g i ( 1st ` u ) /\ w = B ) -> y = w ) )
221 216 220 jaod 
 |-  ( ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ ( s e. ( S ` N ) /\ r e. ( ( S ` suc N ) \ ( S ` N ) ) ) ) /\ ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) ) /\ u e. ( ( S ` suc N ) \ ( S ` N ) ) ) -> ( ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ w = B ) ) -> y = w ) )
222 221 rexlimdva 
 |-  ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ ( s e. ( S ` N ) /\ r e. ( ( S ` suc N ) \ ( S ` N ) ) ) ) /\ ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) ) -> ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ w = B ) ) -> y = w ) )
223 simplll 
 |-  ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ ( s e. ( S ` N ) /\ r e. ( ( S ` suc N ) \ ( S ` N ) ) ) ) /\ ( u e. ( S ` N ) /\ v e. ( ( S ` suc N ) \ ( S ` N ) ) ) ) -> Fun ( S ` suc N ) )
224 204 adantr 
 |-  ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ ( s e. ( S ` N ) /\ r e. ( ( S ` suc N ) \ ( S ` N ) ) ) ) /\ ( u e. ( S ` N ) /\ v e. ( ( S ` suc N ) \ ( S ` N ) ) ) ) -> ( s e. ( S ` suc N ) /\ r e. ( S ` suc N ) ) )
225 101 adantl 
 |-  ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) -> ( u e. ( S ` N ) -> u e. ( S ` suc N ) ) )
226 225 adantr 
 |-  ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ ( s e. ( S ` N ) /\ r e. ( ( S ` suc N ) \ ( S ` N ) ) ) ) -> ( u e. ( S ` N ) -> u e. ( S ` suc N ) ) )
227 226 com12 
 |-  ( u e. ( S ` N ) -> ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ ( s e. ( S ` N ) /\ r e. ( ( S ` suc N ) \ ( S ` N ) ) ) ) -> u e. ( S ` suc N ) ) )
228 227 adantr 
 |-  ( ( u e. ( S ` N ) /\ v e. ( ( S ` suc N ) \ ( S ` N ) ) ) -> ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ ( s e. ( S ` N ) /\ r e. ( ( S ` suc N ) \ ( S ` N ) ) ) ) -> u e. ( S ` suc N ) ) )
229 228 impcom 
 |-  ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ ( s e. ( S ` N ) /\ r e. ( ( S ` suc N ) \ ( S ` N ) ) ) ) /\ ( u e. ( S ` N ) /\ v e. ( ( S ` suc N ) \ ( S ` N ) ) ) ) -> u e. ( S ` suc N ) )
230 106 ad2antll 
 |-  ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ ( s e. ( S ` N ) /\ r e. ( ( S ` suc N ) \ ( S ` N ) ) ) ) /\ ( u e. ( S ` N ) /\ v e. ( ( S ` suc N ) \ ( S ` N ) ) ) ) -> v e. ( S ` suc N ) )
231 229 230 jca 
 |-  ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ ( s e. ( S ` N ) /\ r e. ( ( S ` suc N ) \ ( S ` N ) ) ) ) /\ ( u e. ( S ` N ) /\ v e. ( ( S ` suc N ) \ ( S ` N ) ) ) ) -> ( u e. ( S ` suc N ) /\ v e. ( S ` suc N ) ) )
232 223 224 231 3jca 
 |-  ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ ( s e. ( S ` N ) /\ r e. ( ( S ` suc N ) \ ( S ` N ) ) ) ) /\ ( u e. ( S ` N ) /\ v e. ( ( S ` suc N ) \ ( S ` N ) ) ) ) -> ( Fun ( S ` suc N ) /\ ( s e. ( S ` suc N ) /\ r e. ( S ` suc N ) ) /\ ( u e. ( S ` suc N ) /\ v e. ( S ` suc N ) ) ) )
233 232 64 67 68 syl3an 
 |-  ( ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ ( s e. ( S ` N ) /\ r e. ( ( S ` suc N ) \ ( S ` N ) ) ) ) /\ ( u e. ( S ` N ) /\ v e. ( ( S ` suc N ) \ ( S ` N ) ) ) ) /\ ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) /\ ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) ) -> y = w )
234 233 3exp 
 |-  ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ ( s e. ( S ` N ) /\ r e. ( ( S ` suc N ) \ ( S ` N ) ) ) ) /\ ( u e. ( S ` N ) /\ v e. ( ( S ` suc N ) \ ( S ` N ) ) ) ) -> ( ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) -> ( ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) -> y = w ) ) )
235 234 impancom 
 |-  ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ ( s e. ( S ` N ) /\ r e. ( ( S ` suc N ) \ ( S ` N ) ) ) ) /\ ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) ) -> ( ( u e. ( S ` N ) /\ v e. ( ( S ` suc N ) \ ( S ` N ) ) ) -> ( ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) -> y = w ) ) )
236 235 rexlimdvv 
 |-  ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ ( s e. ( S ` N ) /\ r e. ( ( S ` suc N ) \ ( S ` N ) ) ) ) /\ ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) ) -> ( E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) -> y = w ) )
237 222 236 jaod 
 |-  ( ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ ( s e. ( S ` N ) /\ r e. ( ( S ` suc N ) \ ( S ` N ) ) ) ) /\ ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) ) -> ( ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ w = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) ) -> y = w ) )
238 237 ex 
 |-  ( ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) /\ ( s e. ( S ` N ) /\ r e. ( ( S ` suc N ) \ ( S ` N ) ) ) ) -> ( ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) -> ( ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ w = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) ) -> y = w ) ) )
239 238 rexlimdvva 
 |-  ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) -> ( E. s e. ( S ` N ) E. r e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) -> ( ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ w = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) ) -> y = w ) ) )
240 196 239 jaod 
 |-  ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) -> ( ( E. s e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. r e. ( S ` suc N ) ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) \/ E. j e. _om ( x = A.g j ( 1st ` s ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. j , z >. } u. ( a |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } ) ) \/ E. s e. ( S ` N ) E. r e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) ) -> ( ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ w = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) ) -> y = w ) ) )
241 54 240 biimtrid 
 |-  ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) -> ( ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) -> ( ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ w = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) ) -> y = w ) ) )
242 241 impd 
 |-  ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) -> ( ( ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) /\ ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ w = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) ) ) -> y = w ) )
243 242 alrimivv 
 |-  ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) -> A. y A. w ( ( ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) /\ ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ w = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) ) ) -> y = w ) )
244 eqeq1 
 |-  ( y = w -> ( y = A <-> w = A ) )
245 244 anbi2d 
 |-  ( y = w -> ( ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) <-> ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) ) )
246 245 rexbidv 
 |-  ( y = w -> ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) <-> E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) ) )
247 eqeq1 
 |-  ( y = w -> ( y = B <-> w = B ) )
248 247 anbi2d 
 |-  ( y = w -> ( ( x = A.g i ( 1st ` u ) /\ y = B ) <-> ( x = A.g i ( 1st ` u ) /\ w = B ) ) )
249 248 rexbidv 
 |-  ( y = w -> ( E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) <-> E. i e. _om ( x = A.g i ( 1st ` u ) /\ w = B ) ) )
250 246 249 orbi12d 
 |-  ( y = w -> ( ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) <-> ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ w = B ) ) ) )
251 250 rexbidv 
 |-  ( y = w -> ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) <-> E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ w = B ) ) ) )
252 245 2rexbidv 
 |-  ( y = w -> ( E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) <-> E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) ) )
253 251 252 orbi12d 
 |-  ( y = w -> ( ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) <-> ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ w = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) ) ) )
254 253 mo4 
 |-  ( E* y ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) <-> A. y A. w ( ( ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) /\ ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ w = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = A ) ) ) -> y = w ) )
255 243 254 sylibr 
 |-  ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) -> E* y ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) )
256 255 alrimiv 
 |-  ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) -> A. x E* y ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) )
257 funopab 
 |-  ( Fun { <. x , y >. | ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) } <-> A. x E* y ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) )
258 256 257 sylibr 
 |-  ( ( Fun ( S ` suc N ) /\ ( S ` N ) C_ ( S ` suc N ) ) -> Fun { <. x , y >. | ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) } )