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 syl5eq
 |-  ( ( 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 syl5bb
 |-  ( ( 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 syl5bb
 |-  ( ( 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 syl6bi
 |-  ( 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 syl6bi
 |-  ( 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 syl6bi
 |-  ( ( 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 syl5bi
 |-  ( ( 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 ) ) } )