Metamath Proof Explorer

Theorem satfvsucsuc

Description: The satisfaction predicate as function over wff codes of height ( N + 1 ) , expressed by the minimally necessary satisfaction predicates as function over wff codes of height N . (Contributed by AV, 21-Oct-2023)

Ref Expression
Hypotheses satfvsucsuc.s 
|- S = ( M Sat E )
satfvsucsuc.a 
|- A = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) )
satfvsucsuc.b 
|- B = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) }
Assertion satfvsucsuc 
|- ( ( M e. V /\ E e. W /\ N e. _om ) -> ( S ` suc suc N ) = ( ( S ` suc N ) u. { <. x , y >. | ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) } ) )

Proof

Step Hyp Ref Expression
1 satfvsucsuc.s 
 |-  S = ( M Sat E )
2 satfvsucsuc.a 
 |-  A = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) )
3 satfvsucsuc.b 
 |-  B = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) }
4 peano2 
 |-  ( N e. _om -> suc N e. _om )
5 1 satfvsuc 
 |-  ( ( M e. V /\ E e. W /\ suc N e. _om ) -> ( S ` suc suc N ) = ( ( S ` suc N ) u. { <. x , y >. | E. u e. ( S ` suc N ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) )
6 4 5 syl3an3 
 |-  ( ( M e. V /\ E e. W /\ N e. _om ) -> ( S ` suc suc N ) = ( ( S ` suc N ) u. { <. x , y >. | E. u e. ( S ` suc N ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) )
7 orc 
 |-  ( s e. ( S ` suc N ) -> ( s e. ( S ` suc N ) \/ E. x E. y ( s = <. x , y >. /\ ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) ) ) )
8 7 a1i 
 |-  ( ( M e. V /\ E e. W /\ N e. _om ) -> ( s e. ( S ` suc N ) -> ( s e. ( S ` suc N ) \/ E. x E. y ( s = <. x , y >. /\ ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) ) ) ) )
9 2 eqeq2i 
 |-  ( y = A <-> y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) )
10 9 anbi2i 
 |-  ( ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) <-> ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) )
11 10 rexbii 
 |-  ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) <-> E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) )
12 3 eqeq2i 
 |-  ( y = B <-> y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } )
13 12 anbi2i 
 |-  ( ( x = A.g i ( 1st ` u ) /\ y = B ) <-> ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) )
14 13 rexbii 
 |-  ( E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) <-> E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) )
15 11 14 orbi12i 
 |-  ( ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) <-> ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) )
16 15 rexbii 
 |-  ( E. u e. ( S ` suc N ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) <-> E. u e. ( S ` suc N ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) )
17 16 bicomi 
 |-  ( E. u e. ( S ` suc N ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) <-> E. u e. ( S ` suc N ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) )
18 3simpa 
 |-  ( ( M e. V /\ E e. W /\ N e. _om ) -> ( M e. V /\ E e. W ) )
19 4 ancri 
 |-  ( N e. _om -> ( suc N e. _om /\ N e. _om ) )
20 19 3ad2ant3 
 |-  ( ( M e. V /\ E e. W /\ N e. _om ) -> ( suc N e. _om /\ N e. _om ) )
21 18 20 jca 
 |-  ( ( M e. V /\ E e. W /\ N e. _om ) -> ( ( M e. V /\ E e. W ) /\ ( suc N e. _om /\ N e. _om ) ) )
22 sssucid 
 |-  N C_ suc N
23 22 a1i 
 |-  ( ( ( M e. V /\ E e. W /\ N e. _om ) /\ s = <. x , y >. ) -> N C_ suc N )
24 1 satfsschain 
 |-  ( ( ( M e. V /\ E e. W ) /\ ( suc N e. _om /\ N e. _om ) ) -> ( N C_ suc N -> ( S ` N ) C_ ( S ` suc N ) ) )
25 24 imp 
 |-  ( ( ( ( M e. V /\ E e. W ) /\ ( suc N e. _om /\ N e. _om ) ) /\ N C_ suc N ) -> ( S ` N ) C_ ( S ` suc N ) )
26 21 23 25 syl2an2r 
 |-  ( ( ( M e. V /\ E e. W /\ N e. _om ) /\ s = <. x , y >. ) -> ( S ` N ) C_ ( S ` suc N ) )
27 undif 
 |-  ( ( S ` N ) C_ ( S ` suc N ) <-> ( ( S ` N ) u. ( ( S ` suc N ) \ ( S ` N ) ) ) = ( S ` suc N ) )
28 26 27 sylib 
 |-  ( ( ( M e. V /\ E e. W /\ N e. _om ) /\ s = <. x , y >. ) -> ( ( S ` N ) u. ( ( S ` suc N ) \ ( S ` N ) ) ) = ( S ` suc N ) )
29 28 eqcomd 
 |-  ( ( ( M e. V /\ E e. W /\ N e. _om ) /\ s = <. x , y >. ) -> ( S ` suc N ) = ( ( S ` N ) u. ( ( S ` suc N ) \ ( S ` N ) ) ) )
30 29 rexeqdv 
 |-  ( ( ( M e. V /\ E e. W /\ N e. _om ) /\ s = <. x , y >. ) -> ( E. u e. ( S ` suc N ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) <-> E. u e. ( ( S ` N ) u. ( ( S ` suc N ) \ ( S ` N ) ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) ) )
31 rexun 
 |-  ( E. u e. ( ( S ` N ) u. ( ( S ` suc N ) \ ( S ` N ) ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) <-> ( E. u e. ( S ` N ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) ) )
32 30 31 bitrdi 
 |-  ( ( ( M e. V /\ E e. W /\ N e. _om ) /\ s = <. x , y >. ) -> ( E. u e. ( S ` suc N ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) <-> ( E. u e. ( S ` N ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) ) ) )
33 17 32 bitrid 
 |-  ( ( ( M e. V /\ E e. W /\ N e. _om ) /\ s = <. x , y >. ) -> ( E. u e. ( S ` suc N ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) <-> ( E. u e. ( S ` N ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) ) ) )
34 r19.43 
 |-  ( E. u e. ( S ` N ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) <-> ( E. u e. ( S ` N ) E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. u e. ( S ` N ) E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) )
35 22 a1i 
 |-  ( ( M e. V /\ E e. W /\ N e. _om ) -> N C_ suc N )
36 21 35 jca 
 |-  ( ( M e. V /\ E e. W /\ N e. _om ) -> ( ( ( M e. V /\ E e. W ) /\ ( suc N e. _om /\ N e. _om ) ) /\ N C_ suc N ) )
37 36 25 syl 
 |-  ( ( M e. V /\ E e. W /\ N e. _om ) -> ( S ` N ) C_ ( S ` suc N ) )
38 37 adantr 
 |-  ( ( ( M e. V /\ E e. W /\ N e. _om ) /\ s = <. x , y >. ) -> ( S ` N ) C_ ( S ` suc N ) )
39 38 27 sylib 
 |-  ( ( ( M e. V /\ E e. W /\ N e. _om ) /\ s = <. x , y >. ) -> ( ( S ` N ) u. ( ( S ` suc N ) \ ( S ` N ) ) ) = ( S ` suc N ) )
40 39 eqcomd 
 |-  ( ( ( M e. V /\ E e. W /\ N e. _om ) /\ s = <. x , y >. ) -> ( S ` suc N ) = ( ( S ` N ) u. ( ( S ` suc N ) \ ( S ` N ) ) ) )
41 40 rexeqdv 
 |-  ( ( ( M e. V /\ E e. W /\ N e. _om ) /\ s = <. x , y >. ) -> ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) <-> E. v e. ( ( S ` N ) u. ( ( S ` suc N ) \ ( S ` N ) ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) )
42 rexun 
 |-  ( E. v e. ( ( S ` N ) u. ( ( S ` suc N ) \ ( S ` N ) ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) <-> ( E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) )
43 41 42 bitrdi 
 |-  ( ( ( M e. V /\ E e. W /\ N e. _om ) /\ s = <. x , y >. ) -> ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) <-> ( E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) ) )
44 43 rexbidv 
 |-  ( ( ( M e. V /\ E e. W /\ N e. _om ) /\ s = <. x , y >. ) -> ( E. u e. ( S ` N ) E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) <-> E. u e. ( S ` N ) ( E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) ) )
45 44 orbi1d 
 |-  ( ( ( M e. V /\ E e. W /\ N e. _om ) /\ s = <. x , y >. ) -> ( ( E. u e. ( S ` N ) E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. u e. ( S ` N ) E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) <-> ( E. u e. ( S ` N ) ( E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) \/ E. u e. ( S ` N ) E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) ) )
46 r19.43 
 |-  ( E. u e. ( S ` N ) ( E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) <-> ( E. u e. ( S ` N ) E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) )
47 46 orbi1i 
 |-  ( ( E. u e. ( S ` N ) ( E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) \/ E. u e. ( S ` N ) E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) <-> ( ( E. u e. ( S ` N ) E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) \/ E. u e. ( S ` N ) E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) )
48 or32 
 |-  ( ( ( E. u e. ( S ` N ) E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) \/ E. u e. ( S ` N ) E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) <-> ( ( E. u e. ( S ` N ) E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. u e. ( S ` N ) E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) )
49 r19.43 
 |-  ( E. u e. ( S ` N ) ( E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) <-> ( E. u e. ( S ` N ) E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. u e. ( S ` N ) E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) )
50 49 bicomi 
 |-  ( ( E. u e. ( S ` N ) E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. u e. ( S ` N ) E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) <-> E. u e. ( S ` N ) ( E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) )
51 50 orbi1i 
 |-  ( ( ( E. u e. ( S ` N ) E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. u e. ( S ` N ) E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) <-> ( E. u e. ( S ` N ) ( E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) )
52 48 51 bitri 
 |-  ( ( ( E. u e. ( S ` N ) E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) \/ E. u e. ( S ` N ) E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) <-> ( E. u e. ( S ` N ) ( E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) )
53 47 52 bitri 
 |-  ( ( E. u e. ( S ` N ) ( E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) \/ E. u e. ( S ` N ) E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) <-> ( E. u e. ( S ` N ) ( E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) )
54 45 53 bitrdi 
 |-  ( ( ( M e. V /\ E e. W /\ N e. _om ) /\ s = <. x , y >. ) -> ( ( E. u e. ( S ` N ) E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. u e. ( S ` N ) E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) <-> ( E. u e. ( S ` N ) ( E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) ) )
55 34 54 bitrid 
 |-  ( ( ( M e. V /\ E e. W /\ N e. _om ) /\ s = <. x , y >. ) -> ( E. u e. ( S ` N ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) <-> ( E. u e. ( S ` N ) ( E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) ) )
56 animorr 
 |-  ( ( ( ( M e. V /\ E e. W /\ N e. _om ) /\ s = <. x , y >. ) /\ E. u e. ( S ` N ) ( E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) ) -> ( <. x , y >. e. ( S ` N ) \/ E. u e. ( S ` N ) ( E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) ) )
57 1 satfvsuc 
 |-  ( ( M e. V /\ E e. W /\ N e. _om ) -> ( S ` suc N ) = ( ( S ` N ) u. { <. x , y >. | E. u e. ( S ` N ) ( E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) )
58 57 eleq2d 
 |-  ( ( M e. V /\ E e. W /\ N e. _om ) -> ( s e. ( S ` suc N ) <-> s e. ( ( S ` N ) u. { <. x , y >. | E. u e. ( S ` N ) ( E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) ) )
59 58 adantr 
 |-  ( ( ( M e. V /\ E e. W /\ N e. _om ) /\ s = <. x , y >. ) -> ( s e. ( S ` suc N ) <-> s e. ( ( S ` N ) u. { <. x , y >. | E. u e. ( S ` N ) ( E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) ) )
60 eleq1 
 |-  ( s = <. x , y >. -> ( s e. ( ( S ` N ) u. { <. x , y >. | E. u e. ( S ` N ) ( E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) <-> <. x , y >. e. ( ( S ` N ) u. { <. x , y >. | E. u e. ( S ` N ) ( E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) ) )
61 60 adantl 
 |-  ( ( ( M e. V /\ E e. W /\ N e. _om ) /\ s = <. x , y >. ) -> ( s e. ( ( S ` N ) u. { <. x , y >. | E. u e. ( S ` N ) ( E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) <-> <. x , y >. e. ( ( S ` N ) u. { <. x , y >. | E. u e. ( S ` N ) ( E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) ) )
62 elun 
 |-  ( <. x , y >. e. ( ( S ` N ) u. { <. x , y >. | E. u e. ( S ` N ) ( E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) <-> ( <. x , y >. e. ( S ` N ) \/ <. x , y >. e. { <. x , y >. | E. u e. ( S ` N ) ( E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) )
63 opabidw 
 |-  ( <. x , y >. e. { <. x , y >. | E. u e. ( S ` N ) ( E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } <-> E. u e. ( S ` N ) ( E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) )
64 63 orbi2i 
 |-  ( ( <. x , y >. e. ( S ` N ) \/ <. x , y >. e. { <. x , y >. | E. u e. ( S ` N ) ( E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) <-> ( <. x , y >. e. ( S ` N ) \/ E. u e. ( S ` N ) ( E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) ) )
65 62 64 bitri 
 |-  ( <. x , y >. e. ( ( S ` N ) u. { <. x , y >. | E. u e. ( S ` N ) ( E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) <-> ( <. x , y >. e. ( S ` N ) \/ E. u e. ( S ` N ) ( E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) ) )
66 61 65 bitrdi 
 |-  ( ( ( M e. V /\ E e. W /\ N e. _om ) /\ s = <. x , y >. ) -> ( s e. ( ( S ` N ) u. { <. x , y >. | E. u e. ( S ` N ) ( E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) <-> ( <. x , y >. e. ( S ` N ) \/ E. u e. ( S ` N ) ( E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) ) ) )
67 59 66 bitrd 
 |-  ( ( ( M e. V /\ E e. W /\ N e. _om ) /\ s = <. x , y >. ) -> ( s e. ( S ` suc N ) <-> ( <. x , y >. e. ( S ` N ) \/ E. u e. ( S ` N ) ( E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) ) ) )
68 2 eqcomi 
 |-  ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) = A
69 68 eqeq2i 
 |-  ( y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) <-> y = A )
70 69 anbi2i 
 |-  ( ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) <-> ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) )
71 70 rexbii 
 |-  ( E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) <-> E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) )
72 3 eqcomi 
 |-  { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } = B
73 72 eqeq2i 
 |-  ( y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } <-> y = B )
74 73 anbi2i 
 |-  ( ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) <-> ( x = A.g i ( 1st ` u ) /\ y = B ) )
75 74 rexbii 
 |-  ( E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) <-> E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) )
76 71 75 orbi12i 
 |-  ( ( E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) <-> ( E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) )
77 76 rexbii 
 |-  ( E. u e. ( S ` N ) ( E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) <-> E. u e. ( S ` N ) ( E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) )
78 77 a1i 
 |-  ( ( ( M e. V /\ E e. W /\ N e. _om ) /\ s = <. x , y >. ) -> ( E. u e. ( S ` N ) ( E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) <-> E. u e. ( S ` N ) ( E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) ) )
79 78 orbi2d 
 |-  ( ( ( M e. V /\ E e. W /\ N e. _om ) /\ s = <. x , y >. ) -> ( ( <. x , y >. e. ( S ` N ) \/ E. u e. ( S ` N ) ( E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) ) <-> ( <. x , y >. e. ( S ` N ) \/ E. u e. ( S ` N ) ( E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) ) ) )
80 67 79 bitrd 
 |-  ( ( ( M e. V /\ E e. W /\ N e. _om ) /\ s = <. x , y >. ) -> ( s e. ( S ` suc N ) <-> ( <. x , y >. e. ( S ` N ) \/ E. u e. ( S ` N ) ( E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) ) ) )
81 80 adantr 
 |-  ( ( ( ( M e. V /\ E e. W /\ N e. _om ) /\ s = <. x , y >. ) /\ E. u e. ( S ` N ) ( E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) ) -> ( s e. ( S ` suc N ) <-> ( <. x , y >. e. ( S ` N ) \/ E. u e. ( S ` N ) ( E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) ) ) )
82 56 81 mpbird 
 |-  ( ( ( ( M e. V /\ E e. W /\ N e. _om ) /\ s = <. x , y >. ) /\ E. u e. ( S ` N ) ( E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) ) -> s e. ( S ` suc N ) )
83 82 orcd 
 |-  ( ( ( ( M e. V /\ E e. W /\ N e. _om ) /\ s = <. x , y >. ) /\ E. u e. ( S ` N ) ( E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) ) -> ( s e. ( S ` suc N ) \/ ( s = <. x , y >. /\ ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) ) ) )
84 83 ex 
 |-  ( ( ( M e. V /\ E e. W /\ N e. _om ) /\ s = <. x , y >. ) -> ( E. u e. ( S ` N ) ( E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) -> ( s e. ( S ` suc N ) \/ ( s = <. x , y >. /\ ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) ) ) ) )
85 simplr 
 |-  ( ( ( ( M e. V /\ E e. W /\ N e. _om ) /\ s = <. x , y >. ) /\ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) -> s = <. x , y >. )
86 animorr 
 |-  ( ( ( ( M e. V /\ E e. W /\ N e. _om ) /\ s = <. x , y >. ) /\ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) -> ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) )
87 85 86 jca 
 |-  ( ( ( ( M e. V /\ E e. W /\ N e. _om ) /\ s = <. x , y >. ) /\ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) -> ( s = <. x , y >. /\ ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) ) )
88 87 olcd 
 |-  ( ( ( ( M e. V /\ E e. W /\ N e. _om ) /\ s = <. x , y >. ) /\ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) -> ( s e. ( S ` suc N ) \/ ( s = <. x , y >. /\ ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) ) ) )
89 88 ex 
 |-  ( ( ( M e. V /\ E e. W /\ N e. _om ) /\ s = <. x , y >. ) -> ( E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) -> ( s e. ( S ` suc N ) \/ ( s = <. x , y >. /\ ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) ) ) ) )
90 84 89 jaod 
 |-  ( ( ( M e. V /\ E e. W /\ N e. _om ) /\ s = <. x , y >. ) -> ( ( E. u e. ( S ` N ) ( E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) -> ( s e. ( S ` suc N ) \/ ( s = <. x , y >. /\ ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) ) ) ) )
91 55 90 sylbid 
 |-  ( ( ( M e. V /\ E e. W /\ N e. _om ) /\ s = <. x , y >. ) -> ( E. u e. ( S ` N ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) -> ( s e. ( S ` suc N ) \/ ( s = <. x , y >. /\ ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) ) ) ) )
92 simplr 
 |-  ( ( ( ( M e. V /\ E e. W /\ N e. _om ) /\ s = <. x , y >. ) /\ E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) ) -> s = <. x , y >. )
93 orc 
 |-  ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) -> ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) )
94 93 adantl 
 |-  ( ( ( ( M e. V /\ E e. W /\ N e. _om ) /\ s = <. x , y >. ) /\ E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) ) -> ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) )
95 92 94 jca 
 |-  ( ( ( ( M e. V /\ E e. W /\ N e. _om ) /\ s = <. x , y >. ) /\ E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) ) -> ( s = <. x , y >. /\ ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) ) )
96 95 olcd 
 |-  ( ( ( ( M e. V /\ E e. W /\ N e. _om ) /\ s = <. x , y >. ) /\ E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) ) -> ( s e. ( S ` suc N ) \/ ( s = <. x , y >. /\ ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) ) ) )
97 96 ex 
 |-  ( ( ( M e. V /\ E e. W /\ N e. _om ) /\ s = <. x , y >. ) -> ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) -> ( s e. ( S ` suc N ) \/ ( s = <. x , y >. /\ ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) ) ) ) )
98 91 97 jaod 
 |-  ( ( ( M e. V /\ E e. W /\ N e. _om ) /\ s = <. x , y >. ) -> ( ( E. u e. ( S ` N ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) ) -> ( s e. ( S ` suc N ) \/ ( s = <. x , y >. /\ ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) ) ) ) )
99 33 98 sylbid 
 |-  ( ( ( M e. V /\ E e. W /\ N e. _om ) /\ s = <. x , y >. ) -> ( E. u e. ( S ` suc N ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) -> ( s e. ( S ` suc N ) \/ ( s = <. x , y >. /\ ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) ) ) ) )
100 99 expimpd 
 |-  ( ( M e. V /\ E e. W /\ N e. _om ) -> ( ( s = <. x , y >. /\ E. u e. ( S ` suc N ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) ) -> ( s e. ( S ` suc N ) \/ ( s = <. x , y >. /\ ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) ) ) ) )
101 100 2eximdv 
 |-  ( ( M e. V /\ E e. W /\ N e. _om ) -> ( E. x E. y ( s = <. x , y >. /\ E. u e. ( S ` suc N ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) ) -> E. x E. y ( s e. ( S ` suc N ) \/ ( s = <. x , y >. /\ ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) ) ) ) )
102 19.45v 
 |-  ( E. y ( s e. ( S ` suc N ) \/ ( s = <. x , y >. /\ ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) ) ) <-> ( s e. ( S ` suc N ) \/ E. y ( s = <. x , y >. /\ ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) ) ) )
103 102 exbii 
 |-  ( E. x E. y ( s e. ( S ` suc N ) \/ ( s = <. x , y >. /\ ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) ) ) <-> E. x ( s e. ( S ` suc N ) \/ E. y ( s = <. x , y >. /\ ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) ) ) )
104 19.45v 
 |-  ( E. x ( s e. ( S ` suc N ) \/ E. y ( s = <. x , y >. /\ ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) ) ) <-> ( s e. ( S ` suc N ) \/ E. x E. y ( s = <. x , y >. /\ ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) ) ) )
105 103 104 bitri 
 |-  ( E. x E. y ( s e. ( S ` suc N ) \/ ( s = <. x , y >. /\ ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) ) ) <-> ( s e. ( S ` suc N ) \/ E. x E. y ( s = <. x , y >. /\ ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) ) ) )
106 101 105 imbitrdi 
 |-  ( ( M e. V /\ E e. W /\ N e. _om ) -> ( E. x E. y ( s = <. x , y >. /\ E. u e. ( S ` suc N ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) ) -> ( s e. ( S ` suc N ) \/ E. x E. y ( s = <. x , y >. /\ ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) ) ) ) )
107 8 106 jaod 
 |-  ( ( M e. V /\ E e. W /\ N e. _om ) -> ( ( s e. ( S ` suc N ) \/ E. x E. y ( s = <. x , y >. /\ E. u e. ( S ` suc N ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) ) ) -> ( s e. ( S ` suc N ) \/ E. x E. y ( s = <. x , y >. /\ ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) ) ) ) )
108 difss 
 |-  ( ( S ` suc N ) \ ( S ` N ) ) C_ ( S ` suc N )
109 ssrexv 
 |-  ( ( ( S ` suc N ) \ ( S ` N ) ) C_ ( S ` suc N ) -> ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) -> E. u e. ( S ` suc N ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) ) )
110 108 109 ax-mp 
 |-  ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) -> E. u e. ( S ` suc N ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) )
111 110 a1i 
 |-  ( ( M e. V /\ E e. W /\ N e. _om ) -> ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) -> E. u e. ( S ` suc N ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) ) )
112 111 16 imbitrdi 
 |-  ( ( M e. V /\ E e. W /\ N e. _om ) -> ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) -> E. u e. ( S ` suc N ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) ) )
113 ssrexv 
 |-  ( ( S ` N ) C_ ( S ` suc N ) -> ( E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) -> E. u e. ( S ` suc N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) )
114 37 113 syl 
 |-  ( ( M e. V /\ E e. W /\ N e. _om ) -> ( E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) -> E. u e. ( S ` suc N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) )
115 10 2rexbii 
 |-  ( E. u e. ( S ` suc N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) <-> E. u e. ( S ` suc N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) )
116 114 115 imbitrdi 
 |-  ( ( M e. V /\ E e. W /\ N e. _om ) -> ( E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) -> E. u e. ( S ` suc N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) ) )
117 116 imp 
 |-  ( ( ( M e. V /\ E e. W /\ N e. _om ) /\ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) -> E. u e. ( S ` suc N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) )
118 ssrexv 
 |-  ( ( ( S ` suc N ) \ ( S ` N ) ) C_ ( S ` suc N ) -> ( E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) -> E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) ) )
119 108 118 ax-mp 
 |-  ( E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) -> E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) )
120 119 reximi 
 |-  ( E. u e. ( S ` suc N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) -> E. u e. ( S ` suc N ) E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) )
121 117 120 syl 
 |-  ( ( ( M e. V /\ E e. W /\ N e. _om ) /\ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) -> E. u e. ( S ` suc N ) E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) )
122 121 orcd 
 |-  ( ( ( M e. V /\ E e. W /\ N e. _om ) /\ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) -> ( E. u e. ( S ` suc N ) E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. u e. ( S ` suc N ) E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) )
123 122 ex 
 |-  ( ( M e. V /\ E e. W /\ N e. _om ) -> ( E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) -> ( E. u e. ( S ` suc N ) E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. u e. ( S ` suc N ) E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) ) )
124 r19.43 
 |-  ( E. u e. ( S ` suc N ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) <-> ( E. u e. ( S ` suc N ) E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. u e. ( S ` suc N ) E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) )
125 123 124 imbitrrdi 
 |-  ( ( M e. V /\ E e. W /\ N e. _om ) -> ( E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) -> E. u e. ( S ` suc N ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) ) )
126 112 125 jaod 
 |-  ( ( M e. V /\ E e. W /\ N e. _om ) -> ( ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) -> E. u e. ( S ` suc N ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) ) )
127 126 anim2d 
 |-  ( ( M e. V /\ E e. W /\ N e. _om ) -> ( ( s = <. x , y >. /\ ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) ) -> ( s = <. x , y >. /\ E. u e. ( S ` suc N ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) ) ) )
128 127 2eximdv 
 |-  ( ( M e. V /\ E e. W /\ N e. _om ) -> ( E. x E. y ( s = <. x , y >. /\ ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) ) -> E. x E. y ( s = <. x , y >. /\ E. u e. ( S ` suc N ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) ) ) )
129 128 orim2d 
 |-  ( ( M e. V /\ E e. W /\ N e. _om ) -> ( ( s e. ( S ` suc N ) \/ E. x E. y ( s = <. x , y >. /\ ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) ) ) -> ( s e. ( S ` suc N ) \/ E. x E. y ( s = <. x , y >. /\ E. u e. ( S ` suc N ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) ) ) ) )
130 107 129 impbid 
 |-  ( ( M e. V /\ E e. W /\ N e. _om ) -> ( ( s e. ( S ` suc N ) \/ E. x E. y ( s = <. x , y >. /\ E. u e. ( S ` suc N ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) ) ) <-> ( s e. ( S ` suc N ) \/ E. x E. y ( s = <. x , y >. /\ ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) ) ) ) )
131 elun 
 |-  ( s e. ( ( S ` suc N ) u. { <. x , y >. | E. u e. ( S ` suc N ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) <-> ( s e. ( S ` suc N ) \/ s e. { <. x , y >. | E. u e. ( S ` suc N ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) )
132 elopab 
 |-  ( s e. { <. x , y >. | E. u e. ( S ` suc N ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } <-> E. x E. y ( s = <. x , y >. /\ E. u e. ( S ` suc N ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) ) )
133 132 orbi2i 
 |-  ( ( s e. ( S ` suc N ) \/ s e. { <. x , y >. | E. u e. ( S ` suc N ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) <-> ( s e. ( S ` suc N ) \/ E. x E. y ( s = <. x , y >. /\ E. u e. ( S ` suc N ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) ) ) )
134 131 133 bitri 
 |-  ( s e. ( ( S ` suc N ) u. { <. x , y >. | E. u e. ( S ` suc N ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) <-> ( s e. ( S ` suc N ) \/ E. x E. y ( s = <. x , y >. /\ E. u e. ( S ` suc N ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) ) ) )
135 elun 
 |-  ( s e. ( ( S ` suc N ) u. { <. x , y >. | ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) } ) <-> ( s e. ( S ` suc N ) \/ s e. { <. x , y >. | ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) } ) )
136 elopab 
 |-  ( s e. { <. x , y >. | ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) } <-> E. x E. y ( s = <. x , y >. /\ ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) ) )
137 136 orbi2i 
 |-  ( ( s e. ( S ` suc N ) \/ s e. { <. x , y >. | ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) } ) <-> ( s e. ( S ` suc N ) \/ E. x E. y ( s = <. x , y >. /\ ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) ) ) )
138 135 137 bitri 
 |-  ( s e. ( ( S ` suc N ) u. { <. x , y >. | ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) } ) <-> ( s e. ( S ` suc N ) \/ E. x E. y ( s = <. x , y >. /\ ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) ) ) )
139 130 134 138 3bitr4g 
 |-  ( ( M e. V /\ E e. W /\ N e. _om ) -> ( s e. ( ( S ` suc N ) u. { <. x , y >. | E. u e. ( S ` suc N ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) <-> s e. ( ( S ` suc N ) u. { <. x , y >. | ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) } ) ) )
140 139 eqrdv 
 |-  ( ( M e. V /\ E e. W /\ N e. _om ) -> ( ( S ` suc N ) u. { <. x , y >. | E. u e. ( S ` suc N ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) = ( ( S ` suc N ) u. { <. x , y >. | ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) } ) )
141 6 140 eqtrd 
 |-  ( ( M e. V /\ E e. W /\ N e. _om ) -> ( S ` suc suc N ) = ( ( S ` suc N ) u. { <. x , y >. | ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) } ) )