Metamath Proof Explorer

Theorem r0weon

Description: A set-like well-ordering of the class of ordinal pairs. Proposition 7.58(1) of TakeutiZaring p. 54. (Contributed by Mario Carneiro, 7-Mar-2013) (Revised by Mario Carneiro, 26-Jun-2015)

Ref Expression
Hypotheses leweon.1 
|- L = { <. x , y >. | ( ( x e. ( On X. On ) /\ y e. ( On X. On ) ) /\ ( ( 1st ` x ) e. ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) e. ( 2nd ` y ) ) ) ) }
r0weon.1 
|- R = { <. z , w >. | ( ( z e. ( On X. On ) /\ w e. ( On X. On ) ) /\ ( ( ( 1st ` z ) u. ( 2nd ` z ) ) e. ( ( 1st ` w ) u. ( 2nd ` w ) ) \/ ( ( ( 1st ` z ) u. ( 2nd ` z ) ) = ( ( 1st ` w ) u. ( 2nd ` w ) ) /\ z L w ) ) ) }
Assertion r0weon 
|- ( R We ( On X. On ) /\ R Se ( On X. On ) )

Proof

Step Hyp Ref Expression
1 leweon.1 
 |-  L = { <. x , y >. | ( ( x e. ( On X. On ) /\ y e. ( On X. On ) ) /\ ( ( 1st ` x ) e. ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) e. ( 2nd ` y ) ) ) ) }
2 r0weon.1 
 |-  R = { <. z , w >. | ( ( z e. ( On X. On ) /\ w e. ( On X. On ) ) /\ ( ( ( 1st ` z ) u. ( 2nd ` z ) ) e. ( ( 1st ` w ) u. ( 2nd ` w ) ) \/ ( ( ( 1st ` z ) u. ( 2nd ` z ) ) = ( ( 1st ` w ) u. ( 2nd ` w ) ) /\ z L w ) ) ) }
3 fveq2 
 |-  ( x = z -> ( 1st ` x ) = ( 1st ` z ) )
4 fveq2 
 |-  ( x = z -> ( 2nd ` x ) = ( 2nd ` z ) )
5 3 4 uneq12d 
 |-  ( x = z -> ( ( 1st ` x ) u. ( 2nd ` x ) ) = ( ( 1st ` z ) u. ( 2nd ` z ) ) )
6 eqid 
 |-  ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) = ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) )
7 fvex 
 |-  ( 1st ` z ) e. _V
8 fvex 
 |-  ( 2nd ` z ) e. _V
9 7 8 unex 
 |-  ( ( 1st ` z ) u. ( 2nd ` z ) ) e. _V
10 5 6 9 fvmpt 
 |-  ( z e. ( On X. On ) -> ( ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) ` z ) = ( ( 1st ` z ) u. ( 2nd ` z ) ) )
11 fveq2 
 |-  ( x = w -> ( 1st ` x ) = ( 1st ` w ) )
12 fveq2 
 |-  ( x = w -> ( 2nd ` x ) = ( 2nd ` w ) )
13 11 12 uneq12d 
 |-  ( x = w -> ( ( 1st ` x ) u. ( 2nd ` x ) ) = ( ( 1st ` w ) u. ( 2nd ` w ) ) )
14 fvex 
 |-  ( 1st ` w ) e. _V
15 fvex 
 |-  ( 2nd ` w ) e. _V
16 14 15 unex 
 |-  ( ( 1st ` w ) u. ( 2nd ` w ) ) e. _V
17 13 6 16 fvmpt 
 |-  ( w e. ( On X. On ) -> ( ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) ` w ) = ( ( 1st ` w ) u. ( 2nd ` w ) ) )
18 10 17 breqan12d 
 |-  ( ( z e. ( On X. On ) /\ w e. ( On X. On ) ) -> ( ( ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) ` z ) _E ( ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) ` w ) <-> ( ( 1st ` z ) u. ( 2nd ` z ) ) _E ( ( 1st ` w ) u. ( 2nd ` w ) ) ) )
19 16 epeli 
 |-  ( ( ( 1st ` z ) u. ( 2nd ` z ) ) _E ( ( 1st ` w ) u. ( 2nd ` w ) ) <-> ( ( 1st ` z ) u. ( 2nd ` z ) ) e. ( ( 1st ` w ) u. ( 2nd ` w ) ) )
20 18 19 bitrdi 
 |-  ( ( z e. ( On X. On ) /\ w e. ( On X. On ) ) -> ( ( ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) ` z ) _E ( ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) ` w ) <-> ( ( 1st ` z ) u. ( 2nd ` z ) ) e. ( ( 1st ` w ) u. ( 2nd ` w ) ) ) )
21 10 17 eqeqan12d 
 |-  ( ( z e. ( On X. On ) /\ w e. ( On X. On ) ) -> ( ( ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) ` z ) = ( ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) ` w ) <-> ( ( 1st ` z ) u. ( 2nd ` z ) ) = ( ( 1st ` w ) u. ( 2nd ` w ) ) ) )
22 21 anbi1d 
 |-  ( ( z e. ( On X. On ) /\ w e. ( On X. On ) ) -> ( ( ( ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) ` z ) = ( ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) ` w ) /\ z L w ) <-> ( ( ( 1st ` z ) u. ( 2nd ` z ) ) = ( ( 1st ` w ) u. ( 2nd ` w ) ) /\ z L w ) ) )
23 20 22 orbi12d 
 |-  ( ( z e. ( On X. On ) /\ w e. ( On X. On ) ) -> ( ( ( ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) ` z ) _E ( ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) ` w ) \/ ( ( ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) ` z ) = ( ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) ` w ) /\ z L w ) ) <-> ( ( ( 1st ` z ) u. ( 2nd ` z ) ) e. ( ( 1st ` w ) u. ( 2nd ` w ) ) \/ ( ( ( 1st ` z ) u. ( 2nd ` z ) ) = ( ( 1st ` w ) u. ( 2nd ` w ) ) /\ z L w ) ) ) )
24 23 pm5.32i 
 |-  ( ( ( z e. ( On X. On ) /\ w e. ( On X. On ) ) /\ ( ( ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) ` z ) _E ( ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) ` w ) \/ ( ( ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) ` z ) = ( ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) ` w ) /\ z L w ) ) ) <-> ( ( z e. ( On X. On ) /\ w e. ( On X. On ) ) /\ ( ( ( 1st ` z ) u. ( 2nd ` z ) ) e. ( ( 1st ` w ) u. ( 2nd ` w ) ) \/ ( ( ( 1st ` z ) u. ( 2nd ` z ) ) = ( ( 1st ` w ) u. ( 2nd ` w ) ) /\ z L w ) ) ) )
25 24 opabbii 
 |-  { <. z , w >. | ( ( z e. ( On X. On ) /\ w e. ( On X. On ) ) /\ ( ( ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) ` z ) _E ( ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) ` w ) \/ ( ( ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) ` z ) = ( ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) ` w ) /\ z L w ) ) ) } = { <. z , w >. | ( ( z e. ( On X. On ) /\ w e. ( On X. On ) ) /\ ( ( ( 1st ` z ) u. ( 2nd ` z ) ) e. ( ( 1st ` w ) u. ( 2nd ` w ) ) \/ ( ( ( 1st ` z ) u. ( 2nd ` z ) ) = ( ( 1st ` w ) u. ( 2nd ` w ) ) /\ z L w ) ) ) }
26 2 25 eqtr4i 
 |-  R = { <. z , w >. | ( ( z e. ( On X. On ) /\ w e. ( On X. On ) ) /\ ( ( ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) ` z ) _E ( ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) ` w ) \/ ( ( ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) ` z ) = ( ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) ` w ) /\ z L w ) ) ) }
27 xp1st 
 |-  ( x e. ( On X. On ) -> ( 1st ` x ) e. On )
28 xp2nd 
 |-  ( x e. ( On X. On ) -> ( 2nd ` x ) e. On )
29 fvex 
 |-  ( 1st ` x ) e. _V
30 29 elon 
 |-  ( ( 1st ` x ) e. On <-> Ord ( 1st ` x ) )
31 fvex 
 |-  ( 2nd ` x ) e. _V
32 31 elon 
 |-  ( ( 2nd ` x ) e. On <-> Ord ( 2nd ` x ) )
33 ordun 
 |-  ( ( Ord ( 1st ` x ) /\ Ord ( 2nd ` x ) ) -> Ord ( ( 1st ` x ) u. ( 2nd ` x ) ) )
34 30 32 33 syl2anb 
 |-  ( ( ( 1st ` x ) e. On /\ ( 2nd ` x ) e. On ) -> Ord ( ( 1st ` x ) u. ( 2nd ` x ) ) )
35 27 28 34 syl2anc 
 |-  ( x e. ( On X. On ) -> Ord ( ( 1st ` x ) u. ( 2nd ` x ) ) )
36 29 31 unex 
 |-  ( ( 1st ` x ) u. ( 2nd ` x ) ) e. _V
37 36 elon 
 |-  ( ( ( 1st ` x ) u. ( 2nd ` x ) ) e. On <-> Ord ( ( 1st ` x ) u. ( 2nd ` x ) ) )
38 35 37 sylibr 
 |-  ( x e. ( On X. On ) -> ( ( 1st ` x ) u. ( 2nd ` x ) ) e. On )
39 6 38 fmpti 
 |-  ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) : ( On X. On ) --> On
40 39 a1i 
 |-  ( T. -> ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) : ( On X. On ) --> On )
41 epweon 
 |-  _E We On
42 41 a1i 
 |-  ( T. -> _E We On )
43 1 leweon 
 |-  L We ( On X. On )
44 43 a1i 
 |-  ( T. -> L We ( On X. On ) )
45 vex 
 |-  u e. _V
46 45 dmex 
 |-  dom u e. _V
47 45 rnex 
 |-  ran u e. _V
48 46 47 unex 
 |-  ( dom u u. ran u ) e. _V
49 imadmres 
 |-  ( ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) " dom ( ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) |` u ) ) = ( ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) " u )
50 inss2 
 |-  ( u i^i ( On X. On ) ) C_ ( On X. On )
51 ssun1 
 |-  dom u C_ ( dom u u. ran u )
52 elinel2 
 |-  ( x e. ( u i^i ( On X. On ) ) -> x e. ( On X. On ) )
53 1st2nd2 
 |-  ( x e. ( On X. On ) -> x = <. ( 1st ` x ) , ( 2nd ` x ) >. )
54 52 53 syl 
 |-  ( x e. ( u i^i ( On X. On ) ) -> x = <. ( 1st ` x ) , ( 2nd ` x ) >. )
55 elinel1 
 |-  ( x e. ( u i^i ( On X. On ) ) -> x e. u )
56 54 55 eqeltrrd 
 |-  ( x e. ( u i^i ( On X. On ) ) -> <. ( 1st ` x ) , ( 2nd ` x ) >. e. u )
57 29 31 opeldm 
 |-  ( <. ( 1st ` x ) , ( 2nd ` x ) >. e. u -> ( 1st ` x ) e. dom u )
58 56 57 syl 
 |-  ( x e. ( u i^i ( On X. On ) ) -> ( 1st ` x ) e. dom u )
59 51 58 sselid 
 |-  ( x e. ( u i^i ( On X. On ) ) -> ( 1st ` x ) e. ( dom u u. ran u ) )
60 ssun2 
 |-  ran u C_ ( dom u u. ran u )
61 29 31 opelrn 
 |-  ( <. ( 1st ` x ) , ( 2nd ` x ) >. e. u -> ( 2nd ` x ) e. ran u )
62 56 61 syl 
 |-  ( x e. ( u i^i ( On X. On ) ) -> ( 2nd ` x ) e. ran u )
63 60 62 sselid 
 |-  ( x e. ( u i^i ( On X. On ) ) -> ( 2nd ` x ) e. ( dom u u. ran u ) )
64 59 63 prssd 
 |-  ( x e. ( u i^i ( On X. On ) ) -> { ( 1st ` x ) , ( 2nd ` x ) } C_ ( dom u u. ran u ) )
65 52 27 syl 
 |-  ( x e. ( u i^i ( On X. On ) ) -> ( 1st ` x ) e. On )
66 52 28 syl 
 |-  ( x e. ( u i^i ( On X. On ) ) -> ( 2nd ` x ) e. On )
67 ordunpr 
 |-  ( ( ( 1st ` x ) e. On /\ ( 2nd ` x ) e. On ) -> ( ( 1st ` x ) u. ( 2nd ` x ) ) e. { ( 1st ` x ) , ( 2nd ` x ) } )
68 65 66 67 syl2anc 
 |-  ( x e. ( u i^i ( On X. On ) ) -> ( ( 1st ` x ) u. ( 2nd ` x ) ) e. { ( 1st ` x ) , ( 2nd ` x ) } )
69 64 68 sseldd 
 |-  ( x e. ( u i^i ( On X. On ) ) -> ( ( 1st ` x ) u. ( 2nd ` x ) ) e. ( dom u u. ran u ) )
70 69 rgen 
 |-  A. x e. ( u i^i ( On X. On ) ) ( ( 1st ` x ) u. ( 2nd ` x ) ) e. ( dom u u. ran u )
71 ssrab 
 |-  ( ( u i^i ( On X. On ) ) C_ { x e. ( On X. On ) | ( ( 1st ` x ) u. ( 2nd ` x ) ) e. ( dom u u. ran u ) } <-> ( ( u i^i ( On X. On ) ) C_ ( On X. On ) /\ A. x e. ( u i^i ( On X. On ) ) ( ( 1st ` x ) u. ( 2nd ` x ) ) e. ( dom u u. ran u ) ) )
72 50 70 71 mpbir2an 
 |-  ( u i^i ( On X. On ) ) C_ { x e. ( On X. On ) | ( ( 1st ` x ) u. ( 2nd ` x ) ) e. ( dom u u. ran u ) }
73 dmres 
 |-  dom ( ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) |` u ) = ( u i^i dom ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) )
74 39 fdmi 
 |-  dom ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) = ( On X. On )
75 74 ineq2i 
 |-  ( u i^i dom ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) ) = ( u i^i ( On X. On ) )
76 73 75 eqtri 
 |-  dom ( ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) |` u ) = ( u i^i ( On X. On ) )
77 6 mptpreima 
 |-  ( `' ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) " ( dom u u. ran u ) ) = { x e. ( On X. On ) | ( ( 1st ` x ) u. ( 2nd ` x ) ) e. ( dom u u. ran u ) }
78 72 76 77 3sstr4i 
 |-  dom ( ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) |` u ) C_ ( `' ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) " ( dom u u. ran u ) )
79 funmpt 
 |-  Fun ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) )
80 resss 
 |-  ( ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) |` u ) C_ ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) )
81 dmss 
 |-  ( ( ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) |` u ) C_ ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) -> dom ( ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) |` u ) C_ dom ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) )
82 80 81 ax-mp 
 |-  dom ( ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) |` u ) C_ dom ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) )
83 funimass3 
 |-  ( ( Fun ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) /\ dom ( ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) |` u ) C_ dom ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) ) -> ( ( ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) " dom ( ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) |` u ) ) C_ ( dom u u. ran u ) <-> dom ( ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) |` u ) C_ ( `' ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) " ( dom u u. ran u ) ) ) )
84 79 82 83 mp2an 
 |-  ( ( ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) " dom ( ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) |` u ) ) C_ ( dom u u. ran u ) <-> dom ( ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) |` u ) C_ ( `' ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) " ( dom u u. ran u ) ) )
85 78 84 mpbir 
 |-  ( ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) " dom ( ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) |` u ) ) C_ ( dom u u. ran u )
86 49 85 eqsstrri 
 |-  ( ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) " u ) C_ ( dom u u. ran u )
87 48 86 ssexi 
 |-  ( ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) " u ) e. _V
88 87 a1i 
 |-  ( T. -> ( ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) " u ) e. _V )
89 26 40 42 44 88 fnwe 
 |-  ( T. -> R We ( On X. On ) )
90 epse 
 |-  _E Se On
91 90 a1i 
 |-  ( T. -> _E Se On )
92 vuniex 
 |-  U. u e. _V
93 92 pwex 
 |-  ~P U. u e. _V
94 93 93 xpex 
 |-  ( ~P U. u X. ~P U. u ) e. _V
95 6 mptpreima 
 |-  ( `' ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) " u ) = { x e. ( On X. On ) | ( ( 1st ` x ) u. ( 2nd ` x ) ) e. u }
96 df-rab 
 |-  { x e. ( On X. On ) | ( ( 1st ` x ) u. ( 2nd ` x ) ) e. u } = { x | ( x e. ( On X. On ) /\ ( ( 1st ` x ) u. ( 2nd ` x ) ) e. u ) }
97 95 96 eqtri 
 |-  ( `' ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) " u ) = { x | ( x e. ( On X. On ) /\ ( ( 1st ` x ) u. ( 2nd ` x ) ) e. u ) }
98 53 adantr 
 |-  ( ( x e. ( On X. On ) /\ ( ( 1st ` x ) u. ( 2nd ` x ) ) e. u ) -> x = <. ( 1st ` x ) , ( 2nd ` x ) >. )
99 elssuni 
 |-  ( ( ( 1st ` x ) u. ( 2nd ` x ) ) e. u -> ( ( 1st ` x ) u. ( 2nd ` x ) ) C_ U. u )
100 99 adantl 
 |-  ( ( x e. ( On X. On ) /\ ( ( 1st ` x ) u. ( 2nd ` x ) ) e. u ) -> ( ( 1st ` x ) u. ( 2nd ` x ) ) C_ U. u )
101 100 unssad 
 |-  ( ( x e. ( On X. On ) /\ ( ( 1st ` x ) u. ( 2nd ` x ) ) e. u ) -> ( 1st ` x ) C_ U. u )
102 29 elpw 
 |-  ( ( 1st ` x ) e. ~P U. u <-> ( 1st ` x ) C_ U. u )
103 101 102 sylibr 
 |-  ( ( x e. ( On X. On ) /\ ( ( 1st ` x ) u. ( 2nd ` x ) ) e. u ) -> ( 1st ` x ) e. ~P U. u )
104 100 unssbd 
 |-  ( ( x e. ( On X. On ) /\ ( ( 1st ` x ) u. ( 2nd ` x ) ) e. u ) -> ( 2nd ` x ) C_ U. u )
105 31 elpw 
 |-  ( ( 2nd ` x ) e. ~P U. u <-> ( 2nd ` x ) C_ U. u )
106 104 105 sylibr 
 |-  ( ( x e. ( On X. On ) /\ ( ( 1st ` x ) u. ( 2nd ` x ) ) e. u ) -> ( 2nd ` x ) e. ~P U. u )
107 103 106 jca 
 |-  ( ( x e. ( On X. On ) /\ ( ( 1st ` x ) u. ( 2nd ` x ) ) e. u ) -> ( ( 1st ` x ) e. ~P U. u /\ ( 2nd ` x ) e. ~P U. u ) )
108 elxp6 
 |-  ( x e. ( ~P U. u X. ~P U. u ) <-> ( x = <. ( 1st ` x ) , ( 2nd ` x ) >. /\ ( ( 1st ` x ) e. ~P U. u /\ ( 2nd ` x ) e. ~P U. u ) ) )
109 98 107 108 sylanbrc 
 |-  ( ( x e. ( On X. On ) /\ ( ( 1st ` x ) u. ( 2nd ` x ) ) e. u ) -> x e. ( ~P U. u X. ~P U. u ) )
110 109 abssi 
 |-  { x | ( x e. ( On X. On ) /\ ( ( 1st ` x ) u. ( 2nd ` x ) ) e. u ) } C_ ( ~P U. u X. ~P U. u )
111 97 110 eqsstri 
 |-  ( `' ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) " u ) C_ ( ~P U. u X. ~P U. u )
112 94 111 ssexi 
 |-  ( `' ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) " u ) e. _V
113 112 a1i 
 |-  ( T. -> ( `' ( x e. ( On X. On ) |-> ( ( 1st ` x ) u. ( 2nd ` x ) ) ) " u ) e. _V )
114 26 40 91 113 fnse 
 |-  ( T. -> R Se ( On X. On ) )
115 89 114 jca 
 |-  ( T. -> ( R We ( On X. On ) /\ R Se ( On X. On ) ) )
116 115 mptru 
 |-  ( R We ( On X. On ) /\ R Se ( On X. On ) )