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

Metamath Proof Explorer

Theorem satfv1fvfmla1

Description: The value of the satisfaction predicate at two Godel-sets of membership combined with a Godel-set for NAND. (Contributed by AV, 17-Nov-2023)

Ref Expression
Hypothesis satfv1fvfmla1.x 
|- X = ( ( I e.g J ) |g ( K e.g L ) )
Assertion satfv1fvfmla1 
|- ( ( ( M e. V /\ E e. W ) /\ ( I e. _om /\ J e. _om ) /\ ( K e. _om /\ L e. _om ) ) -> ( ( ( M Sat E ) ` 1o ) ` X ) = { a e. ( M ^m _om ) | ( -. ( a ` I ) E ( a ` J ) \/ -. ( a ` K ) E ( a ` L ) ) } )

Proof

Step Hyp Ref Expression
1 satfv1fvfmla1.x 
 |-  X = ( ( I e.g J ) |g ( K e.g L ) )
2 simpl 
 |-  ( ( M e. V /\ E e. W ) -> M e. V )
3 simpr 
 |-  ( ( M e. V /\ E e. W ) -> E e. W )
4 1onn 
 |-  1o e. _om
5 4 a1i 
 |-  ( ( M e. V /\ E e. W ) -> 1o e. _om )
6 2 3 5 3jca 
 |-  ( ( M e. V /\ E e. W ) -> ( M e. V /\ E e. W /\ 1o e. _om ) )
7 6 3ad2ant1 
 |-  ( ( ( M e. V /\ E e. W ) /\ ( I e. _om /\ J e. _om ) /\ ( K e. _om /\ L e. _om ) ) -> ( M e. V /\ E e. W /\ 1o e. _om ) )
8 satffun 
 |-  ( ( M e. V /\ E e. W /\ 1o e. _om ) -> Fun ( ( M Sat E ) ` 1o ) )
9 7 8 syl 
 |-  ( ( ( M e. V /\ E e. W ) /\ ( I e. _om /\ J e. _om ) /\ ( K e. _om /\ L e. _om ) ) -> Fun ( ( M Sat E ) ` 1o ) )
10 simp2l 
 |-  ( ( ( M e. V /\ E e. W ) /\ ( I e. _om /\ J e. _om ) /\ ( K e. _om /\ L e. _om ) ) -> I e. _om )
11 simp2r 
 |-  ( ( ( M e. V /\ E e. W ) /\ ( I e. _om /\ J e. _om ) /\ ( K e. _om /\ L e. _om ) ) -> J e. _om )
12 simp3l 
 |-  ( ( ( M e. V /\ E e. W ) /\ ( I e. _om /\ J e. _om ) /\ ( K e. _om /\ L e. _om ) ) -> K e. _om )
13 simp3r 
 |-  ( ( ( M e. V /\ E e. W ) /\ ( I e. _om /\ J e. _om ) /\ ( K e. _om /\ L e. _om ) ) -> L e. _om )
14 eqid 
 |-  { 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 ) ) }
15 1 14 pm3.2i 
 |-  ( X = ( ( I e.g J ) |g ( K e.g L ) ) /\ { 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 ) ) } )
16 15 a1i 
 |-  ( ( ( M e. V /\ E e. W ) /\ ( I e. _om /\ J e. _om ) /\ ( K e. _om /\ L e. _om ) ) -> ( X = ( ( I e.g J ) |g ( K e.g L ) ) /\ { 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 ) ) } ) )
17 oveq1 
 |-  ( k = K -> ( k e.g l ) = ( K e.g l ) )
18 17 oveq2d 
 |-  ( k = K -> ( ( I e.g J ) |g ( k e.g l ) ) = ( ( I e.g J ) |g ( K e.g l ) ) )
19 18 eqeq2d 
 |-  ( k = K -> ( X = ( ( I e.g J ) |g ( k e.g l ) ) <-> X = ( ( I e.g J ) |g ( K e.g l ) ) ) )
20 fveq2 
 |-  ( k = K -> ( a ` k ) = ( a ` K ) )
21 20 breq1d 
 |-  ( k = K -> ( ( a ` k ) E ( a ` l ) <-> ( a ` K ) E ( a ` l ) ) )
22 21 notbid 
 |-  ( k = K -> ( -. ( a ` k ) E ( a ` l ) <-> -. ( a ` K ) E ( a ` l ) ) )
23 22 orbi2d 
 |-  ( k = K -> ( ( -. ( a ` I ) E ( a ` J ) \/ -. ( a ` k ) E ( a ` l ) ) <-> ( -. ( a ` I ) E ( a ` J ) \/ -. ( a ` K ) E ( a ` l ) ) ) )
24 23 rabbidv 
 |-  ( k = K -> { 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 ) ) } )
25 24 eqeq2d 
 |-  ( k = K -> ( { 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 ) ) } <-> { 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 ) ) } ) )
26 19 25 anbi12d 
 |-  ( k = K -> ( ( X = ( ( I e.g J ) |g ( k e.g l ) ) /\ { 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 ) ) } ) <-> ( X = ( ( I e.g J ) |g ( K e.g l ) ) /\ { 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 ) ) } ) ) )
27 oveq2 
 |-  ( l = L -> ( K e.g l ) = ( K e.g L ) )
28 27 oveq2d 
 |-  ( l = L -> ( ( I e.g J ) |g ( K e.g l ) ) = ( ( I e.g J ) |g ( K e.g L ) ) )
29 28 eqeq2d 
 |-  ( l = L -> ( X = ( ( I e.g J ) |g ( K e.g l ) ) <-> X = ( ( I e.g J ) |g ( K e.g L ) ) ) )
30 fveq2 
 |-  ( l = L -> ( a ` l ) = ( a ` L ) )
31 30 breq2d 
 |-  ( l = L -> ( ( a ` K ) E ( a ` l ) <-> ( a ` K ) E ( a ` L ) ) )
32 31 notbid 
 |-  ( l = L -> ( -. ( a ` K ) E ( a ` l ) <-> -. ( a ` K ) E ( a ` L ) ) )
33 32 orbi2d 
 |-  ( l = L -> ( ( -. ( a ` I ) E ( a ` J ) \/ -. ( a ` K ) E ( a ` l ) ) <-> ( -. ( a ` I ) E ( a ` J ) \/ -. ( a ` K ) E ( a ` L ) ) ) )
34 33 rabbidv 
 |-  ( l = L -> { 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 ) ) } )
35 34 eqeq2d 
 |-  ( l = L -> ( { 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 ) ) } <-> { 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 ) ) } ) )
36 29 35 anbi12d 
 |-  ( l = L -> ( ( X = ( ( I e.g J ) |g ( K e.g l ) ) /\ { 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 ) ) } ) <-> ( X = ( ( I e.g J ) |g ( K e.g L ) ) /\ { 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 ) ) } ) ) )
37 26 36 rspc2ev 
 |-  ( ( K e. _om /\ L e. _om /\ ( X = ( ( I e.g J ) |g ( K e.g L ) ) /\ { 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 ) ) } ) ) -> E. k e. _om E. l e. _om ( X = ( ( I e.g J ) |g ( k e.g l ) ) /\ { 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 ) ) } ) )
38 12 13 16 37 syl3anc 
 |-  ( ( ( M e. V /\ E e. W ) /\ ( I e. _om /\ J e. _om ) /\ ( K e. _om /\ L e. _om ) ) -> E. k e. _om E. l e. _om ( X = ( ( I e.g J ) |g ( k e.g l ) ) /\ { 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 ) ) } ) )
39 38 orcd 
 |-  ( ( ( M e. V /\ E e. W ) /\ ( I e. _om /\ J e. _om ) /\ ( K e. _om /\ L e. _om ) ) -> ( E. k e. _om E. l e. _om ( X = ( ( I e.g J ) |g ( k e.g l ) ) /\ { 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 ) ) } ) \/ E. n e. _om ( X = A.g n ( I e.g J ) /\ { a e. ( M ^m _om ) | ( -. ( a ` I ) E ( a ` J ) \/ -. ( a ` K ) E ( a ` L ) ) } = { 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 ) ) ) } ) ) )
40 oveq1 
 |-  ( i = I -> ( i e.g j ) = ( I e.g j ) )
41 40 oveq1d 
 |-  ( i = I -> ( ( i e.g j ) |g ( k e.g l ) ) = ( ( I e.g j ) |g ( k e.g l ) ) )
42 41 eqeq2d 
 |-  ( i = I -> ( X = ( ( i e.g j ) |g ( k e.g l ) ) <-> X = ( ( I e.g j ) |g ( k e.g l ) ) ) )
43 fveq2 
 |-  ( i = I -> ( a ` i ) = ( a ` I ) )
44 43 breq1d 
 |-  ( i = I -> ( ( a ` i ) E ( a ` j ) <-> ( a ` I ) E ( a ` j ) ) )
45 44 notbid 
 |-  ( i = I -> ( -. ( a ` i ) E ( a ` j ) <-> -. ( a ` I ) E ( a ` j ) ) )
46 45 orbi1d 
 |-  ( i = I -> ( ( -. ( a ` i ) E ( a ` j ) \/ -. ( a ` k ) E ( a ` l ) ) <-> ( -. ( a ` I ) E ( a ` j ) \/ -. ( a ` k ) E ( a ` l ) ) ) )
47 46 rabbidv 
 |-  ( i = I -> { 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 ) ) } )
48 47 eqeq2d 
 |-  ( i = I -> ( { 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 ) ) } <-> { 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 ) ) } ) )
49 42 48 anbi12d 
 |-  ( i = I -> ( ( X = ( ( i e.g j ) |g ( k e.g l ) ) /\ { 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 ) ) } ) <-> ( X = ( ( I e.g j ) |g ( k e.g l ) ) /\ { 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 ) ) } ) ) )
50 49 2rexbidv 
 |-  ( i = I -> ( E. k e. _om E. l e. _om ( X = ( ( i e.g j ) |g ( k e.g l ) ) /\ { 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 ) ) } ) <-> E. k e. _om E. l e. _om ( X = ( ( I e.g j ) |g ( k e.g l ) ) /\ { 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 ) ) } ) ) )
51 eqidd 
 |-  ( i = I -> n = n )
52 51 40 goaleq12d 
 |-  ( i = I -> A.g n ( i e.g j ) = A.g n ( I e.g j ) )
53 52 eqeq2d 
 |-  ( i = I -> ( X = A.g n ( i e.g j ) <-> X = A.g n ( I e.g j ) ) )
54 eqeq1 
 |-  ( i = I -> ( i = n <-> I = n ) )
55 biidd 
 |-  ( i = I -> ( if- ( j = n , z E z , z E ( a ` j ) ) <-> if- ( j = n , z E z , z E ( a ` j ) ) ) )
56 43 breq1d 
 |-  ( i = I -> ( ( a ` i ) E z <-> ( a ` I ) E z ) )
57 56 44 ifpbi23d 
 |-  ( i = I -> ( if- ( j = n , ( a ` i ) E z , ( a ` i ) E ( a ` j ) ) <-> if- ( j = n , ( a ` I ) E z , ( a ` I ) E ( a ` j ) ) ) )
58 54 55 57 ifpbi123d 
 |-  ( i = I -> ( 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 ) ) ) <-> 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 ) ) ) ) )
59 58 ralbidv 
 |-  ( i = I -> ( 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. 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 ) ) ) ) )
60 59 rabbidv 
 |-  ( i = I -> { 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 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 ) ) ) } )
61 60 eqeq2d 
 |-  ( i = I -> ( { a e. ( M ^m _om ) | ( -. ( a ` I ) E ( a ` J ) \/ -. ( a ` K ) E ( a ` L ) ) } = { 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 ` I ) E ( a ` J ) \/ -. ( a ` K ) E ( a ` L ) ) } = { 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 ) ) ) } ) )
62 53 61 anbi12d 
 |-  ( i = I -> ( ( X = A.g n ( i e.g j ) /\ { a e. ( M ^m _om ) | ( -. ( a ` I ) E ( a ` J ) \/ -. ( a ` K ) E ( a ` L ) ) } = { 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 ) /\ { a e. ( M ^m _om ) | ( -. ( a ` I ) E ( a ` J ) \/ -. ( a ` K ) E ( a ` L ) ) } = { 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 ) ) ) } ) ) )
63 62 rexbidv 
 |-  ( i = I -> ( E. n e. _om ( X = A.g n ( i e.g j ) /\ { a e. ( M ^m _om ) | ( -. ( a ` I ) E ( a ` J ) \/ -. ( a ` K ) E ( a ` L ) ) } = { 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 ) /\ { a e. ( M ^m _om ) | ( -. ( a ` I ) E ( a ` J ) \/ -. ( a ` K ) E ( a ` L ) ) } = { 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 ) ) ) } ) ) )
64 50 63 orbi12d 
 |-  ( i = I -> ( ( E. k e. _om E. l e. _om ( X = ( ( i e.g j ) |g ( k e.g l ) ) /\ { 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 ) ) } ) \/ E. n e. _om ( X = A.g n ( i e.g j ) /\ { a e. ( M ^m _om ) | ( -. ( a ` I ) E ( a ` J ) \/ -. ( a ` K ) E ( a ` L ) ) } = { 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. k e. _om E. l e. _om ( X = ( ( I e.g j ) |g ( k e.g l ) ) /\ { 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 ) ) } ) \/ E. n e. _om ( X = A.g n ( I e.g j ) /\ { a e. ( M ^m _om ) | ( -. ( a ` I ) E ( a ` J ) \/ -. ( a ` K ) E ( a ` L ) ) } = { 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 ) ) ) } ) ) ) )
65 oveq2 
 |-  ( j = J -> ( I e.g j ) = ( I e.g J ) )
66 65 oveq1d 
 |-  ( j = J -> ( ( I e.g j ) |g ( k e.g l ) ) = ( ( I e.g J ) |g ( k e.g l ) ) )
67 66 eqeq2d 
 |-  ( j = J -> ( X = ( ( I e.g j ) |g ( k e.g l ) ) <-> X = ( ( I e.g J ) |g ( k e.g l ) ) ) )
68 fveq2 
 |-  ( j = J -> ( a ` j ) = ( a ` J ) )
69 68 breq2d 
 |-  ( j = J -> ( ( a ` I ) E ( a ` j ) <-> ( a ` I ) E ( a ` J ) ) )
70 69 notbid 
 |-  ( j = J -> ( -. ( a ` I ) E ( a ` j ) <-> -. ( a ` I ) E ( a ` J ) ) )
71 70 orbi1d 
 |-  ( j = J -> ( ( -. ( a ` I ) E ( a ` j ) \/ -. ( a ` k ) E ( a ` l ) ) <-> ( -. ( a ` I ) E ( a ` J ) \/ -. ( a ` k ) E ( a ` l ) ) ) )
72 71 rabbidv 
 |-  ( j = J -> { 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 ) ) } )
73 72 eqeq2d 
 |-  ( j = J -> ( { 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 ) ) } <-> { 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 ) ) } ) )
74 67 73 anbi12d 
 |-  ( j = J -> ( ( X = ( ( I e.g j ) |g ( k e.g l ) ) /\ { 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 ) ) } ) <-> ( X = ( ( I e.g J ) |g ( k e.g l ) ) /\ { 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 ) ) } ) ) )
75 74 2rexbidv 
 |-  ( j = J -> ( E. k e. _om E. l e. _om ( X = ( ( I e.g j ) |g ( k e.g l ) ) /\ { 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 ) ) } ) <-> E. k e. _om E. l e. _om ( X = ( ( I e.g J ) |g ( k e.g l ) ) /\ { 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 ) ) } ) ) )
76 eqidd 
 |-  ( j = J -> n = n )
77 76 65 goaleq12d 
 |-  ( j = J -> A.g n ( I e.g j ) = A.g n ( I e.g J ) )
78 77 eqeq2d 
 |-  ( j = J -> ( X = A.g n ( I e.g j ) <-> X = A.g n ( I e.g J ) ) )
79 eqeq1 
 |-  ( j = J -> ( j = n <-> J = n ) )
80 biidd 
 |-  ( j = J -> ( z E z <-> z E z ) )
81 68 breq2d 
 |-  ( j = J -> ( z E ( a ` j ) <-> z E ( a ` J ) ) )
82 79 80 81 ifpbi123d 
 |-  ( j = J -> ( if- ( j = n , z E z , z E ( a ` j ) ) <-> if- ( J = n , z E z , z E ( a ` J ) ) ) )
83 biidd 
 |-  ( j = J -> ( ( a ` I ) E z <-> ( a ` I ) E z ) )
84 79 83 69 ifpbi123d 
 |-  ( j = J -> ( if- ( j = n , ( a ` I ) E z , ( a ` I ) E ( a ` j ) ) <-> if- ( J = n , ( a ` I ) E z , ( a ` I ) E ( a ` J ) ) ) )
85 82 84 ifpbi23d 
 |-  ( j = J -> ( 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 ) ) ) <-> 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 ) ) ) ) )
86 85 ralbidv 
 |-  ( j = J -> ( 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. 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 ) ) ) ) )
87 86 rabbidv 
 |-  ( j = 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 ) ) ) } = { 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 ) ) ) } )
88 87 eqeq2d 
 |-  ( j = J -> ( { a e. ( M ^m _om ) | ( -. ( a ` I ) E ( a ` J ) \/ -. ( a ` K ) E ( a ` L ) ) } = { 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 ` I ) E ( a ` J ) \/ -. ( a ` K ) E ( a ` L ) ) } = { 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 ) ) ) } ) )
89 78 88 anbi12d 
 |-  ( j = J -> ( ( X = A.g n ( I e.g j ) /\ { a e. ( M ^m _om ) | ( -. ( a ` I ) E ( a ` J ) \/ -. ( a ` K ) E ( a ` L ) ) } = { 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 ) /\ { a e. ( M ^m _om ) | ( -. ( a ` I ) E ( a ` J ) \/ -. ( a ` K ) E ( a ` L ) ) } = { 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 ) ) ) } ) ) )
90 89 rexbidv 
 |-  ( j = J -> ( E. n e. _om ( X = A.g n ( I e.g j ) /\ { a e. ( M ^m _om ) | ( -. ( a ` I ) E ( a ` J ) \/ -. ( a ` K ) E ( a ` L ) ) } = { 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 ) /\ { a e. ( M ^m _om ) | ( -. ( a ` I ) E ( a ` J ) \/ -. ( a ` K ) E ( a ` L ) ) } = { 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 ) ) ) } ) ) )
91 75 90 orbi12d 
 |-  ( j = J -> ( ( E. k e. _om E. l e. _om ( X = ( ( I e.g j ) |g ( k e.g l ) ) /\ { 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 ) ) } ) \/ E. n e. _om ( X = A.g n ( I e.g j ) /\ { a e. ( M ^m _om ) | ( -. ( a ` I ) E ( a ` J ) \/ -. ( a ` K ) E ( a ` L ) ) } = { 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. k e. _om E. l e. _om ( X = ( ( I e.g J ) |g ( k e.g l ) ) /\ { 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 ) ) } ) \/ E. n e. _om ( X = A.g n ( I e.g J ) /\ { a e. ( M ^m _om ) | ( -. ( a ` I ) E ( a ` J ) \/ -. ( a ` K ) E ( a ` L ) ) } = { 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 ) ) ) } ) ) ) )
92 64 91 rspc2ev 
 |-  ( ( I e. _om /\ J e. _om /\ ( E. k e. _om E. l e. _om ( X = ( ( I e.g J ) |g ( k e.g l ) ) /\ { 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 ) ) } ) \/ E. n e. _om ( X = A.g n ( I e.g J ) /\ { a e. ( M ^m _om ) | ( -. ( a ` I ) E ( a ` J ) \/ -. ( a ` K ) E ( a ` L ) ) } = { 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. k e. _om E. l e. _om ( X = ( ( i e.g j ) |g ( k e.g l ) ) /\ { 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 ) ) } ) \/ E. n e. _om ( X = A.g n ( i e.g j ) /\ { a e. ( M ^m _om ) | ( -. ( a ` I ) E ( a ` J ) \/ -. ( a ` K ) E ( a ` L ) ) } = { 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 ) ) ) } ) ) )
93 10 11 39 92 syl3anc 
 |-  ( ( ( M e. V /\ E e. W ) /\ ( I e. _om /\ J e. _om ) /\ ( K e. _om /\ L e. _om ) ) -> 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 ) ) /\ { 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 ) ) } ) \/ E. n e. _om ( X = A.g n ( i e.g j ) /\ { a e. ( M ^m _om ) | ( -. ( a ` I ) E ( a ` J ) \/ -. ( a ` K ) E ( a ` L ) ) } = { 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 ) ) ) } ) ) )
94 1 ovexi 
 |-  X e. _V
95 94 a1i 
 |-  ( ( ( M e. V /\ E e. W ) /\ ( I e. _om /\ J e. _om ) /\ ( K e. _om /\ L e. _om ) ) -> X e. _V )
96 ovex 
 |-  ( M ^m _om ) e. _V
97 96 rabex 
 |-  { a e. ( M ^m _om ) | ( -. ( a ` I ) E ( a ` J ) \/ -. ( a ` K ) E ( a ` L ) ) } e. _V
98 eqeq1 
 |-  ( x = X -> ( x = ( ( i e.g j ) |g ( k e.g l ) ) <-> X = ( ( i e.g j ) |g ( k e.g l ) ) ) )
99 eqeq1 
 |-  ( y = { a e. ( M ^m _om ) | ( -. ( a ` I ) E ( a ` J ) \/ -. ( a ` K ) E ( a ` L ) ) } -> ( y = { 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 ) ) } = { a e. ( M ^m _om ) | ( -. ( a ` i ) E ( a ` j ) \/ -. ( a ` k ) E ( a ` l ) ) } ) )
100 98 99 bi2anan9 
 |-  ( ( x = X /\ 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 = { 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 ) ) /\ { 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 ) ) } ) ) )
101 100 2rexbidv 
 |-  ( ( x = X /\ y = { a e. ( M ^m _om ) | ( -. ( a ` I ) E ( a ` J ) \/ -. ( a ` K ) E ( a ` L ) ) } ) -> ( 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 ( X = ( ( i e.g j ) |g ( k e.g l ) ) /\ { 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 ) ) } ) ) )
102 eqeq1 
 |-  ( x = X -> ( x = A.g n ( i e.g j ) <-> X = A.g n ( i e.g j ) ) )
103 eqeq1 
 |-  ( y = { a e. ( M ^m _om ) | ( -. ( a ` I ) E ( a ` J ) \/ -. ( a ` K ) E ( a ` L ) ) } -> ( 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 ) ) ) } <-> { a e. ( M ^m _om ) | ( -. ( a ` I ) E ( a ` J ) \/ -. ( a ` K ) E ( a ` L ) ) } = { 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 ) ) ) } ) )
104 102 103 bi2anan9 
 |-  ( ( x = X /\ y = { a e. ( M ^m _om ) | ( -. ( a ` I ) E ( a ` J ) \/ -. ( a ` K ) E ( a ` L ) ) } ) -> ( ( 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 ) /\ { a e. ( M ^m _om ) | ( -. ( a ` I ) E ( a ` J ) \/ -. ( a ` K ) E ( a ` L ) ) } = { 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 ) ) ) } ) ) )
105 104 rexbidv 
 |-  ( ( x = X /\ 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. n e. _om ( X = A.g n ( i e.g j ) /\ { a e. ( M ^m _om ) | ( -. ( a ` I ) E ( a ` J ) \/ -. ( a ` K ) E ( a ` L ) ) } = { 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 ) ) ) } ) ) )
106 101 105 orbi12d 
 |-  ( ( x = X /\ y = { a e. ( M ^m _om ) | ( -. ( a ` I ) E ( a ` J ) \/ -. ( a ` K ) E ( a ` L ) ) } ) -> ( ( 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. k e. _om E. l e. _om ( X = ( ( i e.g j ) |g ( k e.g l ) ) /\ { 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 ) ) } ) \/ E. n e. _om ( X = A.g n ( i e.g j ) /\ { a e. ( M ^m _om ) | ( -. ( a ` I ) E ( a ` J ) \/ -. ( a ` K ) E ( a ` L ) ) } = { 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 ) ) ) } ) ) ) )
107 106 2rexbidv 
 |-  ( ( x = X /\ y = { a e. ( M ^m _om ) | ( -. ( a ` I ) E ( a ` J ) \/ -. ( a ` K ) E ( a ` L ) ) } ) -> ( 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. k e. _om E. l e. _om ( X = ( ( i e.g j ) |g ( k e.g l ) ) /\ { 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 ) ) } ) \/ E. n e. _om ( X = A.g n ( i e.g j ) /\ { a e. ( M ^m _om ) | ( -. ( a ` I ) E ( a ` J ) \/ -. ( a ` K ) E ( a ` L ) ) } = { 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 107 opelopabga 
 |-  ( ( X e. _V /\ { a e. ( M ^m _om ) | ( -. ( a ` I ) E ( a ` J ) \/ -. ( a ` K ) E ( a ` L ) ) } e. _V ) -> ( <. X , { a e. ( M ^m _om ) | ( -. ( a ` I ) E ( a ` J ) \/ -. ( a ` K ) E ( a ` L ) ) } >. e. { <. 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 ) ) ) } ) ) } <-> 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 ) ) /\ { 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 ) ) } ) \/ E. n e. _om ( X = A.g n ( i e.g j ) /\ { a e. ( M ^m _om ) | ( -. ( a ` I ) E ( a ` J ) \/ -. ( a ` K ) E ( a ` L ) ) } = { 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 95 97 108 sylancl 
 |-  ( ( ( M e. V /\ E e. W ) /\ ( I e. _om /\ J e. _om ) /\ ( K e. _om /\ L e. _om ) ) -> ( <. X , { a e. ( M ^m _om ) | ( -. ( a ` I ) E ( a ` J ) \/ -. ( a ` K ) E ( a ` L ) ) } >. e. { <. 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 ) ) ) } ) ) } <-> 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 ) ) /\ { 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 ) ) } ) \/ E. n e. _om ( X = A.g n ( i e.g j ) /\ { a e. ( M ^m _om ) | ( -. ( a ` I ) E ( a ` J ) \/ -. ( a ` K ) E ( a ` L ) ) } = { 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 93 109 mpbird 
 |-  ( ( ( M e. V /\ E e. W ) /\ ( I e. _om /\ J e. _om ) /\ ( K e. _om /\ L e. _om ) ) -> <. X , { a e. ( M ^m _om ) | ( -. ( a ` I ) E ( a ` J ) \/ -. ( a ` K ) E ( a ` L ) ) } >. e. { <. 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 ) ) ) } ) ) } )
111 110 olcd 
 |-  ( ( ( M e. V /\ E e. W ) /\ ( I e. _om /\ J e. _om ) /\ ( K e. _om /\ L e. _om ) ) -> ( <. X , { a e. ( M ^m _om ) | ( -. ( a ` I ) E ( a ` J ) \/ -. ( a ` K ) E ( a ` L ) ) } >. e. ( ( M Sat E ) ` (/) ) \/ <. X , { a e. ( M ^m _om ) | ( -. ( a ` I ) E ( a ` J ) \/ -. ( a ` K ) E ( a ` L ) ) } >. e. { <. 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 ) ) ) } ) ) } ) )
112 elun 
 |-  ( <. X , { a e. ( M ^m _om ) | ( -. ( a ` I ) E ( a ` J ) \/ -. ( a ` K ) E ( a ` L ) ) } >. e. ( ( ( M Sat E ) ` (/) ) 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 ) ) ) } ) ) } ) <-> ( <. X , { a e. ( M ^m _om ) | ( -. ( a ` I ) E ( a ` J ) \/ -. ( a ` K ) E ( a ` L ) ) } >. e. ( ( M Sat E ) ` (/) ) \/ <. X , { a e. ( M ^m _om ) | ( -. ( a ` I ) E ( a ` J ) \/ -. ( a ` K ) E ( a ` L ) ) } >. e. { <. 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 ) ) ) } ) ) } ) )
113 111 112 sylibr 
 |-  ( ( ( M e. V /\ E e. W ) /\ ( I e. _om /\ J e. _om ) /\ ( K e. _om /\ L e. _om ) ) -> <. X , { a e. ( M ^m _om ) | ( -. ( a ` I ) E ( a ` J ) \/ -. ( a ` K ) E ( a ` L ) ) } >. e. ( ( ( M Sat E ) ` (/) ) 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 ) ) ) } ) ) } ) )
114 eqid 
 |-  ( M Sat E ) = ( M Sat E )
115 114 satfv1 
 |-  ( ( M e. V /\ E e. W ) -> ( ( M Sat E ) ` 1o ) = ( ( ( M Sat E ) ` (/) ) 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 ) ) ) } ) ) } ) )
116 115 eleq2d 
 |-  ( ( M e. V /\ E e. W ) -> ( <. X , { a e. ( M ^m _om ) | ( -. ( a ` I ) E ( a ` J ) \/ -. ( a ` K ) E ( a ` L ) ) } >. e. ( ( M Sat E ) ` 1o ) <-> <. X , { a e. ( M ^m _om ) | ( -. ( a ` I ) E ( a ` J ) \/ -. ( a ` K ) E ( a ` L ) ) } >. e. ( ( ( M Sat E ) ` (/) ) 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 ) ) ) } ) ) } ) ) )
117 116 3ad2ant1 
 |-  ( ( ( M e. V /\ E e. W ) /\ ( I e. _om /\ J e. _om ) /\ ( K e. _om /\ L e. _om ) ) -> ( <. X , { a e. ( M ^m _om ) | ( -. ( a ` I ) E ( a ` J ) \/ -. ( a ` K ) E ( a ` L ) ) } >. e. ( ( M Sat E ) ` 1o ) <-> <. X , { a e. ( M ^m _om ) | ( -. ( a ` I ) E ( a ` J ) \/ -. ( a ` K ) E ( a ` L ) ) } >. e. ( ( ( M Sat E ) ` (/) ) 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 ) ) ) } ) ) } ) ) )
118 113 117 mpbird 
 |-  ( ( ( M e. V /\ E e. W ) /\ ( I e. _om /\ J e. _om ) /\ ( K e. _om /\ L e. _om ) ) -> <. X , { a e. ( M ^m _om ) | ( -. ( a ` I ) E ( a ` J ) \/ -. ( a ` K ) E ( a ` L ) ) } >. e. ( ( M Sat E ) ` 1o ) )
119 funopfv 
 |-  ( Fun ( ( M Sat E ) ` 1o ) -> ( <. X , { a e. ( M ^m _om ) | ( -. ( a ` I ) E ( a ` J ) \/ -. ( a ` K ) E ( a ` L ) ) } >. e. ( ( M Sat E ) ` 1o ) -> ( ( ( M Sat E ) ` 1o ) ` X ) = { a e. ( M ^m _om ) | ( -. ( a ` I ) E ( a ` J ) \/ -. ( a ` K ) E ( a ` L ) ) } ) )
120 9 118 119 sylc 
 |-  ( ( ( M e. V /\ E e. W ) /\ ( I e. _om /\ J e. _om ) /\ ( K e. _om /\ L e. _om ) ) -> ( ( ( M Sat E ) ` 1o ) ` X ) = { a e. ( M ^m _om ) | ( -. ( a ` I ) E ( a ` J ) \/ -. ( a ` K ) E ( a ` L ) ) } )