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

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 eqtrid 
 |-  ( ( ( 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 imbitrrdi 
 |-  ( 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 ) ) )