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 syl5bb
 |-  ( ( ( 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 syl5bb
 |-  ( ( ( 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 syl6ib
 |-  ( ( 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 syl6ib
 |-  ( ( 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 syl6ib
 |-  ( ( 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 syl6ibr
 |-  ( ( 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 ) ) } ) )