Metamath Proof Explorer

Theorem satfv1

Description: The value of the satisfaction predicate as function over wff codes of height 1. (Contributed by AV, 9-Nov-2023)

Ref Expression
Hypothesis satfv1.s 
|- S = ( M Sat E )
Assertion satfv1 
|- ( ( M e. V /\ E e. W ) -> ( S ` 1o ) = ( ( S ` (/) ) u. { <. x , y >. | E. i e. _om E. j e. _om ( E. k e. _om E. l e. _om ( x = ( ( i e.g j ) |g ( k e.g l ) ) /\ y = { a e. ( M ^m _om ) | ( -. ( a ` i ) E ( a ` j ) \/ -. ( a ` k ) E ( a ` l ) ) } ) \/ E. n e. _om ( x = A.g n ( i e.g j ) /\ y = { a e. ( M ^m _om ) | A. z e. M if- ( i = n , if- ( j = n , z E z , z E ( a ` j ) ) , if- ( j = n , ( a ` i ) E z , ( a ` i ) E ( a ` j ) ) ) } ) ) } ) )

Proof

Step Hyp Ref Expression
1 satfv1.s 
 |-  S = ( M Sat E )
2 df-1o 
 |-  1o = suc (/)
3 2 fveq2i 
 |-  ( S ` 1o ) = ( S ` suc (/) )
4 3 a1i 
 |-  ( ( M e. V /\ E e. W ) -> ( S ` 1o ) = ( S ` suc (/) ) )
5 peano1 
 |-  (/) e. _om
6 1 satfvsuc 
 |-  ( ( M e. V /\ E e. W /\ (/) e. _om ) -> ( S ` suc (/) ) = ( ( S ` (/) ) u. { <. x , y >. | E. o e. ( S ` (/) ) ( E. p e. ( S ` (/) ) ( x = ( ( 1st ` o ) |g ( 1st ` p ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` o ) i^i ( 2nd ` p ) ) ) ) \/ E. n e. _om ( x = A.g n ( 1st ` o ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. ( 2nd ` o ) } ) ) } ) )
7 5 6 mp3an3 
 |-  ( ( M e. V /\ E e. W ) -> ( S ` suc (/) ) = ( ( S ` (/) ) u. { <. x , y >. | E. o e. ( S ` (/) ) ( E. p e. ( S ` (/) ) ( x = ( ( 1st ` o ) |g ( 1st ` p ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` o ) i^i ( 2nd ` p ) ) ) ) \/ E. n e. _om ( x = A.g n ( 1st ` o ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. ( 2nd ` o ) } ) ) } ) )
8 1 satfv0 
 |-  ( ( M e. V /\ E e. W ) -> ( S ` (/) ) = { <. e , b >. | E. i e. _om E. j e. _om ( e = ( i e.g j ) /\ b = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) } )
9 8 rexeqdv 
 |-  ( ( M e. V /\ E e. W ) -> ( E. o e. ( S ` (/) ) ( E. p e. ( S ` (/) ) ( x = ( ( 1st ` o ) |g ( 1st ` p ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` o ) i^i ( 2nd ` p ) ) ) ) \/ E. n e. _om ( x = A.g n ( 1st ` o ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. ( 2nd ` o ) } ) ) <-> E. o e. { <. e , b >. | E. i e. _om E. j e. _om ( e = ( i e.g j ) /\ b = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) } ( E. p e. ( S ` (/) ) ( x = ( ( 1st ` o ) |g ( 1st ` p ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` o ) i^i ( 2nd ` p ) ) ) ) \/ E. n e. _om ( x = A.g n ( 1st ` o ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. ( 2nd ` o ) } ) ) ) )
10 eqid 
 |-  { <. e , b >. | E. i e. _om E. j e. _om ( e = ( i e.g j ) /\ b = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) } = { <. e , b >. | E. i e. _om E. j e. _om ( e = ( i e.g j ) /\ b = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) }
11 vex 
 |-  e e. _V
12 vex 
 |-  b e. _V
13 11 12 op1std 
 |-  ( o = <. e , b >. -> ( 1st ` o ) = e )
14 13 oveq1d 
 |-  ( o = <. e , b >. -> ( ( 1st ` o ) |g ( 1st ` p ) ) = ( e |g ( 1st ` p ) ) )
15 14 eqeq2d 
 |-  ( o = <. e , b >. -> ( x = ( ( 1st ` o ) |g ( 1st ` p ) ) <-> x = ( e |g ( 1st ` p ) ) ) )
16 11 12 op2ndd 
 |-  ( o = <. e , b >. -> ( 2nd ` o ) = b )
17 16 ineq1d 
 |-  ( o = <. e , b >. -> ( ( 2nd ` o ) i^i ( 2nd ` p ) ) = ( b i^i ( 2nd ` p ) ) )
18 17 difeq2d 
 |-  ( o = <. e , b >. -> ( ( M ^m _om ) \ ( ( 2nd ` o ) i^i ( 2nd ` p ) ) ) = ( ( M ^m _om ) \ ( b i^i ( 2nd ` p ) ) ) )
19 18 eqeq2d 
 |-  ( o = <. e , b >. -> ( y = ( ( M ^m _om ) \ ( ( 2nd ` o ) i^i ( 2nd ` p ) ) ) <-> y = ( ( M ^m _om ) \ ( b i^i ( 2nd ` p ) ) ) ) )
20 15 19 anbi12d 
 |-  ( o = <. e , b >. -> ( ( x = ( ( 1st ` o ) |g ( 1st ` p ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` o ) i^i ( 2nd ` p ) ) ) ) <-> ( x = ( e |g ( 1st ` p ) ) /\ y = ( ( M ^m _om ) \ ( b i^i ( 2nd ` p ) ) ) ) ) )
21 20 rexbidv 
 |-  ( o = <. e , b >. -> ( E. p e. ( S ` (/) ) ( x = ( ( 1st ` o ) |g ( 1st ` p ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` o ) i^i ( 2nd ` p ) ) ) ) <-> E. p e. ( S ` (/) ) ( x = ( e |g ( 1st ` p ) ) /\ y = ( ( M ^m _om ) \ ( b i^i ( 2nd ` p ) ) ) ) ) )
22 eqidd 
 |-  ( o = <. e , b >. -> n = n )
23 22 13 goaleq12d 
 |-  ( o = <. e , b >. -> A.g n ( 1st ` o ) = A.g n e )
24 23 eqeq2d 
 |-  ( o = <. e , b >. -> ( x = A.g n ( 1st ` o ) <-> x = A.g n e ) )
25 16 eleq2d 
 |-  ( o = <. e , b >. -> ( ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. ( 2nd ` o ) <-> ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. b ) )
26 25 ralbidv 
 |-  ( o = <. e , b >. -> ( A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. ( 2nd ` o ) <-> A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. b ) )
27 26 rabbidv 
 |-  ( o = <. e , b >. -> { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. ( 2nd ` o ) } = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. b } )
28 27 eqeq2d 
 |-  ( o = <. e , b >. -> ( y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. ( 2nd ` o ) } <-> y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. b } ) )
29 24 28 anbi12d 
 |-  ( o = <. e , b >. -> ( ( x = A.g n ( 1st ` o ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. ( 2nd ` o ) } ) <-> ( x = A.g n e /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. b } ) ) )
30 29 rexbidv 
 |-  ( o = <. e , b >. -> ( E. n e. _om ( x = A.g n ( 1st ` o ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. ( 2nd ` o ) } ) <-> E. n e. _om ( x = A.g n e /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. b } ) ) )
31 21 30 orbi12d 
 |-  ( o = <. e , b >. -> ( ( E. p e. ( S ` (/) ) ( x = ( ( 1st ` o ) |g ( 1st ` p ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` o ) i^i ( 2nd ` p ) ) ) ) \/ E. n e. _om ( x = A.g n ( 1st ` o ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. ( 2nd ` o ) } ) ) <-> ( E. p e. ( S ` (/) ) ( x = ( e |g ( 1st ` p ) ) /\ y = ( ( M ^m _om ) \ ( b i^i ( 2nd ` p ) ) ) ) \/ E. n e. _om ( x = A.g n e /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. b } ) ) ) )
32 10 31 rexopabb 
 |-  ( E. o e. { <. e , b >. | E. i e. _om E. j e. _om ( e = ( i e.g j ) /\ b = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) } ( E. p e. ( S ` (/) ) ( x = ( ( 1st ` o ) |g ( 1st ` p ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` o ) i^i ( 2nd ` p ) ) ) ) \/ E. n e. _om ( x = A.g n ( 1st ` o ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. ( 2nd ` o ) } ) ) <-> E. e E. b ( E. i e. _om E. j e. _om ( e = ( i e.g j ) /\ b = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) /\ ( E. p e. ( S ` (/) ) ( x = ( e |g ( 1st ` p ) ) /\ y = ( ( M ^m _om ) \ ( b i^i ( 2nd ` p ) ) ) ) \/ E. n e. _om ( x = A.g n e /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. b } ) ) ) )
33 9 32 bitrdi 
 |-  ( ( M e. V /\ E e. W ) -> ( E. o e. ( S ` (/) ) ( E. p e. ( S ` (/) ) ( x = ( ( 1st ` o ) |g ( 1st ` p ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` o ) i^i ( 2nd ` p ) ) ) ) \/ E. n e. _om ( x = A.g n ( 1st ` o ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. ( 2nd ` o ) } ) ) <-> E. e E. b ( E. i e. _om E. j e. _om ( e = ( i e.g j ) /\ b = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) /\ ( E. p e. ( S ` (/) ) ( x = ( e |g ( 1st ` p ) ) /\ y = ( ( M ^m _om ) \ ( b i^i ( 2nd ` p ) ) ) ) \/ E. n e. _om ( x = A.g n e /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. b } ) ) ) ) )
34 1 satfv0 
 |-  ( ( M e. V /\ E e. W ) -> ( S ` (/) ) = { <. c , d >. | E. k e. _om E. l e. _om ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) } )
35 34 rexeqdv 
 |-  ( ( M e. V /\ E e. W ) -> ( E. p e. ( S ` (/) ) ( x = ( e |g ( 1st ` p ) ) /\ y = ( ( M ^m _om ) \ ( b i^i ( 2nd ` p ) ) ) ) <-> E. p e. { <. c , d >. | E. k e. _om E. l e. _om ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) } ( x = ( e |g ( 1st ` p ) ) /\ y = ( ( M ^m _om ) \ ( b i^i ( 2nd ` p ) ) ) ) ) )
36 eqid 
 |-  { <. c , d >. | E. k e. _om E. l e. _om ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) } = { <. c , d >. | E. k e. _om E. l e. _om ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) }
37 vex 
 |-  c e. _V
38 vex 
 |-  d e. _V
39 37 38 op1std 
 |-  ( p = <. c , d >. -> ( 1st ` p ) = c )
40 39 oveq2d 
 |-  ( p = <. c , d >. -> ( e |g ( 1st ` p ) ) = ( e |g c ) )
41 40 eqeq2d 
 |-  ( p = <. c , d >. -> ( x = ( e |g ( 1st ` p ) ) <-> x = ( e |g c ) ) )
42 37 38 op2ndd 
 |-  ( p = <. c , d >. -> ( 2nd ` p ) = d )
43 42 ineq2d 
 |-  ( p = <. c , d >. -> ( b i^i ( 2nd ` p ) ) = ( b i^i d ) )
44 43 difeq2d 
 |-  ( p = <. c , d >. -> ( ( M ^m _om ) \ ( b i^i ( 2nd ` p ) ) ) = ( ( M ^m _om ) \ ( b i^i d ) ) )
45 44 eqeq2d 
 |-  ( p = <. c , d >. -> ( y = ( ( M ^m _om ) \ ( b i^i ( 2nd ` p ) ) ) <-> y = ( ( M ^m _om ) \ ( b i^i d ) ) ) )
46 41 45 anbi12d 
 |-  ( p = <. c , d >. -> ( ( x = ( e |g ( 1st ` p ) ) /\ y = ( ( M ^m _om ) \ ( b i^i ( 2nd ` p ) ) ) ) <-> ( x = ( e |g c ) /\ y = ( ( M ^m _om ) \ ( b i^i d ) ) ) ) )
47 36 46 rexopabb 
 |-  ( E. p e. { <. c , d >. | E. k e. _om E. l e. _om ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) } ( x = ( e |g ( 1st ` p ) ) /\ y = ( ( M ^m _om ) \ ( b i^i ( 2nd ` p ) ) ) ) <-> E. c E. d ( E. k e. _om E. l e. _om ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( e |g c ) /\ y = ( ( M ^m _om ) \ ( b i^i d ) ) ) ) )
48 35 47 bitrdi 
 |-  ( ( M e. V /\ E e. W ) -> ( E. p e. ( S ` (/) ) ( x = ( e |g ( 1st ` p ) ) /\ y = ( ( M ^m _om ) \ ( b i^i ( 2nd ` p ) ) ) ) <-> E. c E. d ( E. k e. _om E. l e. _om ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( e |g c ) /\ y = ( ( M ^m _om ) \ ( b i^i d ) ) ) ) ) )
49 48 orbi1d 
 |-  ( ( M e. V /\ E e. W ) -> ( ( E. p e. ( S ` (/) ) ( x = ( e |g ( 1st ` p ) ) /\ y = ( ( M ^m _om ) \ ( b i^i ( 2nd ` p ) ) ) ) \/ E. n e. _om ( x = A.g n e /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. b } ) ) <-> ( E. c E. d ( E. k e. _om E. l e. _om ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( e |g c ) /\ y = ( ( M ^m _om ) \ ( b i^i d ) ) ) ) \/ E. n e. _om ( x = A.g n e /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. b } ) ) ) )
50 49 anbi2d 
 |-  ( ( M e. V /\ E e. W ) -> ( ( E. i e. _om E. j e. _om ( e = ( i e.g j ) /\ b = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) /\ ( E. p e. ( S ` (/) ) ( x = ( e |g ( 1st ` p ) ) /\ y = ( ( M ^m _om ) \ ( b i^i ( 2nd ` p ) ) ) ) \/ E. n e. _om ( x = A.g n e /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. b } ) ) ) <-> ( E. i e. _om E. j e. _om ( e = ( i e.g j ) /\ b = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) /\ ( E. c E. d ( E. k e. _om E. l e. _om ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( e |g c ) /\ y = ( ( M ^m _om ) \ ( b i^i d ) ) ) ) \/ E. n e. _om ( x = A.g n e /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. b } ) ) ) ) )
51 50 2exbidv 
 |-  ( ( M e. V /\ E e. W ) -> ( E. e E. b ( E. i e. _om E. j e. _om ( e = ( i e.g j ) /\ b = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) /\ ( E. p e. ( S ` (/) ) ( x = ( e |g ( 1st ` p ) ) /\ y = ( ( M ^m _om ) \ ( b i^i ( 2nd ` p ) ) ) ) \/ E. n e. _om ( x = A.g n e /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. b } ) ) ) <-> E. e E. b ( E. i e. _om E. j e. _om ( e = ( i e.g j ) /\ b = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) /\ ( E. c E. d ( E. k e. _om E. l e. _om ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( e |g c ) /\ y = ( ( M ^m _om ) \ ( b i^i d ) ) ) ) \/ E. n e. _om ( x = A.g n e /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. b } ) ) ) ) )
52 r19.41vv 
 |-  ( E. i e. _om E. j e. _om ( ( e = ( i e.g j ) /\ b = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) /\ ( E. c E. d ( E. k e. _om E. l e. _om ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( e |g c ) /\ y = ( ( M ^m _om ) \ ( b i^i d ) ) ) ) \/ E. n e. _om ( x = A.g n e /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. b } ) ) ) <-> ( E. i e. _om E. j e. _om ( e = ( i e.g j ) /\ b = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) /\ ( E. c E. d ( E. k e. _om E. l e. _om ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( e |g c ) /\ y = ( ( M ^m _om ) \ ( b i^i d ) ) ) ) \/ E. n e. _om ( x = A.g n e /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. b } ) ) ) )
53 oveq1 
 |-  ( e = ( i e.g j ) -> ( e |g c ) = ( ( i e.g j ) |g c ) )
54 53 eqeq2d 
 |-  ( e = ( i e.g j ) -> ( x = ( e |g c ) <-> x = ( ( i e.g j ) |g c ) ) )
55 ineq1 
 |-  ( b = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } -> ( b i^i d ) = ( { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } i^i d ) )
56 55 difeq2d 
 |-  ( b = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } -> ( ( M ^m _om ) \ ( b i^i d ) ) = ( ( M ^m _om ) \ ( { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } i^i d ) ) )
57 56 eqeq2d 
 |-  ( b = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } -> ( y = ( ( M ^m _om ) \ ( b i^i d ) ) <-> y = ( ( M ^m _om ) \ ( { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } i^i d ) ) ) )
58 54 57 bi2anan9 
 |-  ( ( e = ( i e.g j ) /\ b = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) -> ( ( x = ( e |g c ) /\ y = ( ( M ^m _om ) \ ( b i^i d ) ) ) <-> ( x = ( ( i e.g j ) |g c ) /\ y = ( ( M ^m _om ) \ ( { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } i^i d ) ) ) ) )
59 58 anbi2d 
 |-  ( ( e = ( i e.g j ) /\ b = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) -> ( ( E. k e. _om E. l e. _om ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( e |g c ) /\ y = ( ( M ^m _om ) \ ( b i^i d ) ) ) ) <-> ( E. k e. _om E. l e. _om ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( ( i e.g j ) |g c ) /\ y = ( ( M ^m _om ) \ ( { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } i^i d ) ) ) ) ) )
60 59 2exbidv 
 |-  ( ( e = ( i e.g j ) /\ b = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) -> ( E. c E. d ( E. k e. _om E. l e. _om ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( e |g c ) /\ y = ( ( M ^m _om ) \ ( b i^i d ) ) ) ) <-> E. c E. d ( E. k e. _om E. l e. _om ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( ( i e.g j ) |g c ) /\ y = ( ( M ^m _om ) \ ( { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } i^i d ) ) ) ) ) )
61 eqidd 
 |-  ( e = ( i e.g j ) -> n = n )
62 id 
 |-  ( e = ( i e.g j ) -> e = ( i e.g j ) )
63 61 62 goaleq12d 
 |-  ( e = ( i e.g j ) -> A.g n e = A.g n ( i e.g j ) )
64 63 eqeq2d 
 |-  ( e = ( i e.g j ) -> ( x = A.g n e <-> x = A.g n ( i e.g j ) ) )
65 nfrab1 
 |-  F/_ a { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) }
66 65 nfeq2 
 |-  F/ a b = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) }
67 eleq2 
 |-  ( b = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } -> ( ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. b <-> ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) )
68 67 ralbidv 
 |-  ( b = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } -> ( A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. b <-> A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) )
69 66 68 rabbid 
 |-  ( b = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } -> { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. b } = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } } )
70 69 eqeq2d 
 |-  ( b = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } -> ( y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. b } <-> y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } } ) )
71 64 70 bi2anan9 
 |-  ( ( e = ( i e.g j ) /\ b = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) -> ( ( x = A.g n e /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. b } ) <-> ( x = A.g n ( i e.g j ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } } ) ) )
72 71 rexbidv 
 |-  ( ( e = ( i e.g j ) /\ b = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) -> ( E. n e. _om ( x = A.g n e /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. b } ) <-> E. n e. _om ( x = A.g n ( i e.g j ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } } ) ) )
73 60 72 orbi12d 
 |-  ( ( e = ( i e.g j ) /\ b = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) -> ( ( E. c E. d ( E. k e. _om E. l e. _om ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( e |g c ) /\ y = ( ( M ^m _om ) \ ( b i^i d ) ) ) ) \/ E. n e. _om ( x = A.g n e /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. b } ) ) <-> ( E. c E. d ( E. k e. _om E. l e. _om ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( ( i e.g j ) |g c ) /\ y = ( ( M ^m _om ) \ ( { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } i^i d ) ) ) ) \/ E. n e. _om ( x = A.g n ( i e.g j ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } } ) ) ) )
74 73 adantl 
 |-  ( ( ( i e. _om /\ j e. _om ) /\ ( e = ( i e.g j ) /\ b = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) ) -> ( ( E. c E. d ( E. k e. _om E. l e. _om ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( e |g c ) /\ y = ( ( M ^m _om ) \ ( b i^i d ) ) ) ) \/ E. n e. _om ( x = A.g n e /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. b } ) ) <-> ( E. c E. d ( E. k e. _om E. l e. _om ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( ( i e.g j ) |g c ) /\ y = ( ( M ^m _om ) \ ( { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } i^i d ) ) ) ) \/ E. n e. _om ( x = A.g n ( i e.g j ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } } ) ) ) )
75 r19.41vv 
 |-  ( E. k e. _om E. l e. _om ( ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( ( i e.g j ) |g c ) /\ y = ( ( M ^m _om ) \ ( { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } i^i d ) ) ) ) <-> ( E. k e. _om E. l e. _om ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( ( i e.g j ) |g c ) /\ y = ( ( M ^m _om ) \ ( { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } i^i d ) ) ) ) )
76 oveq2 
 |-  ( c = ( k e.g l ) -> ( ( i e.g j ) |g c ) = ( ( i e.g j ) |g ( k e.g l ) ) )
77 76 adantr 
 |-  ( ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) -> ( ( i e.g j ) |g c ) = ( ( i e.g j ) |g ( k e.g l ) ) )
78 77 eqeq2d 
 |-  ( ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) -> ( x = ( ( i e.g j ) |g c ) <-> x = ( ( i e.g j ) |g ( k e.g l ) ) ) )
79 ineq2 
 |-  ( d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } -> ( { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } i^i d ) = ( { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } i^i { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) )
80 79 difeq2d 
 |-  ( d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } -> ( ( M ^m _om ) \ ( { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } i^i d ) ) = ( ( M ^m _om ) \ ( { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } i^i { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) ) )
81 inrab 
 |-  ( { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } i^i { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) = { a e. ( M ^m _om ) | ( ( a ` i ) E ( a ` j ) /\ ( a ` k ) E ( a ` l ) ) }
82 81 difeq2i 
 |-  ( ( M ^m _om ) \ ( { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } i^i { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) ) = ( ( M ^m _om ) \ { a e. ( M ^m _om ) | ( ( a ` i ) E ( a ` j ) /\ ( a ` k ) E ( a ` l ) ) } )
83 notrab 
 |-  ( ( M ^m _om ) \ { a e. ( M ^m _om ) | ( ( a ` i ) E ( a ` j ) /\ ( a ` k ) E ( a ` l ) ) } ) = { a e. ( M ^m _om ) | -. ( ( a ` i ) E ( a ` j ) /\ ( a ` k ) E ( a ` l ) ) }
84 ianor 
 |-  ( -. ( ( a ` i ) E ( a ` j ) /\ ( a ` k ) E ( a ` l ) ) <-> ( -. ( a ` i ) E ( a ` j ) \/ -. ( a ` k ) E ( a ` l ) ) )
85 84 rabbii 
 |-  { a e. ( M ^m _om ) | -. ( ( a ` i ) E ( a ` j ) /\ ( a ` k ) E ( a ` l ) ) } = { a e. ( M ^m _om ) | ( -. ( a ` i ) E ( a ` j ) \/ -. ( a ` k ) E ( a ` l ) ) }
86 82 83 85 3eqtri 
 |-  ( ( M ^m _om ) \ ( { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } i^i { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) ) = { a e. ( M ^m _om ) | ( -. ( a ` i ) E ( a ` j ) \/ -. ( a ` k ) E ( a ` l ) ) }
87 80 86 eqtrdi 
 |-  ( d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } -> ( ( M ^m _om ) \ ( { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } i^i d ) ) = { a e. ( M ^m _om ) | ( -. ( a ` i ) E ( a ` j ) \/ -. ( a ` k ) E ( a ` l ) ) } )
88 87 eqeq2d 
 |-  ( d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } -> ( y = ( ( M ^m _om ) \ ( { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } i^i d ) ) <-> y = { a e. ( M ^m _om ) | ( -. ( a ` i ) E ( a ` j ) \/ -. ( a ` k ) E ( a ` l ) ) } ) )
89 88 adantl 
 |-  ( ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) -> ( y = ( ( M ^m _om ) \ ( { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } i^i d ) ) <-> y = { a e. ( M ^m _om ) | ( -. ( a ` i ) E ( a ` j ) \/ -. ( a ` k ) E ( a ` l ) ) } ) )
90 78 89 anbi12d 
 |-  ( ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) -> ( ( x = ( ( i e.g j ) |g c ) /\ y = ( ( M ^m _om ) \ ( { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } i^i d ) ) ) <-> ( x = ( ( i e.g j ) |g ( k e.g l ) ) /\ y = { a e. ( M ^m _om ) | ( -. ( a ` i ) E ( a ` j ) \/ -. ( a ` k ) E ( a ` l ) ) } ) ) )
91 90 biimpa 
 |-  ( ( ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( ( i e.g j ) |g c ) /\ y = ( ( M ^m _om ) \ ( { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } i^i d ) ) ) ) -> ( x = ( ( i e.g j ) |g ( k e.g l ) ) /\ y = { a e. ( M ^m _om ) | ( -. ( a ` i ) E ( a ` j ) \/ -. ( a ` k ) E ( a ` l ) ) } ) )
92 91 reximi 
 |-  ( E. l e. _om ( ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( ( i e.g j ) |g c ) /\ y = ( ( M ^m _om ) \ ( { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } i^i d ) ) ) ) -> E. l e. _om ( x = ( ( i e.g j ) |g ( k e.g l ) ) /\ y = { a e. ( M ^m _om ) | ( -. ( a ` i ) E ( a ` j ) \/ -. ( a ` k ) E ( a ` l ) ) } ) )
93 92 reximi 
 |-  ( E. k e. _om E. l e. _om ( ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( ( i e.g j ) |g c ) /\ y = ( ( M ^m _om ) \ ( { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } i^i d ) ) ) ) -> E. k e. _om E. l e. _om ( x = ( ( i e.g j ) |g ( k e.g l ) ) /\ y = { a e. ( M ^m _om ) | ( -. ( a ` i ) E ( a ` j ) \/ -. ( a ` k ) E ( a ` l ) ) } ) )
94 75 93 sylbir 
 |-  ( ( E. k e. _om E. l e. _om ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( ( i e.g j ) |g c ) /\ y = ( ( M ^m _om ) \ ( { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } i^i d ) ) ) ) -> E. k e. _om E. l e. _om ( x = ( ( i e.g j ) |g ( k e.g l ) ) /\ y = { a e. ( M ^m _om ) | ( -. ( a ` i ) E ( a ` j ) \/ -. ( a ` k ) E ( a ` l ) ) } ) )
95 94 exlimivv 
 |-  ( E. c E. d ( E. k e. _om E. l e. _om ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( ( i e.g j ) |g c ) /\ y = ( ( M ^m _om ) \ ( { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } i^i d ) ) ) ) -> E. k e. _om E. l e. _om ( x = ( ( i e.g j ) |g ( k e.g l ) ) /\ y = { a e. ( M ^m _om ) | ( -. ( a ` i ) E ( a ` j ) \/ -. ( a ` k ) E ( a ` l ) ) } ) )
96 95 a1i 
 |-  ( ( ( i e. _om /\ j e. _om ) /\ ( e = ( i e.g j ) /\ b = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) ) -> ( E. c E. d ( E. k e. _om E. l e. _om ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( ( i e.g j ) |g c ) /\ y = ( ( M ^m _om ) \ ( { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } i^i d ) ) ) ) -> E. k e. _om E. l e. _om ( x = ( ( i e.g j ) |g ( k e.g l ) ) /\ y = { a e. ( M ^m _om ) | ( -. ( a ` i ) E ( a ` j ) \/ -. ( a ` k ) E ( a ` l ) ) } ) ) )
97 simpr 
 |-  ( ( ( i e. _om /\ j e. _om ) /\ n e. _om ) -> n e. _om )
98 simpll 
 |-  ( ( ( i e. _om /\ j e. _om ) /\ n e. _om ) -> i e. _om )
99 simplr 
 |-  ( ( ( i e. _om /\ j e. _om ) /\ n e. _om ) -> j e. _om )
100 fveq1 
 |-  ( a = b -> ( a ` i ) = ( b ` i ) )
101 fveq1 
 |-  ( a = b -> ( a ` j ) = ( b ` j ) )
102 100 101 breq12d 
 |-  ( a = b -> ( ( a ` i ) E ( a ` j ) <-> ( b ` i ) E ( b ` j ) ) )
103 102 cbvrabv 
 |-  { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } = { b e. ( M ^m _om ) | ( b ` i ) E ( b ` j ) }
104 103 eleq2i 
 |-  ( ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } <-> ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. { b e. ( M ^m _om ) | ( b ` i ) E ( b ` j ) } )
105 104 ralbii 
 |-  ( A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } <-> A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. { b e. ( M ^m _om ) | ( b ` i ) E ( b ` j ) } )
106 105 rabbii 
 |-  { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } } = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. { b e. ( M ^m _om ) | ( b ` i ) E ( b ` j ) } }
107 satfv1lem 
 |-  ( ( n e. _om /\ i e. _om /\ j e. _om ) -> { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. { b e. ( M ^m _om ) | ( b ` i ) E ( b ` j ) } } = { a e. ( M ^m _om ) | A. z e. M if- ( i = n , if- ( j = n , z E z , z E ( a ` j ) ) , if- ( j = n , ( a ` i ) E z , ( a ` i ) E ( a ` j ) ) ) } )
108 106 107 eqtrid 
 |-  ( ( n e. _om /\ i e. _om /\ j e. _om ) -> { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } } = { a e. ( M ^m _om ) | A. z e. M if- ( i = n , if- ( j = n , z E z , z E ( a ` j ) ) , if- ( j = n , ( a ` i ) E z , ( a ` i ) E ( a ` j ) ) ) } )
109 97 98 99 108 syl3anc 
 |-  ( ( ( i e. _om /\ j e. _om ) /\ n e. _om ) -> { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } } = { a e. ( M ^m _om ) | A. z e. M if- ( i = n , if- ( j = n , z E z , z E ( a ` j ) ) , if- ( j = n , ( a ` i ) E z , ( a ` i ) E ( a ` j ) ) ) } )
110 109 eqeq2d 
 |-  ( ( ( i e. _om /\ j e. _om ) /\ n e. _om ) -> ( y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } } <-> y = { a e. ( M ^m _om ) | A. z e. M if- ( i = n , if- ( j = n , z E z , z E ( a ` j ) ) , if- ( j = n , ( a ` i ) E z , ( a ` i ) E ( a ` j ) ) ) } ) )
111 110 biimpd 
 |-  ( ( ( i e. _om /\ j e. _om ) /\ n e. _om ) -> ( y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } } -> y = { a e. ( M ^m _om ) | A. z e. M if- ( i = n , if- ( j = n , z E z , z E ( a ` j ) ) , if- ( j = n , ( a ` i ) E z , ( a ` i ) E ( a ` j ) ) ) } ) )
112 111 anim2d 
 |-  ( ( ( i e. _om /\ j e. _om ) /\ n e. _om ) -> ( ( x = A.g n ( i e.g j ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } } ) -> ( x = A.g n ( i e.g j ) /\ y = { a e. ( M ^m _om ) | A. z e. M if- ( i = n , if- ( j = n , z E z , z E ( a ` j ) ) , if- ( j = n , ( a ` i ) E z , ( a ` i ) E ( a ` j ) ) ) } ) ) )
113 112 reximdva 
 |-  ( ( i e. _om /\ j e. _om ) -> ( E. n e. _om ( x = A.g n ( i e.g j ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } } ) -> E. n e. _om ( x = A.g n ( i e.g j ) /\ y = { a e. ( M ^m _om ) | A. z e. M if- ( i = n , if- ( j = n , z E z , z E ( a ` j ) ) , if- ( j = n , ( a ` i ) E z , ( a ` i ) E ( a ` j ) ) ) } ) ) )
114 113 adantr 
 |-  ( ( ( i e. _om /\ j e. _om ) /\ ( e = ( i e.g j ) /\ b = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) ) -> ( E. n e. _om ( x = A.g n ( i e.g j ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } } ) -> E. n e. _om ( x = A.g n ( i e.g j ) /\ y = { a e. ( M ^m _om ) | A. z e. M if- ( i = n , if- ( j = n , z E z , z E ( a ` j ) ) , if- ( j = n , ( a ` i ) E z , ( a ` i ) E ( a ` j ) ) ) } ) ) )
115 96 114 orim12d 
 |-  ( ( ( i e. _om /\ j e. _om ) /\ ( e = ( i e.g j ) /\ b = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) ) -> ( ( E. c E. d ( E. k e. _om E. l e. _om ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( ( i e.g j ) |g c ) /\ y = ( ( M ^m _om ) \ ( { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } i^i d ) ) ) ) \/ E. n e. _om ( x = A.g n ( i e.g j ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } } ) ) -> ( E. k e. _om E. l e. _om ( x = ( ( i e.g j ) |g ( k e.g l ) ) /\ y = { a e. ( M ^m _om ) | ( -. ( a ` i ) E ( a ` j ) \/ -. ( a ` k ) E ( a ` l ) ) } ) \/ E. n e. _om ( x = A.g n ( i e.g j ) /\ y = { a e. ( M ^m _om ) | A. z e. M if- ( i = n , if- ( j = n , z E z , z E ( a ` j ) ) , if- ( j = n , ( a ` i ) E z , ( a ` i ) E ( a ` j ) ) ) } ) ) ) )
116 74 115 sylbid 
 |-  ( ( ( i e. _om /\ j e. _om ) /\ ( e = ( i e.g j ) /\ b = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) ) -> ( ( E. c E. d ( E. k e. _om E. l e. _om ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( e |g c ) /\ y = ( ( M ^m _om ) \ ( b i^i d ) ) ) ) \/ E. n e. _om ( x = A.g n e /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. b } ) ) -> ( E. k e. _om E. l e. _om ( x = ( ( i e.g j ) |g ( k e.g l ) ) /\ y = { a e. ( M ^m _om ) | ( -. ( a ` i ) E ( a ` j ) \/ -. ( a ` k ) E ( a ` l ) ) } ) \/ E. n e. _om ( x = A.g n ( i e.g j ) /\ y = { a e. ( M ^m _om ) | A. z e. M if- ( i = n , if- ( j = n , z E z , z E ( a ` j ) ) , if- ( j = n , ( a ` i ) E z , ( a ` i ) E ( a ` j ) ) ) } ) ) ) )
117 116 expimpd 
 |-  ( ( i e. _om /\ j e. _om ) -> ( ( ( e = ( i e.g j ) /\ b = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) /\ ( E. c E. d ( E. k e. _om E. l e. _om ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( e |g c ) /\ y = ( ( M ^m _om ) \ ( b i^i d ) ) ) ) \/ E. n e. _om ( x = A.g n e /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. b } ) ) ) -> ( E. k e. _om E. l e. _om ( x = ( ( i e.g j ) |g ( k e.g l ) ) /\ y = { a e. ( M ^m _om ) | ( -. ( a ` i ) E ( a ` j ) \/ -. ( a ` k ) E ( a ` l ) ) } ) \/ E. n e. _om ( x = A.g n ( i e.g j ) /\ y = { a e. ( M ^m _om ) | A. z e. M if- ( i = n , if- ( j = n , z E z , z E ( a ` j ) ) , if- ( j = n , ( a ` i ) E z , ( a ` i ) E ( a ` j ) ) ) } ) ) ) )
118 117 reximdva 
 |-  ( i e. _om -> ( E. j e. _om ( ( e = ( i e.g j ) /\ b = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) /\ ( E. c E. d ( E. k e. _om E. l e. _om ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( e |g c ) /\ y = ( ( M ^m _om ) \ ( b i^i d ) ) ) ) \/ E. n e. _om ( x = A.g n e /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. b } ) ) ) -> E. j e. _om ( E. k e. _om E. l e. _om ( x = ( ( i e.g j ) |g ( k e.g l ) ) /\ y = { a e. ( M ^m _om ) | ( -. ( a ` i ) E ( a ` j ) \/ -. ( a ` k ) E ( a ` l ) ) } ) \/ E. n e. _om ( x = A.g n ( i e.g j ) /\ y = { a e. ( M ^m _om ) | A. z e. M if- ( i = n , if- ( j = n , z E z , z E ( a ` j ) ) , if- ( j = n , ( a ` i ) E z , ( a ` i ) E ( a ` j ) ) ) } ) ) ) )
119 118 reximia 
 |-  ( E. i e. _om E. j e. _om ( ( e = ( i e.g j ) /\ b = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) /\ ( E. c E. d ( E. k e. _om E. l e. _om ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( e |g c ) /\ y = ( ( M ^m _om ) \ ( b i^i d ) ) ) ) \/ E. n e. _om ( x = A.g n e /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. b } ) ) ) -> E. i e. _om E. j e. _om ( E. k e. _om E. l e. _om ( x = ( ( i e.g j ) |g ( k e.g l ) ) /\ y = { a e. ( M ^m _om ) | ( -. ( a ` i ) E ( a ` j ) \/ -. ( a ` k ) E ( a ` l ) ) } ) \/ E. n e. _om ( x = A.g n ( i e.g j ) /\ y = { a e. ( M ^m _om ) | A. z e. M if- ( i = n , if- ( j = n , z E z , z E ( a ` j ) ) , if- ( j = n , ( a ` i ) E z , ( a ` i ) E ( a ` j ) ) ) } ) ) )
120 52 119 sylbir 
 |-  ( ( E. i e. _om E. j e. _om ( e = ( i e.g j ) /\ b = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) /\ ( E. c E. d ( E. k e. _om E. l e. _om ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( e |g c ) /\ y = ( ( M ^m _om ) \ ( b i^i d ) ) ) ) \/ E. n e. _om ( x = A.g n e /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. b } ) ) ) -> E. i e. _om E. j e. _om ( E. k e. _om E. l e. _om ( x = ( ( i e.g j ) |g ( k e.g l ) ) /\ y = { a e. ( M ^m _om ) | ( -. ( a ` i ) E ( a ` j ) \/ -. ( a ` k ) E ( a ` l ) ) } ) \/ E. n e. _om ( x = A.g n ( i e.g j ) /\ y = { a e. ( M ^m _om ) | A. z e. M if- ( i = n , if- ( j = n , z E z , z E ( a ` j ) ) , if- ( j = n , ( a ` i ) E z , ( a ` i ) E ( a ` j ) ) ) } ) ) )
121 120 exlimivv 
 |-  ( E. e E. b ( E. i e. _om E. j e. _om ( e = ( i e.g j ) /\ b = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) /\ ( E. c E. d ( E. k e. _om E. l e. _om ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( e |g c ) /\ y = ( ( M ^m _om ) \ ( b i^i d ) ) ) ) \/ E. n e. _om ( x = A.g n e /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. b } ) ) ) -> E. i e. _om E. j e. _om ( E. k e. _om E. l e. _om ( x = ( ( i e.g j ) |g ( k e.g l ) ) /\ y = { a e. ( M ^m _om ) | ( -. ( a ` i ) E ( a ` j ) \/ -. ( a ` k ) E ( a ` l ) ) } ) \/ E. n e. _om ( x = A.g n ( i e.g j ) /\ y = { a e. ( M ^m _om ) | A. z e. M if- ( i = n , if- ( j = n , z E z , z E ( a ` j ) ) , if- ( j = n , ( a ` i ) E z , ( a ` i ) E ( a ` j ) ) ) } ) ) )
122 ovex 
 |-  ( i e.g j ) e. _V
123 ovex 
 |-  ( M ^m _om ) e. _V
124 123 rabex 
 |-  { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } e. _V
125 122 124 pm3.2i 
 |-  ( ( i e.g j ) e. _V /\ { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } e. _V )
126 eqid 
 |-  ( k e.g l ) = ( k e.g l )
127 eqid 
 |-  { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) }
128 126 127 pm3.2i 
 |-  ( ( k e.g l ) = ( k e.g l ) /\ { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } )
129 86 eqcomi 
 |-  { a e. ( M ^m _om ) | ( -. ( a ` i ) E ( a ` j ) \/ -. ( a ` k ) E ( a ` l ) ) } = ( ( M ^m _om ) \ ( { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } i^i { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) )
130 129 eqeq2i 
 |-  ( y = { a e. ( M ^m _om ) | ( -. ( a ` i ) E ( a ` j ) \/ -. ( a ` k ) E ( a ` l ) ) } <-> y = ( ( M ^m _om ) \ ( { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } i^i { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) ) )
131 130 biimpi 
 |-  ( y = { a e. ( M ^m _om ) | ( -. ( a ` i ) E ( a ` j ) \/ -. ( a ` k ) E ( a ` l ) ) } -> y = ( ( M ^m _om ) \ ( { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } i^i { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) ) )
132 131 anim2i 
 |-  ( ( x = ( ( i e.g j ) |g ( k e.g l ) ) /\ y = { a e. ( M ^m _om ) | ( -. ( a ` i ) E ( a ` j ) \/ -. ( a ` k ) E ( a ` l ) ) } ) -> ( x = ( ( i e.g j ) |g ( k e.g l ) ) /\ y = ( ( M ^m _om ) \ ( { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } i^i { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) ) ) )
133 ovex 
 |-  ( k e.g l ) e. _V
134 123 rabex 
 |-  { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } e. _V
135 eqeq1 
 |-  ( c = ( k e.g l ) -> ( c = ( k e.g l ) <-> ( k e.g l ) = ( k e.g l ) ) )
136 eqeq1 
 |-  ( d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } -> ( d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } <-> { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) )
137 135 136 bi2anan9 
 |-  ( ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) -> ( ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) <-> ( ( k e.g l ) = ( k e.g l ) /\ { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) ) )
138 76 eqeq2d 
 |-  ( c = ( k e.g l ) -> ( x = ( ( i e.g j ) |g c ) <-> x = ( ( i e.g j ) |g ( k e.g l ) ) ) )
139 80 eqeq2d 
 |-  ( d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } -> ( y = ( ( M ^m _om ) \ ( { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } i^i d ) ) <-> y = ( ( M ^m _om ) \ ( { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } i^i { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) ) ) )
140 138 139 bi2anan9 
 |-  ( ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) -> ( ( x = ( ( i e.g j ) |g c ) /\ y = ( ( M ^m _om ) \ ( { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } i^i d ) ) ) <-> ( x = ( ( i e.g j ) |g ( k e.g l ) ) /\ y = ( ( M ^m _om ) \ ( { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } i^i { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) ) ) ) )
141 137 140 anbi12d 
 |-  ( ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) -> ( ( ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( ( i e.g j ) |g c ) /\ y = ( ( M ^m _om ) \ ( { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } i^i d ) ) ) ) <-> ( ( ( k e.g l ) = ( k e.g l ) /\ { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( ( i e.g j ) |g ( k e.g l ) ) /\ y = ( ( M ^m _om ) \ ( { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } i^i { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) ) ) ) ) )
142 133 134 141 spc2ev 
 |-  ( ( ( ( k e.g l ) = ( k e.g l ) /\ { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( ( i e.g j ) |g ( k e.g l ) ) /\ y = ( ( M ^m _om ) \ ( { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } i^i { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) ) ) ) -> E. c E. d ( ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( ( i e.g j ) |g c ) /\ y = ( ( M ^m _om ) \ ( { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } i^i d ) ) ) ) )
143 128 132 142 sylancr 
 |-  ( ( x = ( ( i e.g j ) |g ( k e.g l ) ) /\ y = { a e. ( M ^m _om ) | ( -. ( a ` i ) E ( a ` j ) \/ -. ( a ` k ) E ( a ` l ) ) } ) -> E. c E. d ( ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( ( i e.g j ) |g c ) /\ y = ( ( M ^m _om ) \ ( { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } i^i d ) ) ) ) )
144 143 reximi 
 |-  ( E. l e. _om ( x = ( ( i e.g j ) |g ( k e.g l ) ) /\ y = { a e. ( M ^m _om ) | ( -. ( a ` i ) E ( a ` j ) \/ -. ( a ` k ) E ( a ` l ) ) } ) -> E. l e. _om E. c E. d ( ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( ( i e.g j ) |g c ) /\ y = ( ( M ^m _om ) \ ( { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } i^i d ) ) ) ) )
145 144 reximi 
 |-  ( E. k e. _om E. l e. _om ( x = ( ( i e.g j ) |g ( k e.g l ) ) /\ y = { a e. ( M ^m _om ) | ( -. ( a ` i ) E ( a ` j ) \/ -. ( a ` k ) E ( a ` l ) ) } ) -> E. k e. _om E. l e. _om E. c E. d ( ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( ( i e.g j ) |g c ) /\ y = ( ( M ^m _om ) \ ( { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } i^i d ) ) ) ) )
146 75 bicomi 
 |-  ( ( E. k e. _om E. l e. _om ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( ( i e.g j ) |g c ) /\ y = ( ( M ^m _om ) \ ( { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } i^i d ) ) ) ) <-> E. k e. _om E. l e. _om ( ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( ( i e.g j ) |g c ) /\ y = ( ( M ^m _om ) \ ( { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } i^i d ) ) ) ) )
147 146 2exbii 
 |-  ( E. c E. d ( E. k e. _om E. l e. _om ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( ( i e.g j ) |g c ) /\ y = ( ( M ^m _om ) \ ( { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } i^i d ) ) ) ) <-> E. c E. d E. k e. _om E. l e. _om ( ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( ( i e.g j ) |g c ) /\ y = ( ( M ^m _om ) \ ( { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } i^i d ) ) ) ) )
148 2ex2rexrot 
 |-  ( E. c E. d E. k e. _om E. l e. _om ( ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( ( i e.g j ) |g c ) /\ y = ( ( M ^m _om ) \ ( { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } i^i d ) ) ) ) <-> E. k e. _om E. l e. _om E. c E. d ( ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( ( i e.g j ) |g c ) /\ y = ( ( M ^m _om ) \ ( { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } i^i d ) ) ) ) )
149 147 148 bitri 
 |-  ( E. c E. d ( E. k e. _om E. l e. _om ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( ( i e.g j ) |g c ) /\ y = ( ( M ^m _om ) \ ( { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } i^i d ) ) ) ) <-> E. k e. _om E. l e. _om E. c E. d ( ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( ( i e.g j ) |g c ) /\ y = ( ( M ^m _om ) \ ( { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } i^i d ) ) ) ) )
150 145 149 sylibr 
 |-  ( E. k e. _om E. l e. _om ( x = ( ( i e.g j ) |g ( k e.g l ) ) /\ y = { a e. ( M ^m _om ) | ( -. ( a ` i ) E ( a ` j ) \/ -. ( a ` k ) E ( a ` l ) ) } ) -> E. c E. d ( E. k e. _om E. l e. _om ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( ( i e.g j ) |g c ) /\ y = ( ( M ^m _om ) \ ( { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } i^i d ) ) ) ) )
151 150 a1i 
 |-  ( ( i e. _om /\ j e. _om ) -> ( E. k e. _om E. l e. _om ( x = ( ( i e.g j ) |g ( k e.g l ) ) /\ y = { a e. ( M ^m _om ) | ( -. ( a ` i ) E ( a ` j ) \/ -. ( a ` k ) E ( a ` l ) ) } ) -> E. c E. d ( E. k e. _om E. l e. _om ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( ( i e.g j ) |g c ) /\ y = ( ( M ^m _om ) \ ( { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } i^i d ) ) ) ) ) )
152 109 eqcomd 
 |-  ( ( ( i e. _om /\ j e. _om ) /\ n e. _om ) -> { a e. ( M ^m _om ) | A. z e. M if- ( i = n , if- ( j = n , z E z , z E ( a ` j ) ) , if- ( j = n , ( a ` i ) E z , ( a ` i ) E ( a ` j ) ) ) } = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } } )
153 152 eqeq2d 
 |-  ( ( ( i e. _om /\ j e. _om ) /\ n e. _om ) -> ( y = { a e. ( M ^m _om ) | A. z e. M if- ( i = n , if- ( j = n , z E z , z E ( a ` j ) ) , if- ( j = n , ( a ` i ) E z , ( a ` i ) E ( a ` j ) ) ) } <-> y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } } ) )
154 153 biimpd 
 |-  ( ( ( i e. _om /\ j e. _om ) /\ n e. _om ) -> ( y = { a e. ( M ^m _om ) | A. z e. M if- ( i = n , if- ( j = n , z E z , z E ( a ` j ) ) , if- ( j = n , ( a ` i ) E z , ( a ` i ) E ( a ` j ) ) ) } -> y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } } ) )
155 154 anim2d 
 |-  ( ( ( i e. _om /\ j e. _om ) /\ n e. _om ) -> ( ( x = A.g n ( i e.g j ) /\ y = { a e. ( M ^m _om ) | A. z e. M if- ( i = n , if- ( j = n , z E z , z E ( a ` j ) ) , if- ( j = n , ( a ` i ) E z , ( a ` i ) E ( a ` j ) ) ) } ) -> ( x = A.g n ( i e.g j ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } } ) ) )
156 155 reximdva 
 |-  ( ( i e. _om /\ j e. _om ) -> ( E. n e. _om ( x = A.g n ( i e.g j ) /\ y = { a e. ( M ^m _om ) | A. z e. M if- ( i = n , if- ( j = n , z E z , z E ( a ` j ) ) , if- ( j = n , ( a ` i ) E z , ( a ` i ) E ( a ` j ) ) ) } ) -> E. n e. _om ( x = A.g n ( i e.g j ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } } ) ) )
157 151 156 orim12d 
 |-  ( ( i e. _om /\ j e. _om ) -> ( ( E. k e. _om E. l e. _om ( x = ( ( i e.g j ) |g ( k e.g l ) ) /\ y = { a e. ( M ^m _om ) | ( -. ( a ` i ) E ( a ` j ) \/ -. ( a ` k ) E ( a ` l ) ) } ) \/ E. n e. _om ( x = A.g n ( i e.g j ) /\ y = { a e. ( M ^m _om ) | A. z e. M if- ( i = n , if- ( j = n , z E z , z E ( a ` j ) ) , if- ( j = n , ( a ` i ) E z , ( a ` i ) E ( a ` j ) ) ) } ) ) -> ( E. c E. d ( E. k e. _om E. l e. _om ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( ( i e.g j ) |g c ) /\ y = ( ( M ^m _om ) \ ( { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } i^i d ) ) ) ) \/ E. n e. _om ( x = A.g n ( i e.g j ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } } ) ) ) )
158 157 imp 
 |-  ( ( ( i e. _om /\ j e. _om ) /\ ( E. k e. _om E. l e. _om ( x = ( ( i e.g j ) |g ( k e.g l ) ) /\ y = { a e. ( M ^m _om ) | ( -. ( a ` i ) E ( a ` j ) \/ -. ( a ` k ) E ( a ` l ) ) } ) \/ E. n e. _om ( x = A.g n ( i e.g j ) /\ y = { a e. ( M ^m _om ) | A. z e. M if- ( i = n , if- ( j = n , z E z , z E ( a ` j ) ) , if- ( j = n , ( a ` i ) E z , ( a ` i ) E ( a ` j ) ) ) } ) ) ) -> ( E. c E. d ( E. k e. _om E. l e. _om ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( ( i e.g j ) |g c ) /\ y = ( ( M ^m _om ) \ ( { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } i^i d ) ) ) ) \/ E. n e. _om ( x = A.g n ( i e.g j ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } } ) ) )
159 eqid 
 |-  ( i e.g j ) = ( i e.g j )
160 eqid 
 |-  { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) }
161 159 160 pm3.2i 
 |-  ( ( i e.g j ) = ( i e.g j ) /\ { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } )
162 158 161 jctil 
 |-  ( ( ( i e. _om /\ j e. _om ) /\ ( E. k e. _om E. l e. _om ( x = ( ( i e.g j ) |g ( k e.g l ) ) /\ y = { a e. ( M ^m _om ) | ( -. ( a ` i ) E ( a ` j ) \/ -. ( a ` k ) E ( a ` l ) ) } ) \/ E. n e. _om ( x = A.g n ( i e.g j ) /\ y = { a e. ( M ^m _om ) | A. z e. M if- ( i = n , if- ( j = n , z E z , z E ( a ` j ) ) , if- ( j = n , ( a ` i ) E z , ( a ` i ) E ( a ` j ) ) ) } ) ) ) -> ( ( ( i e.g j ) = ( i e.g j ) /\ { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) /\ ( E. c E. d ( E. k e. _om E. l e. _om ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( ( i e.g j ) |g c ) /\ y = ( ( M ^m _om ) \ ( { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } i^i d ) ) ) ) \/ E. n e. _om ( x = A.g n ( i e.g j ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } } ) ) ) )
163 eqeq1 
 |-  ( e = ( i e.g j ) -> ( e = ( i e.g j ) <-> ( i e.g j ) = ( i e.g j ) ) )
164 eqeq1 
 |-  ( b = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } -> ( b = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } <-> { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) )
165 163 164 bi2anan9 
 |-  ( ( e = ( i e.g j ) /\ b = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) -> ( ( e = ( i e.g j ) /\ b = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) <-> ( ( i e.g j ) = ( i e.g j ) /\ { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) ) )
166 165 73 anbi12d 
 |-  ( ( e = ( i e.g j ) /\ b = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) -> ( ( ( e = ( i e.g j ) /\ b = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) /\ ( E. c E. d ( E. k e. _om E. l e. _om ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( e |g c ) /\ y = ( ( M ^m _om ) \ ( b i^i d ) ) ) ) \/ E. n e. _om ( x = A.g n e /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. b } ) ) ) <-> ( ( ( i e.g j ) = ( i e.g j ) /\ { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) /\ ( E. c E. d ( E. k e. _om E. l e. _om ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( ( i e.g j ) |g c ) /\ y = ( ( M ^m _om ) \ ( { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } i^i d ) ) ) ) \/ E. n e. _om ( x = A.g n ( i e.g j ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } } ) ) ) ) )
167 166 spc2egv 
 |-  ( ( ( i e.g j ) e. _V /\ { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } e. _V ) -> ( ( ( ( i e.g j ) = ( i e.g j ) /\ { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) /\ ( E. c E. d ( E. k e. _om E. l e. _om ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( ( i e.g j ) |g c ) /\ y = ( ( M ^m _om ) \ ( { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } i^i d ) ) ) ) \/ E. n e. _om ( x = A.g n ( i e.g j ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } } ) ) ) -> E. e E. b ( ( e = ( i e.g j ) /\ b = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) /\ ( E. c E. d ( E. k e. _om E. l e. _om ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( e |g c ) /\ y = ( ( M ^m _om ) \ ( b i^i d ) ) ) ) \/ E. n e. _om ( x = A.g n e /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. b } ) ) ) ) )
168 125 162 167 mpsyl 
 |-  ( ( ( i e. _om /\ j e. _om ) /\ ( E. k e. _om E. l e. _om ( x = ( ( i e.g j ) |g ( k e.g l ) ) /\ y = { a e. ( M ^m _om ) | ( -. ( a ` i ) E ( a ` j ) \/ -. ( a ` k ) E ( a ` l ) ) } ) \/ E. n e. _om ( x = A.g n ( i e.g j ) /\ y = { a e. ( M ^m _om ) | A. z e. M if- ( i = n , if- ( j = n , z E z , z E ( a ` j ) ) , if- ( j = n , ( a ` i ) E z , ( a ` i ) E ( a ` j ) ) ) } ) ) ) -> E. e E. b ( ( e = ( i e.g j ) /\ b = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) /\ ( E. c E. d ( E. k e. _om E. l e. _om ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( e |g c ) /\ y = ( ( M ^m _om ) \ ( b i^i d ) ) ) ) \/ E. n e. _om ( x = A.g n e /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. b } ) ) ) )
169 168 ex 
 |-  ( ( i e. _om /\ j e. _om ) -> ( ( E. k e. _om E. l e. _om ( x = ( ( i e.g j ) |g ( k e.g l ) ) /\ y = { a e. ( M ^m _om ) | ( -. ( a ` i ) E ( a ` j ) \/ -. ( a ` k ) E ( a ` l ) ) } ) \/ E. n e. _om ( x = A.g n ( i e.g j ) /\ y = { a e. ( M ^m _om ) | A. z e. M if- ( i = n , if- ( j = n , z E z , z E ( a ` j ) ) , if- ( j = n , ( a ` i ) E z , ( a ` i ) E ( a ` j ) ) ) } ) ) -> E. e E. b ( ( e = ( i e.g j ) /\ b = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) /\ ( E. c E. d ( E. k e. _om E. l e. _om ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( e |g c ) /\ y = ( ( M ^m _om ) \ ( b i^i d ) ) ) ) \/ E. n e. _om ( x = A.g n e /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. b } ) ) ) ) )
170 169 reximdva 
 |-  ( i e. _om -> ( E. j e. _om ( E. k e. _om E. l e. _om ( x = ( ( i e.g j ) |g ( k e.g l ) ) /\ y = { a e. ( M ^m _om ) | ( -. ( a ` i ) E ( a ` j ) \/ -. ( a ` k ) E ( a ` l ) ) } ) \/ E. n e. _om ( x = A.g n ( i e.g j ) /\ y = { a e. ( M ^m _om ) | A. z e. M if- ( i = n , if- ( j = n , z E z , z E ( a ` j ) ) , if- ( j = n , ( a ` i ) E z , ( a ` i ) E ( a ` j ) ) ) } ) ) -> E. j e. _om E. e E. b ( ( e = ( i e.g j ) /\ b = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) /\ ( E. c E. d ( E. k e. _om E. l e. _om ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( e |g c ) /\ y = ( ( M ^m _om ) \ ( b i^i d ) ) ) ) \/ E. n e. _om ( x = A.g n e /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. b } ) ) ) ) )
171 170 reximia 
 |-  ( E. i e. _om E. j e. _om ( E. k e. _om E. l e. _om ( x = ( ( i e.g j ) |g ( k e.g l ) ) /\ y = { a e. ( M ^m _om ) | ( -. ( a ` i ) E ( a ` j ) \/ -. ( a ` k ) E ( a ` l ) ) } ) \/ E. n e. _om ( x = A.g n ( i e.g j ) /\ y = { a e. ( M ^m _om ) | A. z e. M if- ( i = n , if- ( j = n , z E z , z E ( a ` j ) ) , if- ( j = n , ( a ` i ) E z , ( a ` i ) E ( a ` j ) ) ) } ) ) -> E. i e. _om E. j e. _om E. e E. b ( ( e = ( i e.g j ) /\ b = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) /\ ( E. c E. d ( E. k e. _om E. l e. _om ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( e |g c ) /\ y = ( ( M ^m _om ) \ ( b i^i d ) ) ) ) \/ E. n e. _om ( x = A.g n e /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. b } ) ) ) )
172 52 bicomi 
 |-  ( ( E. i e. _om E. j e. _om ( e = ( i e.g j ) /\ b = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) /\ ( E. c E. d ( E. k e. _om E. l e. _om ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( e |g c ) /\ y = ( ( M ^m _om ) \ ( b i^i d ) ) ) ) \/ E. n e. _om ( x = A.g n e /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. b } ) ) ) <-> E. i e. _om E. j e. _om ( ( e = ( i e.g j ) /\ b = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) /\ ( E. c E. d ( E. k e. _om E. l e. _om ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( e |g c ) /\ y = ( ( M ^m _om ) \ ( b i^i d ) ) ) ) \/ E. n e. _om ( x = A.g n e /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. b } ) ) ) )
173 172 2exbii 
 |-  ( E. e E. b ( E. i e. _om E. j e. _om ( e = ( i e.g j ) /\ b = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) /\ ( E. c E. d ( E. k e. _om E. l e. _om ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( e |g c ) /\ y = ( ( M ^m _om ) \ ( b i^i d ) ) ) ) \/ E. n e. _om ( x = A.g n e /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. b } ) ) ) <-> E. e E. b E. i e. _om E. j e. _om ( ( e = ( i e.g j ) /\ b = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) /\ ( E. c E. d ( E. k e. _om E. l e. _om ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( e |g c ) /\ y = ( ( M ^m _om ) \ ( b i^i d ) ) ) ) \/ E. n e. _om ( x = A.g n e /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. b } ) ) ) )
174 2ex2rexrot 
 |-  ( E. e E. b E. i e. _om E. j e. _om ( ( e = ( i e.g j ) /\ b = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) /\ ( E. c E. d ( E. k e. _om E. l e. _om ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( e |g c ) /\ y = ( ( M ^m _om ) \ ( b i^i d ) ) ) ) \/ E. n e. _om ( x = A.g n e /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. b } ) ) ) <-> E. i e. _om E. j e. _om E. e E. b ( ( e = ( i e.g j ) /\ b = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) /\ ( E. c E. d ( E. k e. _om E. l e. _om ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( e |g c ) /\ y = ( ( M ^m _om ) \ ( b i^i d ) ) ) ) \/ E. n e. _om ( x = A.g n e /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. b } ) ) ) )
175 173 174 bitri 
 |-  ( E. e E. b ( E. i e. _om E. j e. _om ( e = ( i e.g j ) /\ b = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) /\ ( E. c E. d ( E. k e. _om E. l e. _om ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( e |g c ) /\ y = ( ( M ^m _om ) \ ( b i^i d ) ) ) ) \/ E. n e. _om ( x = A.g n e /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. b } ) ) ) <-> E. i e. _om E. j e. _om E. e E. b ( ( e = ( i e.g j ) /\ b = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) /\ ( E. c E. d ( E. k e. _om E. l e. _om ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( e |g c ) /\ y = ( ( M ^m _om ) \ ( b i^i d ) ) ) ) \/ E. n e. _om ( x = A.g n e /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. b } ) ) ) )
176 171 175 sylibr 
 |-  ( E. i e. _om E. j e. _om ( E. k e. _om E. l e. _om ( x = ( ( i e.g j ) |g ( k e.g l ) ) /\ y = { a e. ( M ^m _om ) | ( -. ( a ` i ) E ( a ` j ) \/ -. ( a ` k ) E ( a ` l ) ) } ) \/ E. n e. _om ( x = A.g n ( i e.g j ) /\ y = { a e. ( M ^m _om ) | A. z e. M if- ( i = n , if- ( j = n , z E z , z E ( a ` j ) ) , if- ( j = n , ( a ` i ) E z , ( a ` i ) E ( a ` j ) ) ) } ) ) -> E. e E. b ( E. i e. _om E. j e. _om ( e = ( i e.g j ) /\ b = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) /\ ( E. c E. d ( E. k e. _om E. l e. _om ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( e |g c ) /\ y = ( ( M ^m _om ) \ ( b i^i d ) ) ) ) \/ E. n e. _om ( x = A.g n e /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. b } ) ) ) )
177 121 176 impbii 
 |-  ( E. e E. b ( E. i e. _om E. j e. _om ( e = ( i e.g j ) /\ b = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) /\ ( E. c E. d ( E. k e. _om E. l e. _om ( c = ( k e.g l ) /\ d = { a e. ( M ^m _om ) | ( a ` k ) E ( a ` l ) } ) /\ ( x = ( e |g c ) /\ y = ( ( M ^m _om ) \ ( b i^i d ) ) ) ) \/ E. n e. _om ( x = A.g n e /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. b } ) ) ) <-> E. i e. _om E. j e. _om ( E. k e. _om E. l e. _om ( x = ( ( i e.g j ) |g ( k e.g l ) ) /\ y = { a e. ( M ^m _om ) | ( -. ( a ` i ) E ( a ` j ) \/ -. ( a ` k ) E ( a ` l ) ) } ) \/ E. n e. _om ( x = A.g n ( i e.g j ) /\ y = { a e. ( M ^m _om ) | A. z e. M if- ( i = n , if- ( j = n , z E z , z E ( a ` j ) ) , if- ( j = n , ( a ` i ) E z , ( a ` i ) E ( a ` j ) ) ) } ) ) )
178 51 177 bitrdi 
 |-  ( ( M e. V /\ E e. W ) -> ( E. e E. b ( E. i e. _om E. j e. _om ( e = ( i e.g j ) /\ b = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) /\ ( E. p e. ( S ` (/) ) ( x = ( e |g ( 1st ` p ) ) /\ y = ( ( M ^m _om ) \ ( b i^i ( 2nd ` p ) ) ) ) \/ E. n e. _om ( x = A.g n e /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. b } ) ) ) <-> E. i e. _om E. j e. _om ( E. k e. _om E. l e. _om ( x = ( ( i e.g j ) |g ( k e.g l ) ) /\ y = { a e. ( M ^m _om ) | ( -. ( a ` i ) E ( a ` j ) \/ -. ( a ` k ) E ( a ` l ) ) } ) \/ E. n e. _om ( x = A.g n ( i e.g j ) /\ y = { a e. ( M ^m _om ) | A. z e. M if- ( i = n , if- ( j = n , z E z , z E ( a ` j ) ) , if- ( j = n , ( a ` i ) E z , ( a ` i ) E ( a ` j ) ) ) } ) ) ) )
179 33 178 bitrd 
 |-  ( ( M e. V /\ E e. W ) -> ( E. o e. ( S ` (/) ) ( E. p e. ( S ` (/) ) ( x = ( ( 1st ` o ) |g ( 1st ` p ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` o ) i^i ( 2nd ` p ) ) ) ) \/ E. n e. _om ( x = A.g n ( 1st ` o ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. ( 2nd ` o ) } ) ) <-> E. i e. _om E. j e. _om ( E. k e. _om E. l e. _om ( x = ( ( i e.g j ) |g ( k e.g l ) ) /\ y = { a e. ( M ^m _om ) | ( -. ( a ` i ) E ( a ` j ) \/ -. ( a ` k ) E ( a ` l ) ) } ) \/ E. n e. _om ( x = A.g n ( i e.g j ) /\ y = { a e. ( M ^m _om ) | A. z e. M if- ( i = n , if- ( j = n , z E z , z E ( a ` j ) ) , if- ( j = n , ( a ` i ) E z , ( a ` i ) E ( a ` j ) ) ) } ) ) ) )
180 179 opabbidv 
 |-  ( ( M e. V /\ E e. W ) -> { <. x , y >. | E. o e. ( S ` (/) ) ( E. p e. ( S ` (/) ) ( x = ( ( 1st ` o ) |g ( 1st ` p ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` o ) i^i ( 2nd ` p ) ) ) ) \/ E. n e. _om ( x = A.g n ( 1st ` o ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. ( 2nd ` o ) } ) ) } = { <. x , y >. | E. i e. _om E. j e. _om ( E. k e. _om E. l e. _om ( x = ( ( i e.g j ) |g ( k e.g l ) ) /\ y = { a e. ( M ^m _om ) | ( -. ( a ` i ) E ( a ` j ) \/ -. ( a ` k ) E ( a ` l ) ) } ) \/ E. n e. _om ( x = A.g n ( i e.g j ) /\ y = { a e. ( M ^m _om ) | A. z e. M if- ( i = n , if- ( j = n , z E z , z E ( a ` j ) ) , if- ( j = n , ( a ` i ) E z , ( a ` i ) E ( a ` j ) ) ) } ) ) } )
181 180 uneq2d 
 |-  ( ( M e. V /\ E e. W ) -> ( ( S ` (/) ) u. { <. x , y >. | E. o e. ( S ` (/) ) ( E. p e. ( S ` (/) ) ( x = ( ( 1st ` o ) |g ( 1st ` p ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` o ) i^i ( 2nd ` p ) ) ) ) \/ E. n e. _om ( x = A.g n ( 1st ` o ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. n , z >. } u. ( a |` ( _om \ { n } ) ) ) e. ( 2nd ` o ) } ) ) } ) = ( ( S ` (/) ) u. { <. x , y >. | E. i e. _om E. j e. _om ( E. k e. _om E. l e. _om ( x = ( ( i e.g j ) |g ( k e.g l ) ) /\ y = { a e. ( M ^m _om ) | ( -. ( a ` i ) E ( a ` j ) \/ -. ( a ` k ) E ( a ` l ) ) } ) \/ E. n e. _om ( x = A.g n ( i e.g j ) /\ y = { a e. ( M ^m _om ) | A. z e. M if- ( i = n , if- ( j = n , z E z , z E ( a ` j ) ) , if- ( j = n , ( a ` i ) E z , ( a ` i ) E ( a ` j ) ) ) } ) ) } ) )
182 4 7 181 3eqtrd 
 |-  ( ( M e. V /\ E e. W ) -> ( S ` 1o ) = ( ( S ` (/) ) u. { <. x , y >. | E. i e. _om E. j e. _om ( E. k e. _om E. l e. _om ( x = ( ( i e.g j ) |g ( k e.g l ) ) /\ y = { a e. ( M ^m _om ) | ( -. ( a ` i ) E ( a ` j ) \/ -. ( a ` k ) E ( a ` l ) ) } ) \/ E. n e. _om ( x = A.g n ( i e.g j ) /\ y = { a e. ( M ^m _om ) | A. z e. M if- ( i = n , if- ( j = n , z E z , z E ( a ` j ) ) , if- ( j = n , ( a ` i ) E z , ( a ` i ) E ( a ` j ) ) ) } ) ) } ) )