Metamath Proof Explorer


Theorem sat1el2xp

Description: The first component of an element of the value of the satisfaction predicate as function over wff codes in the empty model with an empty binary relation is a member of a doubled Cartesian product. (Contributed by AV, 17-Sep-2023)

Ref Expression
Assertion sat1el2xp
|- ( N e. _om -> A. w e. ( ( (/) Sat (/) ) ` N ) E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) )

Proof

Step Hyp Ref Expression
1 fveq2
 |-  ( x = (/) -> ( ( (/) Sat (/) ) ` x ) = ( ( (/) Sat (/) ) ` (/) ) )
2 1 raleqdv
 |-  ( x = (/) -> ( A. w e. ( ( (/) Sat (/) ) ` x ) E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) <-> A. w e. ( ( (/) Sat (/) ) ` (/) ) E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) ) )
3 fveq2
 |-  ( x = y -> ( ( (/) Sat (/) ) ` x ) = ( ( (/) Sat (/) ) ` y ) )
4 3 raleqdv
 |-  ( x = y -> ( A. w e. ( ( (/) Sat (/) ) ` x ) E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) <-> A. w e. ( ( (/) Sat (/) ) ` y ) E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) ) )
5 fveq2
 |-  ( x = suc y -> ( ( (/) Sat (/) ) ` x ) = ( ( (/) Sat (/) ) ` suc y ) )
6 5 raleqdv
 |-  ( x = suc y -> ( A. w e. ( ( (/) Sat (/) ) ` x ) E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) <-> A. w e. ( ( (/) Sat (/) ) ` suc y ) E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) ) )
7 fveq2
 |-  ( x = N -> ( ( (/) Sat (/) ) ` x ) = ( ( (/) Sat (/) ) ` N ) )
8 7 raleqdv
 |-  ( x = N -> ( A. w e. ( ( (/) Sat (/) ) ` x ) E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) <-> A. w e. ( ( (/) Sat (/) ) ` N ) E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) ) )
9 eqeq1
 |-  ( x = ( 1st ` w ) -> ( x = ( i e.g j ) <-> ( 1st ` w ) = ( i e.g j ) ) )
10 9 2rexbidv
 |-  ( x = ( 1st ` w ) -> ( E. i e. _om E. j e. _om x = ( i e.g j ) <-> E. i e. _om E. j e. _om ( 1st ` w ) = ( i e.g j ) ) )
11 10 anbi2d
 |-  ( x = ( 1st ` w ) -> ( ( z = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) <-> ( z = (/) /\ E. i e. _om E. j e. _om ( 1st ` w ) = ( i e.g j ) ) ) )
12 eqeq1
 |-  ( z = ( 2nd ` w ) -> ( z = (/) <-> ( 2nd ` w ) = (/) ) )
13 12 anbi1d
 |-  ( z = ( 2nd ` w ) -> ( ( z = (/) /\ E. i e. _om E. j e. _om ( 1st ` w ) = ( i e.g j ) ) <-> ( ( 2nd ` w ) = (/) /\ E. i e. _om E. j e. _om ( 1st ` w ) = ( i e.g j ) ) ) )
14 11 13 elopabi
 |-  ( w e. { <. x , z >. | ( z = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } -> ( ( 2nd ` w ) = (/) /\ E. i e. _om E. j e. _om ( 1st ` w ) = ( i e.g j ) ) )
15 goel
 |-  ( ( i e. _om /\ j e. _om ) -> ( i e.g j ) = <. (/) , <. i , j >. >. )
16 15 eqeq2d
 |-  ( ( i e. _om /\ j e. _om ) -> ( ( 1st ` w ) = ( i e.g j ) <-> ( 1st ` w ) = <. (/) , <. i , j >. >. ) )
17 omex
 |-  _om e. _V
18 17 17 pm3.2i
 |-  ( _om e. _V /\ _om e. _V )
19 peano1
 |-  (/) e. _om
20 19 a1i
 |-  ( ( i e. _om /\ j e. _om ) -> (/) e. _om )
21 opelxpi
 |-  ( ( i e. _om /\ j e. _om ) -> <. i , j >. e. ( _om X. _om ) )
22 20 21 opelxpd
 |-  ( ( i e. _om /\ j e. _om ) -> <. (/) , <. i , j >. >. e. ( _om X. ( _om X. _om ) ) )
23 xpeq12
 |-  ( ( a = _om /\ b = _om ) -> ( a X. b ) = ( _om X. _om ) )
24 23 xpeq2d
 |-  ( ( a = _om /\ b = _om ) -> ( _om X. ( a X. b ) ) = ( _om X. ( _om X. _om ) ) )
25 24 eleq2d
 |-  ( ( a = _om /\ b = _om ) -> ( <. (/) , <. i , j >. >. e. ( _om X. ( a X. b ) ) <-> <. (/) , <. i , j >. >. e. ( _om X. ( _om X. _om ) ) ) )
26 25 spc2egv
 |-  ( ( _om e. _V /\ _om e. _V ) -> ( <. (/) , <. i , j >. >. e. ( _om X. ( _om X. _om ) ) -> E. a E. b <. (/) , <. i , j >. >. e. ( _om X. ( a X. b ) ) ) )
27 18 22 26 mpsyl
 |-  ( ( i e. _om /\ j e. _om ) -> E. a E. b <. (/) , <. i , j >. >. e. ( _om X. ( a X. b ) ) )
28 eleq1
 |-  ( ( 1st ` w ) = <. (/) , <. i , j >. >. -> ( ( 1st ` w ) e. ( _om X. ( a X. b ) ) <-> <. (/) , <. i , j >. >. e. ( _om X. ( a X. b ) ) ) )
29 28 2exbidv
 |-  ( ( 1st ` w ) = <. (/) , <. i , j >. >. -> ( E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) <-> E. a E. b <. (/) , <. i , j >. >. e. ( _om X. ( a X. b ) ) ) )
30 27 29 syl5ibrcom
 |-  ( ( i e. _om /\ j e. _om ) -> ( ( 1st ` w ) = <. (/) , <. i , j >. >. -> E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) ) )
31 16 30 sylbid
 |-  ( ( i e. _om /\ j e. _om ) -> ( ( 1st ` w ) = ( i e.g j ) -> E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) ) )
32 31 rexlimivv
 |-  ( E. i e. _om E. j e. _om ( 1st ` w ) = ( i e.g j ) -> E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) )
33 32 adantl
 |-  ( ( ( 2nd ` w ) = (/) /\ E. i e. _om E. j e. _om ( 1st ` w ) = ( i e.g j ) ) -> E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) )
34 14 33 syl
 |-  ( w e. { <. x , z >. | ( z = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } -> E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) )
35 satf00
 |-  ( ( (/) Sat (/) ) ` (/) ) = { <. x , z >. | ( z = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) }
36 34 35 eleq2s
 |-  ( w e. ( ( (/) Sat (/) ) ` (/) ) -> E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) )
37 36 rgen
 |-  A. w e. ( ( (/) Sat (/) ) ` (/) ) E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) )
38 omsucelsucb
 |-  ( y e. _om <-> suc y e. suc _om )
39 satf0sucom
 |-  ( suc y e. suc _om -> ( ( (/) Sat (/) ) ` suc y ) = ( rec ( ( f e. _V |-> ( f u. { <. x , z >. | ( z = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , z >. | ( z = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ` suc y ) )
40 38 39 sylbi
 |-  ( y e. _om -> ( ( (/) Sat (/) ) ` suc y ) = ( rec ( ( f e. _V |-> ( f u. { <. x , z >. | ( z = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , z >. | ( z = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ` suc y ) )
41 40 adantr
 |-  ( ( y e. _om /\ A. w e. ( ( (/) Sat (/) ) ` y ) E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) ) -> ( ( (/) Sat (/) ) ` suc y ) = ( rec ( ( f e. _V |-> ( f u. { <. x , z >. | ( z = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , z >. | ( z = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ` suc y ) )
42 nnon
 |-  ( y e. _om -> y e. On )
43 rdgsuc
 |-  ( y e. On -> ( rec ( ( f e. _V |-> ( f u. { <. x , z >. | ( z = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , z >. | ( z = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ` suc y ) = ( ( f e. _V |-> ( f u. { <. x , z >. | ( z = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) ` ( rec ( ( f e. _V |-> ( f u. { <. x , z >. | ( z = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , z >. | ( z = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ` y ) ) )
44 42 43 syl
 |-  ( y e. _om -> ( rec ( ( f e. _V |-> ( f u. { <. x , z >. | ( z = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , z >. | ( z = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ` suc y ) = ( ( f e. _V |-> ( f u. { <. x , z >. | ( z = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) ` ( rec ( ( f e. _V |-> ( f u. { <. x , z >. | ( z = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , z >. | ( z = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ` y ) ) )
45 44 adantr
 |-  ( ( y e. _om /\ A. w e. ( ( (/) Sat (/) ) ` y ) E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) ) -> ( rec ( ( f e. _V |-> ( f u. { <. x , z >. | ( z = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , z >. | ( z = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ` suc y ) = ( ( f e. _V |-> ( f u. { <. x , z >. | ( z = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) ` ( rec ( ( f e. _V |-> ( f u. { <. x , z >. | ( z = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , z >. | ( z = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ` y ) ) )
46 elelsuc
 |-  ( y e. _om -> y e. suc _om )
47 satf0sucom
 |-  ( y e. suc _om -> ( ( (/) Sat (/) ) ` y ) = ( rec ( ( f e. _V |-> ( f u. { <. x , z >. | ( z = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , z >. | ( z = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ` y ) )
48 46 47 syl
 |-  ( y e. _om -> ( ( (/) Sat (/) ) ` y ) = ( rec ( ( f e. _V |-> ( f u. { <. x , z >. | ( z = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , z >. | ( z = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ` y ) )
49 48 eqcomd
 |-  ( y e. _om -> ( rec ( ( f e. _V |-> ( f u. { <. x , z >. | ( z = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , z >. | ( z = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ` y ) = ( ( (/) Sat (/) ) ` y ) )
50 49 fveq2d
 |-  ( y e. _om -> ( ( f e. _V |-> ( f u. { <. x , z >. | ( z = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) ` ( rec ( ( f e. _V |-> ( f u. { <. x , z >. | ( z = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , z >. | ( z = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ` y ) ) = ( ( f e. _V |-> ( f u. { <. x , z >. | ( z = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) ` ( ( (/) Sat (/) ) ` y ) ) )
51 50 adantr
 |-  ( ( y e. _om /\ A. w e. ( ( (/) Sat (/) ) ` y ) E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) ) -> ( ( f e. _V |-> ( f u. { <. x , z >. | ( z = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) ` ( rec ( ( f e. _V |-> ( f u. { <. x , z >. | ( z = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , z >. | ( z = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ` y ) ) = ( ( f e. _V |-> ( f u. { <. x , z >. | ( z = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) ` ( ( (/) Sat (/) ) ` y ) ) )
52 eqidd
 |-  ( ( y e. _om /\ A. w e. ( ( (/) Sat (/) ) ` y ) E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) ) -> ( f e. _V |-> ( f u. { <. x , z >. | ( z = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) = ( f e. _V |-> ( f u. { <. x , z >. | ( z = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) )
53 id
 |-  ( f = ( ( (/) Sat (/) ) ` y ) -> f = ( ( (/) Sat (/) ) ` y ) )
54 rexeq
 |-  ( f = ( ( (/) Sat (/) ) ` y ) -> ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) <-> E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) ) )
55 54 orbi1d
 |-  ( f = ( ( (/) Sat (/) ) ` y ) -> ( ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) <-> ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) )
56 55 rexeqbi1dv
 |-  ( f = ( ( (/) Sat (/) ) ` y ) -> ( E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) <-> E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) )
57 56 anbi2d
 |-  ( f = ( ( (/) Sat (/) ) ` y ) -> ( ( z = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) <-> ( z = (/) /\ E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) ) )
58 57 opabbidv
 |-  ( f = ( ( (/) Sat (/) ) ` y ) -> { <. x , z >. | ( z = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } = { <. x , z >. | ( z = (/) /\ E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } )
59 53 58 uneq12d
 |-  ( f = ( ( (/) Sat (/) ) ` y ) -> ( f u. { <. x , z >. | ( z = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) = ( ( ( (/) Sat (/) ) ` y ) u. { <. x , z >. | ( z = (/) /\ E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) )
60 59 adantl
 |-  ( ( ( y e. _om /\ A. w e. ( ( (/) Sat (/) ) ` y ) E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) ) /\ f = ( ( (/) Sat (/) ) ` y ) ) -> ( f u. { <. x , z >. | ( z = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) = ( ( ( (/) Sat (/) ) ` y ) u. { <. x , z >. | ( z = (/) /\ E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) )
61 fvexd
 |-  ( ( y e. _om /\ A. w e. ( ( (/) Sat (/) ) ` y ) E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) ) -> ( ( (/) Sat (/) ) ` y ) e. _V )
62 17 a1i
 |-  ( ( y e. _om /\ A. w e. ( ( (/) Sat (/) ) ` y ) E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) ) -> _om e. _V )
63 satf0suclem
 |-  ( ( ( ( (/) Sat (/) ) ` y ) e. _V /\ ( ( (/) Sat (/) ) ` y ) e. _V /\ _om e. _V ) -> { <. x , z >. | ( z = (/) /\ E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } e. _V )
64 61 61 62 63 syl3anc
 |-  ( ( y e. _om /\ A. w e. ( ( (/) Sat (/) ) ` y ) E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) ) -> { <. x , z >. | ( z = (/) /\ E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } e. _V )
65 unexg
 |-  ( ( ( ( (/) Sat (/) ) ` y ) e. _V /\ { <. x , z >. | ( z = (/) /\ E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } e. _V ) -> ( ( ( (/) Sat (/) ) ` y ) u. { <. x , z >. | ( z = (/) /\ E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) e. _V )
66 61 64 65 syl2anc
 |-  ( ( y e. _om /\ A. w e. ( ( (/) Sat (/) ) ` y ) E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) ) -> ( ( ( (/) Sat (/) ) ` y ) u. { <. x , z >. | ( z = (/) /\ E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) e. _V )
67 52 60 61 66 fvmptd
 |-  ( ( y e. _om /\ A. w e. ( ( (/) Sat (/) ) ` y ) E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) ) -> ( ( f e. _V |-> ( f u. { <. x , z >. | ( z = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) ` ( ( (/) Sat (/) ) ` y ) ) = ( ( ( (/) Sat (/) ) ` y ) u. { <. x , z >. | ( z = (/) /\ E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) )
68 45 51 67 3eqtrd
 |-  ( ( y e. _om /\ A. w e. ( ( (/) Sat (/) ) ` y ) E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) ) -> ( rec ( ( f e. _V |-> ( f u. { <. x , z >. | ( z = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , z >. | ( z = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ` suc y ) = ( ( ( (/) Sat (/) ) ` y ) u. { <. x , z >. | ( z = (/) /\ E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) )
69 41 68 eqtrd
 |-  ( ( y e. _om /\ A. w e. ( ( (/) Sat (/) ) ` y ) E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) ) -> ( ( (/) Sat (/) ) ` suc y ) = ( ( ( (/) Sat (/) ) ` y ) u. { <. x , z >. | ( z = (/) /\ E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) )
70 69 eleq2d
 |-  ( ( y e. _om /\ A. w e. ( ( (/) Sat (/) ) ` y ) E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) ) -> ( t e. ( ( (/) Sat (/) ) ` suc y ) <-> t e. ( ( ( (/) Sat (/) ) ` y ) u. { <. x , z >. | ( z = (/) /\ E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) )
71 elun
 |-  ( t e. ( ( ( (/) Sat (/) ) ` y ) u. { <. x , z >. | ( z = (/) /\ E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) <-> ( t e. ( ( (/) Sat (/) ) ` y ) \/ t e. { <. x , z >. | ( z = (/) /\ E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) )
72 70 71 bitrdi
 |-  ( ( y e. _om /\ A. w e. ( ( (/) Sat (/) ) ` y ) E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) ) -> ( t e. ( ( (/) Sat (/) ) ` suc y ) <-> ( t e. ( ( (/) Sat (/) ) ` y ) \/ t e. { <. x , z >. | ( z = (/) /\ E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) )
73 fveq2
 |-  ( w = t -> ( 1st ` w ) = ( 1st ` t ) )
74 73 eleq1d
 |-  ( w = t -> ( ( 1st ` w ) e. ( _om X. ( a X. b ) ) <-> ( 1st ` t ) e. ( _om X. ( a X. b ) ) ) )
75 74 2exbidv
 |-  ( w = t -> ( E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) <-> E. a E. b ( 1st ` t ) e. ( _om X. ( a X. b ) ) ) )
76 75 rspccv
 |-  ( A. w e. ( ( (/) Sat (/) ) ` y ) E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) -> ( t e. ( ( (/) Sat (/) ) ` y ) -> E. a E. b ( 1st ` t ) e. ( _om X. ( a X. b ) ) ) )
77 76 adantl
 |-  ( ( y e. _om /\ A. w e. ( ( (/) Sat (/) ) ` y ) E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) ) -> ( t e. ( ( (/) Sat (/) ) ` y ) -> E. a E. b ( 1st ` t ) e. ( _om X. ( a X. b ) ) ) )
78 fveq2
 |-  ( w = v -> ( 1st ` w ) = ( 1st ` v ) )
79 78 eleq1d
 |-  ( w = v -> ( ( 1st ` w ) e. ( _om X. ( a X. b ) ) <-> ( 1st ` v ) e. ( _om X. ( a X. b ) ) ) )
80 79 2exbidv
 |-  ( w = v -> ( E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) <-> E. a E. b ( 1st ` v ) e. ( _om X. ( a X. b ) ) ) )
81 80 rspcva
 |-  ( ( v e. ( ( (/) Sat (/) ) ` y ) /\ A. w e. ( ( (/) Sat (/) ) ` y ) E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) ) -> E. a E. b ( 1st ` v ) e. ( _om X. ( a X. b ) ) )
82 sels
 |-  ( ( 1st ` v ) e. ( _om X. ( a X. b ) ) -> E. s ( 1st ` v ) e. s )
83 82 exlimivv
 |-  ( E. a E. b ( 1st ` v ) e. ( _om X. ( a X. b ) ) -> E. s ( 1st ` v ) e. s )
84 81 83 syl
 |-  ( ( v e. ( ( (/) Sat (/) ) ` y ) /\ A. w e. ( ( (/) Sat (/) ) ` y ) E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) ) -> E. s ( 1st ` v ) e. s )
85 84 expcom
 |-  ( A. w e. ( ( (/) Sat (/) ) ` y ) E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) -> ( v e. ( ( (/) Sat (/) ) ` y ) -> E. s ( 1st ` v ) e. s ) )
86 fveq2
 |-  ( w = u -> ( 1st ` w ) = ( 1st ` u ) )
87 86 eleq1d
 |-  ( w = u -> ( ( 1st ` w ) e. ( _om X. ( a X. b ) ) <-> ( 1st ` u ) e. ( _om X. ( a X. b ) ) ) )
88 87 2exbidv
 |-  ( w = u -> ( E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) <-> E. a E. b ( 1st ` u ) e. ( _om X. ( a X. b ) ) ) )
89 88 rspcva
 |-  ( ( u e. ( ( (/) Sat (/) ) ` y ) /\ A. w e. ( ( (/) Sat (/) ) ` y ) E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) ) -> E. a E. b ( 1st ` u ) e. ( _om X. ( a X. b ) ) )
90 sels
 |-  ( ( 1st ` u ) e. ( _om X. ( a X. b ) ) -> E. s ( 1st ` u ) e. s )
91 90 exlimivv
 |-  ( E. a E. b ( 1st ` u ) e. ( _om X. ( a X. b ) ) -> E. s ( 1st ` u ) e. s )
92 89 91 syl
 |-  ( ( u e. ( ( (/) Sat (/) ) ` y ) /\ A. w e. ( ( (/) Sat (/) ) ` y ) E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) ) -> E. s ( 1st ` u ) e. s )
93 eleq2w
 |-  ( s = r -> ( ( 1st ` u ) e. s <-> ( 1st ` u ) e. r ) )
94 93 cbvexvw
 |-  ( E. s ( 1st ` u ) e. s <-> E. r ( 1st ` u ) e. r )
95 vex
 |-  r e. _V
96 vex
 |-  s e. _V
97 95 96 pm3.2i
 |-  ( r e. _V /\ s e. _V )
98 df-ov
 |-  ( ( 1st ` u ) |g ( 1st ` v ) ) = ( |g ` <. ( 1st ` u ) , ( 1st ` v ) >. )
99 df-gona
 |-  |g = ( e e. ( _V X. _V ) |-> <. 1o , e >. )
100 opeq2
 |-  ( e = <. ( 1st ` u ) , ( 1st ` v ) >. -> <. 1o , e >. = <. 1o , <. ( 1st ` u ) , ( 1st ` v ) >. >. )
101 opelvvg
 |-  ( ( ( 1st ` u ) e. r /\ ( 1st ` v ) e. s ) -> <. ( 1st ` u ) , ( 1st ` v ) >. e. ( _V X. _V ) )
102 opex
 |-  <. 1o , <. ( 1st ` u ) , ( 1st ` v ) >. >. e. _V
103 102 a1i
 |-  ( ( ( 1st ` u ) e. r /\ ( 1st ` v ) e. s ) -> <. 1o , <. ( 1st ` u ) , ( 1st ` v ) >. >. e. _V )
104 99 100 101 103 fvmptd3
 |-  ( ( ( 1st ` u ) e. r /\ ( 1st ` v ) e. s ) -> ( |g ` <. ( 1st ` u ) , ( 1st ` v ) >. ) = <. 1o , <. ( 1st ` u ) , ( 1st ` v ) >. >. )
105 98 104 syl5eq
 |-  ( ( ( 1st ` u ) e. r /\ ( 1st ` v ) e. s ) -> ( ( 1st ` u ) |g ( 1st ` v ) ) = <. 1o , <. ( 1st ` u ) , ( 1st ` v ) >. >. )
106 1onn
 |-  1o e. _om
107 106 a1i
 |-  ( ( ( 1st ` u ) e. r /\ ( 1st ` v ) e. s ) -> 1o e. _om )
108 opelxpi
 |-  ( ( ( 1st ` u ) e. r /\ ( 1st ` v ) e. s ) -> <. ( 1st ` u ) , ( 1st ` v ) >. e. ( r X. s ) )
109 107 108 opelxpd
 |-  ( ( ( 1st ` u ) e. r /\ ( 1st ` v ) e. s ) -> <. 1o , <. ( 1st ` u ) , ( 1st ` v ) >. >. e. ( _om X. ( r X. s ) ) )
110 105 109 eqeltrd
 |-  ( ( ( 1st ` u ) e. r /\ ( 1st ` v ) e. s ) -> ( ( 1st ` u ) |g ( 1st ` v ) ) e. ( _om X. ( r X. s ) ) )
111 xpeq12
 |-  ( ( a = r /\ b = s ) -> ( a X. b ) = ( r X. s ) )
112 111 xpeq2d
 |-  ( ( a = r /\ b = s ) -> ( _om X. ( a X. b ) ) = ( _om X. ( r X. s ) ) )
113 112 eleq2d
 |-  ( ( a = r /\ b = s ) -> ( ( ( 1st ` u ) |g ( 1st ` v ) ) e. ( _om X. ( a X. b ) ) <-> ( ( 1st ` u ) |g ( 1st ` v ) ) e. ( _om X. ( r X. s ) ) ) )
114 113 spc2egv
 |-  ( ( r e. _V /\ s e. _V ) -> ( ( ( 1st ` u ) |g ( 1st ` v ) ) e. ( _om X. ( r X. s ) ) -> E. a E. b ( ( 1st ` u ) |g ( 1st ` v ) ) e. ( _om X. ( a X. b ) ) ) )
115 97 110 114 mpsyl
 |-  ( ( ( 1st ` u ) e. r /\ ( 1st ` v ) e. s ) -> E. a E. b ( ( 1st ` u ) |g ( 1st ` v ) ) e. ( _om X. ( a X. b ) ) )
116 eleq1
 |-  ( ( 1st ` t ) = ( ( 1st ` u ) |g ( 1st ` v ) ) -> ( ( 1st ` t ) e. ( _om X. ( a X. b ) ) <-> ( ( 1st ` u ) |g ( 1st ` v ) ) e. ( _om X. ( a X. b ) ) ) )
117 116 2exbidv
 |-  ( ( 1st ` t ) = ( ( 1st ` u ) |g ( 1st ` v ) ) -> ( E. a E. b ( 1st ` t ) e. ( _om X. ( a X. b ) ) <-> E. a E. b ( ( 1st ` u ) |g ( 1st ` v ) ) e. ( _om X. ( a X. b ) ) ) )
118 115 117 syl5ibrcom
 |-  ( ( ( 1st ` u ) e. r /\ ( 1st ` v ) e. s ) -> ( ( 1st ` t ) = ( ( 1st ` u ) |g ( 1st ` v ) ) -> E. a E. b ( 1st ` t ) e. ( _om X. ( a X. b ) ) ) )
119 118 ex
 |-  ( ( 1st ` u ) e. r -> ( ( 1st ` v ) e. s -> ( ( 1st ` t ) = ( ( 1st ` u ) |g ( 1st ` v ) ) -> E. a E. b ( 1st ` t ) e. ( _om X. ( a X. b ) ) ) ) )
120 119 exlimdv
 |-  ( ( 1st ` u ) e. r -> ( E. s ( 1st ` v ) e. s -> ( ( 1st ` t ) = ( ( 1st ` u ) |g ( 1st ` v ) ) -> E. a E. b ( 1st ` t ) e. ( _om X. ( a X. b ) ) ) ) )
121 120 com23
 |-  ( ( 1st ` u ) e. r -> ( ( 1st ` t ) = ( ( 1st ` u ) |g ( 1st ` v ) ) -> ( E. s ( 1st ` v ) e. s -> E. a E. b ( 1st ` t ) e. ( _om X. ( a X. b ) ) ) ) )
122 121 exlimiv
 |-  ( E. r ( 1st ` u ) e. r -> ( ( 1st ` t ) = ( ( 1st ` u ) |g ( 1st ` v ) ) -> ( E. s ( 1st ` v ) e. s -> E. a E. b ( 1st ` t ) e. ( _om X. ( a X. b ) ) ) ) )
123 94 122 sylbi
 |-  ( E. s ( 1st ` u ) e. s -> ( ( 1st ` t ) = ( ( 1st ` u ) |g ( 1st ` v ) ) -> ( E. s ( 1st ` v ) e. s -> E. a E. b ( 1st ` t ) e. ( _om X. ( a X. b ) ) ) ) )
124 92 123 syl
 |-  ( ( u e. ( ( (/) Sat (/) ) ` y ) /\ A. w e. ( ( (/) Sat (/) ) ` y ) E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) ) -> ( ( 1st ` t ) = ( ( 1st ` u ) |g ( 1st ` v ) ) -> ( E. s ( 1st ` v ) e. s -> E. a E. b ( 1st ` t ) e. ( _om X. ( a X. b ) ) ) ) )
125 124 expcom
 |-  ( A. w e. ( ( (/) Sat (/) ) ` y ) E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) -> ( u e. ( ( (/) Sat (/) ) ` y ) -> ( ( 1st ` t ) = ( ( 1st ` u ) |g ( 1st ` v ) ) -> ( E. s ( 1st ` v ) e. s -> E. a E. b ( 1st ` t ) e. ( _om X. ( a X. b ) ) ) ) ) )
126 125 com24
 |-  ( A. w e. ( ( (/) Sat (/) ) ` y ) E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) -> ( E. s ( 1st ` v ) e. s -> ( ( 1st ` t ) = ( ( 1st ` u ) |g ( 1st ` v ) ) -> ( u e. ( ( (/) Sat (/) ) ` y ) -> E. a E. b ( 1st ` t ) e. ( _om X. ( a X. b ) ) ) ) ) )
127 85 126 syld
 |-  ( A. w e. ( ( (/) Sat (/) ) ` y ) E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) -> ( v e. ( ( (/) Sat (/) ) ` y ) -> ( ( 1st ` t ) = ( ( 1st ` u ) |g ( 1st ` v ) ) -> ( u e. ( ( (/) Sat (/) ) ` y ) -> E. a E. b ( 1st ` t ) e. ( _om X. ( a X. b ) ) ) ) ) )
128 127 adantl
 |-  ( ( y e. _om /\ A. w e. ( ( (/) Sat (/) ) ` y ) E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) ) -> ( v e. ( ( (/) Sat (/) ) ` y ) -> ( ( 1st ` t ) = ( ( 1st ` u ) |g ( 1st ` v ) ) -> ( u e. ( ( (/) Sat (/) ) ` y ) -> E. a E. b ( 1st ` t ) e. ( _om X. ( a X. b ) ) ) ) ) )
129 128 com14
 |-  ( u e. ( ( (/) Sat (/) ) ` y ) -> ( v e. ( ( (/) Sat (/) ) ` y ) -> ( ( 1st ` t ) = ( ( 1st ` u ) |g ( 1st ` v ) ) -> ( ( y e. _om /\ A. w e. ( ( (/) Sat (/) ) ` y ) E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) ) -> E. a E. b ( 1st ` t ) e. ( _om X. ( a X. b ) ) ) ) ) )
130 129 rexlimdv
 |-  ( u e. ( ( (/) Sat (/) ) ` y ) -> ( E. v e. ( ( (/) Sat (/) ) ` y ) ( 1st ` t ) = ( ( 1st ` u ) |g ( 1st ` v ) ) -> ( ( y e. _om /\ A. w e. ( ( (/) Sat (/) ) ` y ) E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) ) -> E. a E. b ( 1st ` t ) e. ( _om X. ( a X. b ) ) ) ) )
131 17 96 pm3.2i
 |-  ( _om e. _V /\ s e. _V )
132 df-goal
 |-  A.g i ( 1st ` u ) = <. 2o , <. i , ( 1st ` u ) >. >.
133 2onn
 |-  2o e. _om
134 133 a1i
 |-  ( ( ( 1st ` u ) e. s /\ i e. _om ) -> 2o e. _om )
135 opelxpi
 |-  ( ( i e. _om /\ ( 1st ` u ) e. s ) -> <. i , ( 1st ` u ) >. e. ( _om X. s ) )
136 135 ancoms
 |-  ( ( ( 1st ` u ) e. s /\ i e. _om ) -> <. i , ( 1st ` u ) >. e. ( _om X. s ) )
137 134 136 opelxpd
 |-  ( ( ( 1st ` u ) e. s /\ i e. _om ) -> <. 2o , <. i , ( 1st ` u ) >. >. e. ( _om X. ( _om X. s ) ) )
138 132 137 eqeltrid
 |-  ( ( ( 1st ` u ) e. s /\ i e. _om ) -> A.g i ( 1st ` u ) e. ( _om X. ( _om X. s ) ) )
139 138 3adant3
 |-  ( ( ( 1st ` u ) e. s /\ i e. _om /\ ( 1st ` t ) = A.g i ( 1st ` u ) ) -> A.g i ( 1st ` u ) e. ( _om X. ( _om X. s ) ) )
140 eleq1
 |-  ( ( 1st ` t ) = A.g i ( 1st ` u ) -> ( ( 1st ` t ) e. ( _om X. ( _om X. s ) ) <-> A.g i ( 1st ` u ) e. ( _om X. ( _om X. s ) ) ) )
141 140 3ad2ant3
 |-  ( ( ( 1st ` u ) e. s /\ i e. _om /\ ( 1st ` t ) = A.g i ( 1st ` u ) ) -> ( ( 1st ` t ) e. ( _om X. ( _om X. s ) ) <-> A.g i ( 1st ` u ) e. ( _om X. ( _om X. s ) ) ) )
142 139 141 mpbird
 |-  ( ( ( 1st ` u ) e. s /\ i e. _om /\ ( 1st ` t ) = A.g i ( 1st ` u ) ) -> ( 1st ` t ) e. ( _om X. ( _om X. s ) ) )
143 xpeq12
 |-  ( ( a = _om /\ b = s ) -> ( a X. b ) = ( _om X. s ) )
144 143 xpeq2d
 |-  ( ( a = _om /\ b = s ) -> ( _om X. ( a X. b ) ) = ( _om X. ( _om X. s ) ) )
145 144 eleq2d
 |-  ( ( a = _om /\ b = s ) -> ( ( 1st ` t ) e. ( _om X. ( a X. b ) ) <-> ( 1st ` t ) e. ( _om X. ( _om X. s ) ) ) )
146 145 spc2egv
 |-  ( ( _om e. _V /\ s e. _V ) -> ( ( 1st ` t ) e. ( _om X. ( _om X. s ) ) -> E. a E. b ( 1st ` t ) e. ( _om X. ( a X. b ) ) ) )
147 131 142 146 mpsyl
 |-  ( ( ( 1st ` u ) e. s /\ i e. _om /\ ( 1st ` t ) = A.g i ( 1st ` u ) ) -> E. a E. b ( 1st ` t ) e. ( _om X. ( a X. b ) ) )
148 147 3exp
 |-  ( ( 1st ` u ) e. s -> ( i e. _om -> ( ( 1st ` t ) = A.g i ( 1st ` u ) -> E. a E. b ( 1st ` t ) e. ( _om X. ( a X. b ) ) ) ) )
149 148 com23
 |-  ( ( 1st ` u ) e. s -> ( ( 1st ` t ) = A.g i ( 1st ` u ) -> ( i e. _om -> E. a E. b ( 1st ` t ) e. ( _om X. ( a X. b ) ) ) ) )
150 149 a1d
 |-  ( ( 1st ` u ) e. s -> ( y e. _om -> ( ( 1st ` t ) = A.g i ( 1st ` u ) -> ( i e. _om -> E. a E. b ( 1st ` t ) e. ( _om X. ( a X. b ) ) ) ) ) )
151 150 exlimiv
 |-  ( E. s ( 1st ` u ) e. s -> ( y e. _om -> ( ( 1st ` t ) = A.g i ( 1st ` u ) -> ( i e. _om -> E. a E. b ( 1st ` t ) e. ( _om X. ( a X. b ) ) ) ) ) )
152 92 151 syl
 |-  ( ( u e. ( ( (/) Sat (/) ) ` y ) /\ A. w e. ( ( (/) Sat (/) ) ` y ) E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) ) -> ( y e. _om -> ( ( 1st ` t ) = A.g i ( 1st ` u ) -> ( i e. _om -> E. a E. b ( 1st ` t ) e. ( _om X. ( a X. b ) ) ) ) ) )
153 152 ex
 |-  ( u e. ( ( (/) Sat (/) ) ` y ) -> ( A. w e. ( ( (/) Sat (/) ) ` y ) E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) -> ( y e. _om -> ( ( 1st ` t ) = A.g i ( 1st ` u ) -> ( i e. _om -> E. a E. b ( 1st ` t ) e. ( _om X. ( a X. b ) ) ) ) ) ) )
154 153 impcomd
 |-  ( u e. ( ( (/) Sat (/) ) ` y ) -> ( ( y e. _om /\ A. w e. ( ( (/) Sat (/) ) ` y ) E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) ) -> ( ( 1st ` t ) = A.g i ( 1st ` u ) -> ( i e. _om -> E. a E. b ( 1st ` t ) e. ( _om X. ( a X. b ) ) ) ) ) )
155 154 com24
 |-  ( u e. ( ( (/) Sat (/) ) ` y ) -> ( i e. _om -> ( ( 1st ` t ) = A.g i ( 1st ` u ) -> ( ( y e. _om /\ A. w e. ( ( (/) Sat (/) ) ` y ) E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) ) -> E. a E. b ( 1st ` t ) e. ( _om X. ( a X. b ) ) ) ) ) )
156 155 rexlimdv
 |-  ( u e. ( ( (/) Sat (/) ) ` y ) -> ( E. i e. _om ( 1st ` t ) = A.g i ( 1st ` u ) -> ( ( y e. _om /\ A. w e. ( ( (/) Sat (/) ) ` y ) E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) ) -> E. a E. b ( 1st ` t ) e. ( _om X. ( a X. b ) ) ) ) )
157 130 156 jaod
 |-  ( u e. ( ( (/) Sat (/) ) ` y ) -> ( ( E. v e. ( ( (/) Sat (/) ) ` y ) ( 1st ` t ) = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om ( 1st ` t ) = A.g i ( 1st ` u ) ) -> ( ( y e. _om /\ A. w e. ( ( (/) Sat (/) ) ` y ) E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) ) -> E. a E. b ( 1st ` t ) e. ( _om X. ( a X. b ) ) ) ) )
158 157 rexlimiv
 |-  ( E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) ( 1st ` t ) = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om ( 1st ` t ) = A.g i ( 1st ` u ) ) -> ( ( y e. _om /\ A. w e. ( ( (/) Sat (/) ) ` y ) E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) ) -> E. a E. b ( 1st ` t ) e. ( _om X. ( a X. b ) ) ) )
159 158 adantl
 |-  ( ( ( 2nd ` t ) = (/) /\ E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) ( 1st ` t ) = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om ( 1st ` t ) = A.g i ( 1st ` u ) ) ) -> ( ( y e. _om /\ A. w e. ( ( (/) Sat (/) ) ` y ) E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) ) -> E. a E. b ( 1st ` t ) e. ( _om X. ( a X. b ) ) ) )
160 eqeq1
 |-  ( x = ( 1st ` t ) -> ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) <-> ( 1st ` t ) = ( ( 1st ` u ) |g ( 1st ` v ) ) ) )
161 160 rexbidv
 |-  ( x = ( 1st ` t ) -> ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) <-> E. v e. ( ( (/) Sat (/) ) ` y ) ( 1st ` t ) = ( ( 1st ` u ) |g ( 1st ` v ) ) ) )
162 eqeq1
 |-  ( x = ( 1st ` t ) -> ( x = A.g i ( 1st ` u ) <-> ( 1st ` t ) = A.g i ( 1st ` u ) ) )
163 162 rexbidv
 |-  ( x = ( 1st ` t ) -> ( E. i e. _om x = A.g i ( 1st ` u ) <-> E. i e. _om ( 1st ` t ) = A.g i ( 1st ` u ) ) )
164 161 163 orbi12d
 |-  ( x = ( 1st ` t ) -> ( ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) <-> ( E. v e. ( ( (/) Sat (/) ) ` y ) ( 1st ` t ) = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om ( 1st ` t ) = A.g i ( 1st ` u ) ) ) )
165 164 rexbidv
 |-  ( x = ( 1st ` t ) -> ( E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) <-> E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) ( 1st ` t ) = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om ( 1st ` t ) = A.g i ( 1st ` u ) ) ) )
166 165 anbi2d
 |-  ( x = ( 1st ` t ) -> ( ( z = (/) /\ E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) <-> ( z = (/) /\ E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) ( 1st ` t ) = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om ( 1st ` t ) = A.g i ( 1st ` u ) ) ) ) )
167 eqeq1
 |-  ( z = ( 2nd ` t ) -> ( z = (/) <-> ( 2nd ` t ) = (/) ) )
168 167 anbi1d
 |-  ( z = ( 2nd ` t ) -> ( ( z = (/) /\ E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) ( 1st ` t ) = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om ( 1st ` t ) = A.g i ( 1st ` u ) ) ) <-> ( ( 2nd ` t ) = (/) /\ E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) ( 1st ` t ) = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om ( 1st ` t ) = A.g i ( 1st ` u ) ) ) ) )
169 166 168 elopabi
 |-  ( t e. { <. x , z >. | ( z = (/) /\ E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } -> ( ( 2nd ` t ) = (/) /\ E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) ( 1st ` t ) = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om ( 1st ` t ) = A.g i ( 1st ` u ) ) ) )
170 159 169 syl11
 |-  ( ( y e. _om /\ A. w e. ( ( (/) Sat (/) ) ` y ) E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) ) -> ( t e. { <. x , z >. | ( z = (/) /\ E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } -> E. a E. b ( 1st ` t ) e. ( _om X. ( a X. b ) ) ) )
171 77 170 jaod
 |-  ( ( y e. _om /\ A. w e. ( ( (/) Sat (/) ) ` y ) E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) ) -> ( ( t e. ( ( (/) Sat (/) ) ` y ) \/ t e. { <. x , z >. | ( z = (/) /\ E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) -> E. a E. b ( 1st ` t ) e. ( _om X. ( a X. b ) ) ) )
172 72 171 sylbid
 |-  ( ( y e. _om /\ A. w e. ( ( (/) Sat (/) ) ` y ) E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) ) -> ( t e. ( ( (/) Sat (/) ) ` suc y ) -> E. a E. b ( 1st ` t ) e. ( _om X. ( a X. b ) ) ) )
173 172 ex
 |-  ( y e. _om -> ( A. w e. ( ( (/) Sat (/) ) ` y ) E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) -> ( t e. ( ( (/) Sat (/) ) ` suc y ) -> E. a E. b ( 1st ` t ) e. ( _om X. ( a X. b ) ) ) ) )
174 173 ralrimdv
 |-  ( y e. _om -> ( A. w e. ( ( (/) Sat (/) ) ` y ) E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) -> A. t e. ( ( (/) Sat (/) ) ` suc y ) E. a E. b ( 1st ` t ) e. ( _om X. ( a X. b ) ) ) )
175 75 cbvralvw
 |-  ( A. w e. ( ( (/) Sat (/) ) ` suc y ) E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) <-> A. t e. ( ( (/) Sat (/) ) ` suc y ) E. a E. b ( 1st ` t ) e. ( _om X. ( a X. b ) ) )
176 174 175 syl6ibr
 |-  ( y e. _om -> ( A. w e. ( ( (/) Sat (/) ) ` y ) E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) -> A. w e. ( ( (/) Sat (/) ) ` suc y ) E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) ) )
177 2 4 6 8 37 176 finds
 |-  ( N e. _om -> A. w e. ( ( (/) Sat (/) ) ` N ) E. a E. b ( 1st ` w ) e. ( _om X. ( a X. b ) ) )