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

Metamath Proof Explorer

Theorem satffunlem1lem1

Description: Lemma for satffunlem1 . (Contributed by AV, 17-Oct-2023)

Ref Expression
Assertion satffunlem1lem1 
|- ( Fun ( ( M Sat E ) ` N ) -> Fun { <. x , y >. | E. u e. ( ( M Sat E ) ` N ) ( E. v e. ( ( M Sat E ) ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( u = s -> ( 1st ` u ) = ( 1st ` s ) )
2 fveq2 
 |-  ( v = r -> ( 1st ` v ) = ( 1st ` r ) )
3 1 2 oveqan12d 
 |-  ( ( u = s /\ v = r ) -> ( ( 1st ` u ) |g ( 1st ` v ) ) = ( ( 1st ` s ) |g ( 1st ` r ) ) )
4 3 eqeq2d 
 |-  ( ( u = s /\ v = r ) -> ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) <-> x = ( ( 1st ` s ) |g ( 1st ` r ) ) ) )
5 fveq2 
 |-  ( u = s -> ( 2nd ` u ) = ( 2nd ` s ) )
6 fveq2 
 |-  ( v = r -> ( 2nd ` v ) = ( 2nd ` r ) )
7 5 6 ineqan12d 
 |-  ( ( u = s /\ v = r ) -> ( ( 2nd ` u ) i^i ( 2nd ` v ) ) = ( ( 2nd ` s ) i^i ( 2nd ` r ) ) )
8 7 difeq2d 
 |-  ( ( u = s /\ v = r ) -> ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) )
9 8 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 ) ) ) ) )
10 4 9 anbi12d 
 |-  ( ( u = s /\ v = r ) -> ( ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) <-> ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) ) )
11 10 cbvrexdva 
 |-  ( u = s -> ( E. v e. ( ( M Sat E ) ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) <-> E. r e. ( ( M Sat E ) ` N ) ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) ) )
12 simpr 
 |-  ( ( u = s /\ i = j ) -> i = j )
13 1 adantr 
 |-  ( ( u = s /\ i = j ) -> ( 1st ` u ) = ( 1st ` s ) )
14 12 13 goaleq12d 
 |-  ( ( u = s /\ i = j ) -> A.g i ( 1st ` u ) = A.g j ( 1st ` s ) )
15 14 eqeq2d 
 |-  ( ( u = s /\ i = j ) -> ( x = A.g i ( 1st ` u ) <-> x = A.g j ( 1st ` s ) ) )
16 opeq1 
 |-  ( i = j -> <. i , k >. = <. j , k >. )
17 16 sneqd 
 |-  ( i = j -> { <. i , k >. } = { <. j , k >. } )
18 sneq 
 |-  ( i = j -> { i } = { j } )
19 18 difeq2d 
 |-  ( i = j -> ( _om \ { i } ) = ( _om \ { j } ) )
20 19 reseq2d 
 |-  ( i = j -> ( f |` ( _om \ { i } ) ) = ( f |` ( _om \ { j } ) ) )
21 17 20 uneq12d 
 |-  ( i = j -> ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) = ( { <. j , k >. } u. ( f |` ( _om \ { j } ) ) ) )
22 21 adantl 
 |-  ( ( u = s /\ i = j ) -> ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) = ( { <. j , k >. } u. ( f |` ( _om \ { j } ) ) ) )
23 5 adantr 
 |-  ( ( u = s /\ i = j ) -> ( 2nd ` u ) = ( 2nd ` s ) )
24 22 23 eleq12d 
 |-  ( ( u = s /\ i = j ) -> ( ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) <-> ( { <. j , k >. } u. ( f |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) ) )
25 24 ralbidv 
 |-  ( ( u = s /\ i = j ) -> ( A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) <-> A. k e. M ( { <. j , k >. } u. ( f |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) ) )
26 25 rabbidv 
 |-  ( ( u = s /\ i = j ) -> { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } = { f e. ( M ^m _om ) | A. k e. M ( { <. j , k >. } u. ( f |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } )
27 26 eqeq2d 
 |-  ( ( u = s /\ i = j ) -> ( y = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } <-> y = { f e. ( M ^m _om ) | A. k e. M ( { <. j , k >. } u. ( f |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } ) )
28 15 27 anbi12d 
 |-  ( ( u = s /\ i = j ) -> ( ( x = A.g i ( 1st ` u ) /\ y = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) <-> ( x = A.g j ( 1st ` s ) /\ y = { f e. ( M ^m _om ) | A. k e. M ( { <. j , k >. } u. ( f |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } ) ) )
29 28 cbvrexdva 
 |-  ( u = s -> ( E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) <-> E. j e. _om ( x = A.g j ( 1st ` s ) /\ y = { f e. ( M ^m _om ) | A. k e. M ( { <. j , k >. } u. ( f |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } ) ) )
30 11 29 orbi12d 
 |-  ( u = s -> ( ( E. v e. ( ( M Sat E ) ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) <-> ( E. r e. ( ( M Sat E ) ` 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 = { f e. ( M ^m _om ) | A. k e. M ( { <. j , k >. } u. ( f |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } ) ) ) )
31 30 cbvrexvw 
 |-  ( E. u e. ( ( M Sat E ) ` N ) ( E. v e. ( ( M Sat E ) ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) <-> E. s e. ( ( M Sat E ) ` N ) ( E. r e. ( ( M Sat E ) ` 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 = { f e. ( M ^m _om ) | A. k e. M ( { <. j , k >. } u. ( f |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } ) ) )
32 simp-4l 
 |-  ( ( ( ( ( Fun ( ( M Sat E ) ` N ) /\ s e. ( ( M Sat E ) ` N ) ) /\ r e. ( ( M Sat E ) ` N ) ) /\ u e. ( ( M Sat E ) ` N ) ) /\ v e. ( ( M Sat E ) ` N ) ) -> Fun ( ( M Sat E ) ` N ) )
33 simpr 
 |-  ( ( ( ( Fun ( ( M Sat E ) ` N ) /\ s e. ( ( M Sat E ) ` N ) ) /\ r e. ( ( M Sat E ) ` N ) ) /\ u e. ( ( M Sat E ) ` N ) ) -> u e. ( ( M Sat E ) ` N ) )
34 33 anim1i 
 |-  ( ( ( ( ( Fun ( ( M Sat E ) ` N ) /\ s e. ( ( M Sat E ) ` N ) ) /\ r e. ( ( M Sat E ) ` N ) ) /\ u e. ( ( M Sat E ) ` N ) ) /\ v e. ( ( M Sat E ) ` N ) ) -> ( u e. ( ( M Sat E ) ` N ) /\ v e. ( ( M Sat E ) ` N ) ) )
35 simpr 
 |-  ( ( Fun ( ( M Sat E ) ` N ) /\ s e. ( ( M Sat E ) ` N ) ) -> s e. ( ( M Sat E ) ` N ) )
36 35 anim1i 
 |-  ( ( ( Fun ( ( M Sat E ) ` N ) /\ s e. ( ( M Sat E ) ` N ) ) /\ r e. ( ( M Sat E ) ` N ) ) -> ( s e. ( ( M Sat E ) ` N ) /\ r e. ( ( M Sat E ) ` N ) ) )
37 36 ad2antrr 
 |-  ( ( ( ( ( Fun ( ( M Sat E ) ` N ) /\ s e. ( ( M Sat E ) ` N ) ) /\ r e. ( ( M Sat E ) ` N ) ) /\ u e. ( ( M Sat E ) ` N ) ) /\ v e. ( ( M Sat E ) ` N ) ) -> ( s e. ( ( M Sat E ) ` N ) /\ r e. ( ( M Sat E ) ` N ) ) )
38 satffunlem 
 |-  ( ( ( Fun ( ( M Sat E ) ` N ) /\ ( u e. ( ( M Sat E ) ` N ) /\ v e. ( ( M Sat E ) ` N ) ) /\ ( s e. ( ( M Sat E ) ` N ) /\ r e. ( ( M Sat E ) ` N ) ) ) /\ ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ z = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) /\ ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) ) -> z = y )
39 38 eqcomd 
 |-  ( ( ( Fun ( ( M Sat E ) ` N ) /\ ( u e. ( ( M Sat E ) ` N ) /\ v e. ( ( M Sat E ) ` N ) ) /\ ( s e. ( ( M Sat E ) ` N ) /\ r e. ( ( M Sat E ) ` N ) ) ) /\ ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ z = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) /\ ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) ) -> y = z )
40 39 3exp 
 |-  ( ( Fun ( ( M Sat E ) ` N ) /\ ( u e. ( ( M Sat E ) ` N ) /\ v e. ( ( M Sat E ) ` N ) ) /\ ( s e. ( ( M Sat E ) ` N ) /\ r e. ( ( M Sat E ) ` N ) ) ) -> ( ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ z = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) -> ( ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) -> y = z ) ) )
41 32 34 37 40 syl3anc 
 |-  ( ( ( ( ( Fun ( ( M Sat E ) ` N ) /\ s e. ( ( M Sat E ) ` N ) ) /\ r e. ( ( M Sat E ) ` N ) ) /\ u e. ( ( M Sat E ) ` N ) ) /\ v e. ( ( M Sat E ) ` N ) ) -> ( ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ z = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) -> ( ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) -> y = z ) ) )
42 41 rexlimdva 
 |-  ( ( ( ( Fun ( ( M Sat E ) ` N ) /\ s e. ( ( M Sat E ) ` N ) ) /\ r e. ( ( M Sat E ) ` N ) ) /\ u e. ( ( M Sat E ) ` N ) ) -> ( E. v e. ( ( M Sat E ) ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ z = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) -> ( ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) -> y = z ) ) )
43 eqeq1 
 |-  ( x = A.g i ( 1st ` u ) -> ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) <-> A.g i ( 1st ` u ) = ( ( 1st ` s ) |g ( 1st ` r ) ) ) )
44 df-goal 
 |-  A.g i ( 1st ` u ) = <. 2o , <. i , ( 1st ` u ) >. >.
45 fvex 
 |-  ( 1st ` s ) e. _V
46 fvex 
 |-  ( 1st ` r ) e. _V
47 gonafv 
 |-  ( ( ( 1st ` s ) e. _V /\ ( 1st ` r ) e. _V ) -> ( ( 1st ` s ) |g ( 1st ` r ) ) = <. 1o , <. ( 1st ` s ) , ( 1st ` r ) >. >. )
48 45 46 47 mp2an 
 |-  ( ( 1st ` s ) |g ( 1st ` r ) ) = <. 1o , <. ( 1st ` s ) , ( 1st ` r ) >. >.
49 44 48 eqeq12i 
 |-  ( A.g i ( 1st ` u ) = ( ( 1st ` s ) |g ( 1st ` r ) ) <-> <. 2o , <. i , ( 1st ` u ) >. >. = <. 1o , <. ( 1st ` s ) , ( 1st ` r ) >. >. )
50 2oex 
 |-  2o e. _V
51 opex 
 |-  <. i , ( 1st ` u ) >. e. _V
52 50 51 opth 
 |-  ( <. 2o , <. i , ( 1st ` u ) >. >. = <. 1o , <. ( 1st ` s ) , ( 1st ` r ) >. >. <-> ( 2o = 1o /\ <. i , ( 1st ` u ) >. = <. ( 1st ` s ) , ( 1st ` r ) >. ) )
53 1one2o 
 |-  1o =/= 2o
54 df-ne 
 |-  ( 1o =/= 2o <-> -. 1o = 2o )
55 pm2.21 
 |-  ( -. 1o = 2o -> ( 1o = 2o -> ( y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) -> y = z ) ) )
56 54 55 sylbi 
 |-  ( 1o =/= 2o -> ( 1o = 2o -> ( y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) -> y = z ) ) )
57 53 56 ax-mp 
 |-  ( 1o = 2o -> ( y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) -> y = z ) )
58 57 eqcoms 
 |-  ( 2o = 1o -> ( y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) -> y = z ) )
59 58 adantr 
 |-  ( ( 2o = 1o /\ <. i , ( 1st ` u ) >. = <. ( 1st ` s ) , ( 1st ` r ) >. ) -> ( y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) -> y = z ) )
60 52 59 sylbi 
 |-  ( <. 2o , <. i , ( 1st ` u ) >. >. = <. 1o , <. ( 1st ` s ) , ( 1st ` r ) >. >. -> ( y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) -> y = z ) )
61 49 60 sylbi 
 |-  ( A.g i ( 1st ` u ) = ( ( 1st ` s ) |g ( 1st ` r ) ) -> ( y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) -> y = z ) )
62 43 61 biimtrdi 
 |-  ( x = A.g i ( 1st ` u ) -> ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) -> ( y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) -> y = z ) ) )
63 62 impd 
 |-  ( x = A.g i ( 1st ` u ) -> ( ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) -> y = z ) )
64 63 adantr 
 |-  ( ( x = A.g i ( 1st ` u ) /\ z = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) -> ( ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) -> y = z ) )
65 64 a1i 
 |-  ( ( ( ( ( Fun ( ( M Sat E ) ` N ) /\ s e. ( ( M Sat E ) ` N ) ) /\ r e. ( ( M Sat E ) ` N ) ) /\ u e. ( ( M Sat E ) ` N ) ) /\ i e. _om ) -> ( ( x = A.g i ( 1st ` u ) /\ z = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) -> ( ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) -> y = z ) ) )
66 65 rexlimdva 
 |-  ( ( ( ( Fun ( ( M Sat E ) ` N ) /\ s e. ( ( M Sat E ) ` N ) ) /\ r e. ( ( M Sat E ) ` N ) ) /\ u e. ( ( M Sat E ) ` N ) ) -> ( E. i e. _om ( x = A.g i ( 1st ` u ) /\ z = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) -> ( ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) -> y = z ) ) )
67 42 66 jaod 
 |-  ( ( ( ( Fun ( ( M Sat E ) ` N ) /\ s e. ( ( M Sat E ) ` N ) ) /\ r e. ( ( M Sat E ) ` N ) ) /\ u e. ( ( M Sat E ) ` N ) ) -> ( ( E. v e. ( ( M Sat E ) ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ z = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ z = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) -> ( ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) -> y = z ) ) )
68 67 rexlimdva 
 |-  ( ( ( Fun ( ( M Sat E ) ` N ) /\ s e. ( ( M Sat E ) ` N ) ) /\ r e. ( ( M Sat E ) ` N ) ) -> ( E. u e. ( ( M Sat E ) ` N ) ( E. v e. ( ( M Sat E ) ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ z = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ z = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) -> ( ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) -> y = z ) ) )
69 68 com23 
 |-  ( ( ( Fun ( ( M Sat E ) ` N ) /\ s e. ( ( M Sat E ) ` N ) ) /\ r e. ( ( M Sat E ) ` N ) ) -> ( ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) -> ( E. u e. ( ( M Sat E ) ` N ) ( E. v e. ( ( M Sat E ) ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ z = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ z = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) -> y = z ) ) )
70 69 rexlimdva 
 |-  ( ( Fun ( ( M Sat E ) ` N ) /\ s e. ( ( M Sat E ) ` N ) ) -> ( E. r e. ( ( M Sat E ) ` N ) ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) -> ( E. u e. ( ( M Sat E ) ` N ) ( E. v e. ( ( M Sat E ) ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ z = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ z = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) -> y = z ) ) )
71 eqeq1 
 |-  ( x = A.g j ( 1st ` s ) -> ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) <-> A.g j ( 1st ` s ) = ( ( 1st ` u ) |g ( 1st ` v ) ) ) )
72 df-goal 
 |-  A.g j ( 1st ` s ) = <. 2o , <. j , ( 1st ` s ) >. >.
73 fvex 
 |-  ( 1st ` u ) e. _V
74 fvex 
 |-  ( 1st ` v ) e. _V
75 gonafv 
 |-  ( ( ( 1st ` u ) e. _V /\ ( 1st ` v ) e. _V ) -> ( ( 1st ` u ) |g ( 1st ` v ) ) = <. 1o , <. ( 1st ` u ) , ( 1st ` v ) >. >. )
76 73 74 75 mp2an 
 |-  ( ( 1st ` u ) |g ( 1st ` v ) ) = <. 1o , <. ( 1st ` u ) , ( 1st ` v ) >. >.
77 72 76 eqeq12i 
 |-  ( A.g j ( 1st ` s ) = ( ( 1st ` u ) |g ( 1st ` v ) ) <-> <. 2o , <. j , ( 1st ` s ) >. >. = <. 1o , <. ( 1st ` u ) , ( 1st ` v ) >. >. )
78 opex 
 |-  <. j , ( 1st ` s ) >. e. _V
79 50 78 opth 
 |-  ( <. 2o , <. j , ( 1st ` s ) >. >. = <. 1o , <. ( 1st ` u ) , ( 1st ` v ) >. >. <-> ( 2o = 1o /\ <. j , ( 1st ` s ) >. = <. ( 1st ` u ) , ( 1st ` v ) >. ) )
80 pm2.21 
 |-  ( -. 1o = 2o -> ( 1o = 2o -> y = z ) )
81 54 80 sylbi 
 |-  ( 1o =/= 2o -> ( 1o = 2o -> y = z ) )
82 53 81 ax-mp 
 |-  ( 1o = 2o -> y = z )
83 82 eqcoms 
 |-  ( 2o = 1o -> y = z )
84 83 adantr 
 |-  ( ( 2o = 1o /\ <. j , ( 1st ` s ) >. = <. ( 1st ` u ) , ( 1st ` v ) >. ) -> y = z )
85 79 84 sylbi 
 |-  ( <. 2o , <. j , ( 1st ` s ) >. >. = <. 1o , <. ( 1st ` u ) , ( 1st ` v ) >. >. -> y = z )
86 77 85 sylbi 
 |-  ( A.g j ( 1st ` s ) = ( ( 1st ` u ) |g ( 1st ` v ) ) -> y = z )
87 71 86 biimtrdi 
 |-  ( x = A.g j ( 1st ` s ) -> ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) -> y = z ) )
88 87 adantr 
 |-  ( ( x = A.g j ( 1st ` s ) /\ y = { f e. ( M ^m _om ) | A. k e. M ( { <. j , k >. } u. ( f |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } ) -> ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) -> y = z ) )
89 88 com12 
 |-  ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) -> ( ( x = A.g j ( 1st ` s ) /\ y = { f e. ( M ^m _om ) | A. k e. M ( { <. j , k >. } u. ( f |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } ) -> y = z ) )
90 89 adantr 
 |-  ( ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ z = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) -> ( ( x = A.g j ( 1st ` s ) /\ y = { f e. ( M ^m _om ) | A. k e. M ( { <. j , k >. } u. ( f |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } ) -> y = z ) )
91 90 a1i 
 |-  ( ( ( ( ( Fun ( ( M Sat E ) ` N ) /\ s e. ( ( M Sat E ) ` N ) ) /\ j e. _om ) /\ u e. ( ( M Sat E ) ` N ) ) /\ v e. ( ( M Sat E ) ` N ) ) -> ( ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ z = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) -> ( ( x = A.g j ( 1st ` s ) /\ y = { f e. ( M ^m _om ) | A. k e. M ( { <. j , k >. } u. ( f |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } ) -> y = z ) ) )
92 91 rexlimdva 
 |-  ( ( ( ( Fun ( ( M Sat E ) ` N ) /\ s e. ( ( M Sat E ) ` N ) ) /\ j e. _om ) /\ u e. ( ( M Sat E ) ` N ) ) -> ( E. v e. ( ( M Sat E ) ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ z = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) -> ( ( x = A.g j ( 1st ` s ) /\ y = { f e. ( M ^m _om ) | A. k e. M ( { <. j , k >. } u. ( f |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } ) -> y = z ) ) )
93 eqeq1 
 |-  ( x = A.g i ( 1st ` u ) -> ( x = A.g j ( 1st ` s ) <-> A.g i ( 1st ` u ) = A.g j ( 1st ` s ) ) )
94 44 72 eqeq12i 
 |-  ( A.g i ( 1st ` u ) = A.g j ( 1st ` s ) <-> <. 2o , <. i , ( 1st ` u ) >. >. = <. 2o , <. j , ( 1st ` s ) >. >. )
95 50 51 opth 
 |-  ( <. 2o , <. i , ( 1st ` u ) >. >. = <. 2o , <. j , ( 1st ` s ) >. >. <-> ( 2o = 2o /\ <. i , ( 1st ` u ) >. = <. j , ( 1st ` s ) >. ) )
96 vex 
 |-  i e. _V
97 96 73 opth 
 |-  ( <. i , ( 1st ` u ) >. = <. j , ( 1st ` s ) >. <-> ( i = j /\ ( 1st ` u ) = ( 1st ` s ) ) )
98 97 anbi2i 
 |-  ( ( 2o = 2o /\ <. i , ( 1st ` u ) >. = <. j , ( 1st ` s ) >. ) <-> ( 2o = 2o /\ ( i = j /\ ( 1st ` u ) = ( 1st ` s ) ) ) )
99 94 95 98 3bitri 
 |-  ( A.g i ( 1st ` u ) = A.g j ( 1st ` s ) <-> ( 2o = 2o /\ ( i = j /\ ( 1st ` u ) = ( 1st ` s ) ) ) )
100 93 99 bitrdi 
 |-  ( x = A.g i ( 1st ` u ) -> ( x = A.g j ( 1st ` s ) <-> ( 2o = 2o /\ ( i = j /\ ( 1st ` u ) = ( 1st ` s ) ) ) ) )
101 100 adantl 
 |-  ( ( ( ( ( ( Fun ( ( M Sat E ) ` N ) /\ s e. ( ( M Sat E ) ` N ) ) /\ j e. _om ) /\ u e. ( ( M Sat E ) ` N ) ) /\ i e. _om ) /\ x = A.g i ( 1st ` u ) ) -> ( x = A.g j ( 1st ` s ) <-> ( 2o = 2o /\ ( i = j /\ ( 1st ` u ) = ( 1st ` s ) ) ) ) )
102 funfv1st2nd 
 |-  ( ( Fun ( ( M Sat E ) ` N ) /\ s e. ( ( M Sat E ) ` N ) ) -> ( ( ( M Sat E ) ` N ) ` ( 1st ` s ) ) = ( 2nd ` s ) )
103 102 ex 
 |-  ( Fun ( ( M Sat E ) ` N ) -> ( s e. ( ( M Sat E ) ` N ) -> ( ( ( M Sat E ) ` N ) ` ( 1st ` s ) ) = ( 2nd ` s ) ) )
104 funfv1st2nd 
 |-  ( ( Fun ( ( M Sat E ) ` N ) /\ u e. ( ( M Sat E ) ` N ) ) -> ( ( ( M Sat E ) ` N ) ` ( 1st ` u ) ) = ( 2nd ` u ) )
105 104 ex 
 |-  ( Fun ( ( M Sat E ) ` N ) -> ( u e. ( ( M Sat E ) ` N ) -> ( ( ( M Sat E ) ` N ) ` ( 1st ` u ) ) = ( 2nd ` u ) ) )
106 fveqeq2 
 |-  ( ( 1st ` u ) = ( 1st ` s ) -> ( ( ( ( M Sat E ) ` N ) ` ( 1st ` u ) ) = ( 2nd ` u ) <-> ( ( ( M Sat E ) ` N ) ` ( 1st ` s ) ) = ( 2nd ` u ) ) )
107 eqtr2 
 |-  ( ( ( ( ( M Sat E ) ` N ) ` ( 1st ` s ) ) = ( 2nd ` u ) /\ ( ( ( M Sat E ) ` N ) ` ( 1st ` s ) ) = ( 2nd ` s ) ) -> ( 2nd ` u ) = ( 2nd ` s ) )
108 opeq1 
 |-  ( j = i -> <. j , k >. = <. i , k >. )
109 108 sneqd 
 |-  ( j = i -> { <. j , k >. } = { <. i , k >. } )
110 sneq 
 |-  ( j = i -> { j } = { i } )
111 110 difeq2d 
 |-  ( j = i -> ( _om \ { j } ) = ( _om \ { i } ) )
112 111 reseq2d 
 |-  ( j = i -> ( f |` ( _om \ { j } ) ) = ( f |` ( _om \ { i } ) ) )
113 109 112 uneq12d 
 |-  ( j = i -> ( { <. j , k >. } u. ( f |` ( _om \ { j } ) ) ) = ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) )
114 113 eqcoms 
 |-  ( i = j -> ( { <. j , k >. } u. ( f |` ( _om \ { j } ) ) ) = ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) )
115 114 adantl 
 |-  ( ( ( 2nd ` u ) = ( 2nd ` s ) /\ i = j ) -> ( { <. j , k >. } u. ( f |` ( _om \ { j } ) ) ) = ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) )
116 simpl 
 |-  ( ( ( 2nd ` u ) = ( 2nd ` s ) /\ i = j ) -> ( 2nd ` u ) = ( 2nd ` s ) )
117 116 eqcomd 
 |-  ( ( ( 2nd ` u ) = ( 2nd ` s ) /\ i = j ) -> ( 2nd ` s ) = ( 2nd ` u ) )
118 115 117 eleq12d 
 |-  ( ( ( 2nd ` u ) = ( 2nd ` s ) /\ i = j ) -> ( ( { <. j , k >. } u. ( f |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) <-> ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) ) )
119 118 ralbidv 
 |-  ( ( ( 2nd ` u ) = ( 2nd ` s ) /\ i = j ) -> ( A. k e. M ( { <. j , k >. } u. ( f |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) <-> A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) ) )
120 119 rabbidv 
 |-  ( ( ( 2nd ` u ) = ( 2nd ` s ) /\ i = j ) -> { f e. ( M ^m _om ) | A. k e. M ( { <. j , k >. } u. ( f |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } )
121 eqeq12 
 |-  ( ( y = { f e. ( M ^m _om ) | A. k e. M ( { <. j , k >. } u. ( f |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } /\ z = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) -> ( y = z <-> { f e. ( M ^m _om ) | A. k e. M ( { <. j , k >. } u. ( f |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) )
122 120 121 syl5ibrcom 
 |-  ( ( ( 2nd ` u ) = ( 2nd ` s ) /\ i = j ) -> ( ( y = { f e. ( M ^m _om ) | A. k e. M ( { <. j , k >. } u. ( f |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } /\ z = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) -> y = z ) )
123 122 exp4b 
 |-  ( ( 2nd ` u ) = ( 2nd ` s ) -> ( i = j -> ( y = { f e. ( M ^m _om ) | A. k e. M ( { <. j , k >. } u. ( f |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } -> ( z = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } -> y = z ) ) ) )
124 107 123 syl 
 |-  ( ( ( ( ( M Sat E ) ` N ) ` ( 1st ` s ) ) = ( 2nd ` u ) /\ ( ( ( M Sat E ) ` N ) ` ( 1st ` s ) ) = ( 2nd ` s ) ) -> ( i = j -> ( y = { f e. ( M ^m _om ) | A. k e. M ( { <. j , k >. } u. ( f |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } -> ( z = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } -> y = z ) ) ) )
125 124 ex 
 |-  ( ( ( ( M Sat E ) ` N ) ` ( 1st ` s ) ) = ( 2nd ` u ) -> ( ( ( ( M Sat E ) ` N ) ` ( 1st ` s ) ) = ( 2nd ` s ) -> ( i = j -> ( y = { f e. ( M ^m _om ) | A. k e. M ( { <. j , k >. } u. ( f |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } -> ( z = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } -> y = z ) ) ) ) )
126 106 125 biimtrdi 
 |-  ( ( 1st ` u ) = ( 1st ` s ) -> ( ( ( ( M Sat E ) ` N ) ` ( 1st ` u ) ) = ( 2nd ` u ) -> ( ( ( ( M Sat E ) ` N ) ` ( 1st ` s ) ) = ( 2nd ` s ) -> ( i = j -> ( y = { f e. ( M ^m _om ) | A. k e. M ( { <. j , k >. } u. ( f |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } -> ( z = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } -> y = z ) ) ) ) ) )
127 126 com24 
 |-  ( ( 1st ` u ) = ( 1st ` s ) -> ( i = j -> ( ( ( ( M Sat E ) ` N ) ` ( 1st ` s ) ) = ( 2nd ` s ) -> ( ( ( ( M Sat E ) ` N ) ` ( 1st ` u ) ) = ( 2nd ` u ) -> ( y = { f e. ( M ^m _om ) | A. k e. M ( { <. j , k >. } u. ( f |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } -> ( z = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } -> y = z ) ) ) ) ) )
128 127 impcom 
 |-  ( ( i = j /\ ( 1st ` u ) = ( 1st ` s ) ) -> ( ( ( ( M Sat E ) ` N ) ` ( 1st ` s ) ) = ( 2nd ` s ) -> ( ( ( ( M Sat E ) ` N ) ` ( 1st ` u ) ) = ( 2nd ` u ) -> ( y = { f e. ( M ^m _om ) | A. k e. M ( { <. j , k >. } u. ( f |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } -> ( z = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } -> y = z ) ) ) ) )
129 128 com13 
 |-  ( ( ( ( M Sat E ) ` N ) ` ( 1st ` u ) ) = ( 2nd ` u ) -> ( ( ( ( M Sat E ) ` N ) ` ( 1st ` s ) ) = ( 2nd ` s ) -> ( ( i = j /\ ( 1st ` u ) = ( 1st ` s ) ) -> ( y = { f e. ( M ^m _om ) | A. k e. M ( { <. j , k >. } u. ( f |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } -> ( z = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } -> y = z ) ) ) ) )
130 105 129 syl6 
 |-  ( Fun ( ( M Sat E ) ` N ) -> ( u e. ( ( M Sat E ) ` N ) -> ( ( ( ( M Sat E ) ` N ) ` ( 1st ` s ) ) = ( 2nd ` s ) -> ( ( i = j /\ ( 1st ` u ) = ( 1st ` s ) ) -> ( y = { f e. ( M ^m _om ) | A. k e. M ( { <. j , k >. } u. ( f |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } -> ( z = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } -> y = z ) ) ) ) ) )
131 130 com23 
 |-  ( Fun ( ( M Sat E ) ` N ) -> ( ( ( ( M Sat E ) ` N ) ` ( 1st ` s ) ) = ( 2nd ` s ) -> ( u e. ( ( M Sat E ) ` N ) -> ( ( i = j /\ ( 1st ` u ) = ( 1st ` s ) ) -> ( y = { f e. ( M ^m _om ) | A. k e. M ( { <. j , k >. } u. ( f |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } -> ( z = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } -> y = z ) ) ) ) ) )
132 103 131 syld 
 |-  ( Fun ( ( M Sat E ) ` N ) -> ( s e. ( ( M Sat E ) ` N ) -> ( u e. ( ( M Sat E ) ` N ) -> ( ( i = j /\ ( 1st ` u ) = ( 1st ` s ) ) -> ( y = { f e. ( M ^m _om ) | A. k e. M ( { <. j , k >. } u. ( f |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } -> ( z = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } -> y = z ) ) ) ) ) )
133 132 imp 
 |-  ( ( Fun ( ( M Sat E ) ` N ) /\ s e. ( ( M Sat E ) ` N ) ) -> ( u e. ( ( M Sat E ) ` N ) -> ( ( i = j /\ ( 1st ` u ) = ( 1st ` s ) ) -> ( y = { f e. ( M ^m _om ) | A. k e. M ( { <. j , k >. } u. ( f |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } -> ( z = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } -> y = z ) ) ) ) )
134 133 adantr 
 |-  ( ( ( Fun ( ( M Sat E ) ` N ) /\ s e. ( ( M Sat E ) ` N ) ) /\ j e. _om ) -> ( u e. ( ( M Sat E ) ` N ) -> ( ( i = j /\ ( 1st ` u ) = ( 1st ` s ) ) -> ( y = { f e. ( M ^m _om ) | A. k e. M ( { <. j , k >. } u. ( f |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } -> ( z = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } -> y = z ) ) ) ) )
135 134 imp 
 |-  ( ( ( ( Fun ( ( M Sat E ) ` N ) /\ s e. ( ( M Sat E ) ` N ) ) /\ j e. _om ) /\ u e. ( ( M Sat E ) ` N ) ) -> ( ( i = j /\ ( 1st ` u ) = ( 1st ` s ) ) -> ( y = { f e. ( M ^m _om ) | A. k e. M ( { <. j , k >. } u. ( f |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } -> ( z = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } -> y = z ) ) ) )
136 135 adantld 
 |-  ( ( ( ( Fun ( ( M Sat E ) ` N ) /\ s e. ( ( M Sat E ) ` N ) ) /\ j e. _om ) /\ u e. ( ( M Sat E ) ` N ) ) -> ( ( 2o = 2o /\ ( i = j /\ ( 1st ` u ) = ( 1st ` s ) ) ) -> ( y = { f e. ( M ^m _om ) | A. k e. M ( { <. j , k >. } u. ( f |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } -> ( z = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } -> y = z ) ) ) )
137 136 ad2antrr 
 |-  ( ( ( ( ( ( Fun ( ( M Sat E ) ` N ) /\ s e. ( ( M Sat E ) ` N ) ) /\ j e. _om ) /\ u e. ( ( M Sat E ) ` N ) ) /\ i e. _om ) /\ x = A.g i ( 1st ` u ) ) -> ( ( 2o = 2o /\ ( i = j /\ ( 1st ` u ) = ( 1st ` s ) ) ) -> ( y = { f e. ( M ^m _om ) | A. k e. M ( { <. j , k >. } u. ( f |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } -> ( z = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } -> y = z ) ) ) )
138 101 137 sylbid 
 |-  ( ( ( ( ( ( Fun ( ( M Sat E ) ` N ) /\ s e. ( ( M Sat E ) ` N ) ) /\ j e. _om ) /\ u e. ( ( M Sat E ) ` N ) ) /\ i e. _om ) /\ x = A.g i ( 1st ` u ) ) -> ( x = A.g j ( 1st ` s ) -> ( y = { f e. ( M ^m _om ) | A. k e. M ( { <. j , k >. } u. ( f |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } -> ( z = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } -> y = z ) ) ) )
139 138 impd 
 |-  ( ( ( ( ( ( Fun ( ( M Sat E ) ` N ) /\ s e. ( ( M Sat E ) ` N ) ) /\ j e. _om ) /\ u e. ( ( M Sat E ) ` N ) ) /\ i e. _om ) /\ x = A.g i ( 1st ` u ) ) -> ( ( x = A.g j ( 1st ` s ) /\ y = { f e. ( M ^m _om ) | A. k e. M ( { <. j , k >. } u. ( f |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } ) -> ( z = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } -> y = z ) ) )
140 139 ex 
 |-  ( ( ( ( ( Fun ( ( M Sat E ) ` N ) /\ s e. ( ( M Sat E ) ` N ) ) /\ j e. _om ) /\ u e. ( ( M Sat E ) ` N ) ) /\ i e. _om ) -> ( x = A.g i ( 1st ` u ) -> ( ( x = A.g j ( 1st ` s ) /\ y = { f e. ( M ^m _om ) | A. k e. M ( { <. j , k >. } u. ( f |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } ) -> ( z = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } -> y = z ) ) ) )
141 140 com34 
 |-  ( ( ( ( ( Fun ( ( M Sat E ) ` N ) /\ s e. ( ( M Sat E ) ` N ) ) /\ j e. _om ) /\ u e. ( ( M Sat E ) ` N ) ) /\ i e. _om ) -> ( x = A.g i ( 1st ` u ) -> ( z = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } -> ( ( x = A.g j ( 1st ` s ) /\ y = { f e. ( M ^m _om ) | A. k e. M ( { <. j , k >. } u. ( f |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } ) -> y = z ) ) ) )
142 141 impd 
 |-  ( ( ( ( ( Fun ( ( M Sat E ) ` N ) /\ s e. ( ( M Sat E ) ` N ) ) /\ j e. _om ) /\ u e. ( ( M Sat E ) ` N ) ) /\ i e. _om ) -> ( ( x = A.g i ( 1st ` u ) /\ z = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) -> ( ( x = A.g j ( 1st ` s ) /\ y = { f e. ( M ^m _om ) | A. k e. M ( { <. j , k >. } u. ( f |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } ) -> y = z ) ) )
143 142 rexlimdva 
 |-  ( ( ( ( Fun ( ( M Sat E ) ` N ) /\ s e. ( ( M Sat E ) ` N ) ) /\ j e. _om ) /\ u e. ( ( M Sat E ) ` N ) ) -> ( E. i e. _om ( x = A.g i ( 1st ` u ) /\ z = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) -> ( ( x = A.g j ( 1st ` s ) /\ y = { f e. ( M ^m _om ) | A. k e. M ( { <. j , k >. } u. ( f |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } ) -> y = z ) ) )
144 92 143 jaod 
 |-  ( ( ( ( Fun ( ( M Sat E ) ` N ) /\ s e. ( ( M Sat E ) ` N ) ) /\ j e. _om ) /\ u e. ( ( M Sat E ) ` N ) ) -> ( ( E. v e. ( ( M Sat E ) ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ z = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ z = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) -> ( ( x = A.g j ( 1st ` s ) /\ y = { f e. ( M ^m _om ) | A. k e. M ( { <. j , k >. } u. ( f |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } ) -> y = z ) ) )
145 144 rexlimdva 
 |-  ( ( ( Fun ( ( M Sat E ) ` N ) /\ s e. ( ( M Sat E ) ` N ) ) /\ j e. _om ) -> ( E. u e. ( ( M Sat E ) ` N ) ( E. v e. ( ( M Sat E ) ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ z = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ z = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) -> ( ( x = A.g j ( 1st ` s ) /\ y = { f e. ( M ^m _om ) | A. k e. M ( { <. j , k >. } u. ( f |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } ) -> y = z ) ) )
146 145 com23 
 |-  ( ( ( Fun ( ( M Sat E ) ` N ) /\ s e. ( ( M Sat E ) ` N ) ) /\ j e. _om ) -> ( ( x = A.g j ( 1st ` s ) /\ y = { f e. ( M ^m _om ) | A. k e. M ( { <. j , k >. } u. ( f |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } ) -> ( E. u e. ( ( M Sat E ) ` N ) ( E. v e. ( ( M Sat E ) ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ z = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ z = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) -> y = z ) ) )
147 146 rexlimdva 
 |-  ( ( Fun ( ( M Sat E ) ` N ) /\ s e. ( ( M Sat E ) ` N ) ) -> ( E. j e. _om ( x = A.g j ( 1st ` s ) /\ y = { f e. ( M ^m _om ) | A. k e. M ( { <. j , k >. } u. ( f |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } ) -> ( E. u e. ( ( M Sat E ) ` N ) ( E. v e. ( ( M Sat E ) ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ z = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ z = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) -> y = z ) ) )
148 70 147 jaod 
 |-  ( ( Fun ( ( M Sat E ) ` N ) /\ s e. ( ( M Sat E ) ` N ) ) -> ( ( E. r e. ( ( M Sat E ) ` 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 = { f e. ( M ^m _om ) | A. k e. M ( { <. j , k >. } u. ( f |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } ) ) -> ( E. u e. ( ( M Sat E ) ` N ) ( E. v e. ( ( M Sat E ) ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ z = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ z = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) -> y = z ) ) )
149 148 rexlimdva 
 |-  ( Fun ( ( M Sat E ) ` N ) -> ( E. s e. ( ( M Sat E ) ` N ) ( E. r e. ( ( M Sat E ) ` 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 = { f e. ( M ^m _om ) | A. k e. M ( { <. j , k >. } u. ( f |` ( _om \ { j } ) ) ) e. ( 2nd ` s ) } ) ) -> ( E. u e. ( ( M Sat E ) ` N ) ( E. v e. ( ( M Sat E ) ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ z = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ z = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) -> y = z ) ) )
150 31 149 biimtrid 
 |-  ( Fun ( ( M Sat E ) ` N ) -> ( E. u e. ( ( M Sat E ) ` N ) ( E. v e. ( ( M Sat E ) ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) -> ( E. u e. ( ( M Sat E ) ` N ) ( E. v e. ( ( M Sat E ) ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ z = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ z = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) -> y = z ) ) )
151 150 impd 
 |-  ( Fun ( ( M Sat E ) ` N ) -> ( ( E. u e. ( ( M Sat E ) ` N ) ( E. v e. ( ( M Sat E ) ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) /\ E. u e. ( ( M Sat E ) ` N ) ( E. v e. ( ( M Sat E ) ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ z = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ z = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) ) -> y = z ) )
152 151 alrimivv 
 |-  ( Fun ( ( M Sat E ) ` N ) -> A. y A. z ( ( E. u e. ( ( M Sat E ) ` N ) ( E. v e. ( ( M Sat E ) ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) /\ E. u e. ( ( M Sat E ) ` N ) ( E. v e. ( ( M Sat E ) ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ z = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ z = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) ) -> y = z ) )
153 eqeq1 
 |-  ( y = z -> ( y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) <-> z = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) )
154 153 anbi2d 
 |-  ( y = z -> ( ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) <-> ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ z = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) ) )
155 154 rexbidv 
 |-  ( y = z -> ( E. v e. ( ( M Sat E ) ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) <-> E. v e. ( ( M Sat E ) ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ z = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) ) )
156 eqeq1 
 |-  ( y = z -> ( y = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } <-> z = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) )
157 156 anbi2d 
 |-  ( y = z -> ( ( x = A.g i ( 1st ` u ) /\ y = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) <-> ( x = A.g i ( 1st ` u ) /\ z = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) )
158 157 rexbidv 
 |-  ( y = z -> ( E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) <-> E. i e. _om ( x = A.g i ( 1st ` u ) /\ z = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) )
159 155 158 orbi12d 
 |-  ( y = z -> ( ( E. v e. ( ( M Sat E ) ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) <-> ( E. v e. ( ( M Sat E ) ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ z = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ z = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) ) )
160 159 rexbidv 
 |-  ( y = z -> ( E. u e. ( ( M Sat E ) ` N ) ( E. v e. ( ( M Sat E ) ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) <-> E. u e. ( ( M Sat E ) ` N ) ( E. v e. ( ( M Sat E ) ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ z = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ z = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) ) )
161 160 mo4 
 |-  ( E* y E. u e. ( ( M Sat E ) ` N ) ( E. v e. ( ( M Sat E ) ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) <-> A. y A. z ( ( E. u e. ( ( M Sat E ) ` N ) ( E. v e. ( ( M Sat E ) ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) /\ E. u e. ( ( M Sat E ) ` N ) ( E. v e. ( ( M Sat E ) ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ z = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ z = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) ) -> y = z ) )
162 152 161 sylibr 
 |-  ( Fun ( ( M Sat E ) ` N ) -> E* y E. u e. ( ( M Sat E ) ` N ) ( E. v e. ( ( M Sat E ) ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) )
163 162 alrimiv 
 |-  ( Fun ( ( M Sat E ) ` N ) -> A. x E* y E. u e. ( ( M Sat E ) ` N ) ( E. v e. ( ( M Sat E ) ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) )
164 funopab 
 |-  ( Fun { <. x , y >. | E. u e. ( ( M Sat E ) ` N ) ( E. v e. ( ( M Sat E ) ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } <-> A. x E* y E. u e. ( ( M Sat E ) ` N ) ( E. v e. ( ( M Sat E ) ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) )
165 163 164 sylibr 
 |-  ( Fun ( ( M Sat E ) ` N ) -> Fun { <. x , y >. | E. u e. ( ( M Sat E ) ` N ) ( E. v e. ( ( M Sat E ) ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { f e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } )