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