Metamath Proof Explorer

Theorem hartogslem1

Description: Lemma for hartogs . (Contributed by Mario Carneiro, 14-Jan-2013) (Revised by Mario Carneiro, 15-May-2015)

Ref Expression
Hypotheses hartogslem.2 
|- F = { <. r , y >. | ( ( ( dom r C_ A /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) }
hartogslem.3 
|- R = { <. s , t >. | E. w e. y E. z e. y ( ( s = ( f ` w ) /\ t = ( f ` z ) ) /\ w _E z ) }
Assertion hartogslem1 
|- ( dom F C_ ~P ( A X. A ) /\ Fun F /\ ( A e. V -> ran F = { x e. On | x ~<_ A } ) )

Proof

Step Hyp Ref Expression
1 hartogslem.2 
 |-  F = { <. r , y >. | ( ( ( dom r C_ A /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) }
2 hartogslem.3 
 |-  R = { <. s , t >. | E. w e. y E. z e. y ( ( s = ( f ` w ) /\ t = ( f ` z ) ) /\ w _E z ) }
3 1 dmeqi 
 |-  dom F = dom { <. r , y >. | ( ( ( dom r C_ A /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) }
4 dmopab 
 |-  dom { <. r , y >. | ( ( ( dom r C_ A /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) } = { r | E. y ( ( ( dom r C_ A /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) }
5 3 4 eqtri 
 |-  dom F = { r | E. y ( ( ( dom r C_ A /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) }
6 simp3 
 |-  ( ( dom r C_ A /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) -> r C_ ( dom r X. dom r ) )
7 simp1 
 |-  ( ( dom r C_ A /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) -> dom r C_ A )
8 xpss12 
 |-  ( ( dom r C_ A /\ dom r C_ A ) -> ( dom r X. dom r ) C_ ( A X. A ) )
9 7 7 8 syl2anc 
 |-  ( ( dom r C_ A /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) -> ( dom r X. dom r ) C_ ( A X. A ) )
10 6 9 sstrd 
 |-  ( ( dom r C_ A /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) -> r C_ ( A X. A ) )
11 velpw 
 |-  ( r e. ~P ( A X. A ) <-> r C_ ( A X. A ) )
12 10 11 sylibr 
 |-  ( ( dom r C_ A /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) -> r e. ~P ( A X. A ) )
13 12 ad2antrr 
 |-  ( ( ( ( dom r C_ A /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) -> r e. ~P ( A X. A ) )
14 13 exlimiv 
 |-  ( E. y ( ( ( dom r C_ A /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) -> r e. ~P ( A X. A ) )
15 14 abssi 
 |-  { r | E. y ( ( ( dom r C_ A /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) } C_ ~P ( A X. A )
16 5 15 eqsstri 
 |-  dom F C_ ~P ( A X. A )
17 funopab4 
 |-  Fun { <. r , y >. | ( ( ( dom r C_ A /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) }
18 1 funeqi 
 |-  ( Fun F <-> Fun { <. r , y >. | ( ( ( dom r C_ A /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) } )
19 17 18 mpbir 
 |-  Fun F
20 1 rneqi 
 |-  ran F = ran { <. r , y >. | ( ( ( dom r C_ A /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) }
21 rnopab 
 |-  ran { <. r , y >. | ( ( ( dom r C_ A /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) } = { y | E. r ( ( ( dom r C_ A /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) }
22 20 21 eqtri 
 |-  ran F = { y | E. r ( ( ( dom r C_ A /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) }
23 breq1 
 |-  ( x = y -> ( x ~<_ A <-> y ~<_ A ) )
24 23 elrab 
 |-  ( y e. { x e. On | x ~<_ A } <-> ( y e. On /\ y ~<_ A ) )
25 f1f 
 |-  ( f : y -1-1-> A -> f : y --> A )
26 25 adantl 
 |-  ( ( y e. On /\ f : y -1-1-> A ) -> f : y --> A )
27 26 frnd 
 |-  ( ( y e. On /\ f : y -1-1-> A ) -> ran f C_ A )
28 resss 
 |-  ( _I |` ran f ) C_ _I
29 ssun2 
 |-  _I C_ ( R u. _I )
30 28 29 sstri 
 |-  ( _I |` ran f ) C_ ( R u. _I )
31 idssxp 
 |-  ( _I |` ran f ) C_ ( ran f X. ran f )
32 30 31 ssini 
 |-  ( _I |` ran f ) C_ ( ( R u. _I ) i^i ( ran f X. ran f ) )
33 32 a1i 
 |-  ( ( y e. On /\ f : y -1-1-> A ) -> ( _I |` ran f ) C_ ( ( R u. _I ) i^i ( ran f X. ran f ) ) )
34 inss2 
 |-  ( ( R u. _I ) i^i ( ran f X. ran f ) ) C_ ( ran f X. ran f )
35 34 a1i 
 |-  ( ( y e. On /\ f : y -1-1-> A ) -> ( ( R u. _I ) i^i ( ran f X. ran f ) ) C_ ( ran f X. ran f ) )
36 27 33 35 3jca 
 |-  ( ( y e. On /\ f : y -1-1-> A ) -> ( ran f C_ A /\ ( _I |` ran f ) C_ ( ( R u. _I ) i^i ( ran f X. ran f ) ) /\ ( ( R u. _I ) i^i ( ran f X. ran f ) ) C_ ( ran f X. ran f ) ) )
37 eloni 
 |-  ( y e. On -> Ord y )
38 ordwe 
 |-  ( Ord y -> _E We y )
39 37 38 syl 
 |-  ( y e. On -> _E We y )
40 39 adantr 
 |-  ( ( y e. On /\ f : y -1-1-> A ) -> _E We y )
41 f1f1orn 
 |-  ( f : y -1-1-> A -> f : y -1-1-onto-> ran f )
42 41 adantl 
 |-  ( ( y e. On /\ f : y -1-1-> A ) -> f : y -1-1-onto-> ran f )
43 f1oiso 
 |-  ( ( f : y -1-1-onto-> ran f /\ R = { <. s , t >. | E. w e. y E. z e. y ( ( s = ( f ` w ) /\ t = ( f ` z ) ) /\ w _E z ) } ) -> f Isom _E , R ( y , ran f ) )
44 42 2 43 sylancl 
 |-  ( ( y e. On /\ f : y -1-1-> A ) -> f Isom _E , R ( y , ran f ) )
45 isores2 
 |-  ( f Isom _E , R ( y , ran f ) <-> f Isom _E , ( R i^i ( ran f X. ran f ) ) ( y , ran f ) )
46 44 45 sylib 
 |-  ( ( y e. On /\ f : y -1-1-> A ) -> f Isom _E , ( R i^i ( ran f X. ran f ) ) ( y , ran f ) )
47 isowe 
 |-  ( f Isom _E , ( R i^i ( ran f X. ran f ) ) ( y , ran f ) -> ( _E We y <-> ( R i^i ( ran f X. ran f ) ) We ran f ) )
48 46 47 syl 
 |-  ( ( y e. On /\ f : y -1-1-> A ) -> ( _E We y <-> ( R i^i ( ran f X. ran f ) ) We ran f ) )
49 40 48 mpbid 
 |-  ( ( y e. On /\ f : y -1-1-> A ) -> ( R i^i ( ran f X. ran f ) ) We ran f )
50 weso 
 |-  ( ( R i^i ( ran f X. ran f ) ) We ran f -> ( R i^i ( ran f X. ran f ) ) Or ran f )
51 49 50 syl 
 |-  ( ( y e. On /\ f : y -1-1-> A ) -> ( R i^i ( ran f X. ran f ) ) Or ran f )
52 inss2 
 |-  ( R i^i ( ran f X. ran f ) ) C_ ( ran f X. ran f )
53 52 brel 
 |-  ( x ( R i^i ( ran f X. ran f ) ) x -> ( x e. ran f /\ x e. ran f ) )
54 53 simpld 
 |-  ( x ( R i^i ( ran f X. ran f ) ) x -> x e. ran f )
55 sonr 
 |-  ( ( ( R i^i ( ran f X. ran f ) ) Or ran f /\ x e. ran f ) -> -. x ( R i^i ( ran f X. ran f ) ) x )
56 51 54 55 syl2an 
 |-  ( ( ( y e. On /\ f : y -1-1-> A ) /\ x ( R i^i ( ran f X. ran f ) ) x ) -> -. x ( R i^i ( ran f X. ran f ) ) x )
57 56 pm2.01da 
 |-  ( ( y e. On /\ f : y -1-1-> A ) -> -. x ( R i^i ( ran f X. ran f ) ) x )
58 57 alrimiv 
 |-  ( ( y e. On /\ f : y -1-1-> A ) -> A. x -. x ( R i^i ( ran f X. ran f ) ) x )
59 intirr 
 |-  ( ( ( R i^i ( ran f X. ran f ) ) i^i _I ) = (/) <-> A. x -. x ( R i^i ( ran f X. ran f ) ) x )
60 58 59 sylibr 
 |-  ( ( y e. On /\ f : y -1-1-> A ) -> ( ( R i^i ( ran f X. ran f ) ) i^i _I ) = (/) )
61 disj3 
 |-  ( ( ( R i^i ( ran f X. ran f ) ) i^i _I ) = (/) <-> ( R i^i ( ran f X. ran f ) ) = ( ( R i^i ( ran f X. ran f ) ) \ _I ) )
62 60 61 sylib 
 |-  ( ( y e. On /\ f : y -1-1-> A ) -> ( R i^i ( ran f X. ran f ) ) = ( ( R i^i ( ran f X. ran f ) ) \ _I ) )
63 weeq1 
 |-  ( ( R i^i ( ran f X. ran f ) ) = ( ( R i^i ( ran f X. ran f ) ) \ _I ) -> ( ( R i^i ( ran f X. ran f ) ) We ran f <-> ( ( R i^i ( ran f X. ran f ) ) \ _I ) We ran f ) )
64 62 63 syl 
 |-  ( ( y e. On /\ f : y -1-1-> A ) -> ( ( R i^i ( ran f X. ran f ) ) We ran f <-> ( ( R i^i ( ran f X. ran f ) ) \ _I ) We ran f ) )
65 49 64 mpbid 
 |-  ( ( y e. On /\ f : y -1-1-> A ) -> ( ( R i^i ( ran f X. ran f ) ) \ _I ) We ran f )
66 37 adantr 
 |-  ( ( y e. On /\ f : y -1-1-> A ) -> Ord y )
67 isoeq3 
 |-  ( ( R i^i ( ran f X. ran f ) ) = ( ( R i^i ( ran f X. ran f ) ) \ _I ) -> ( f Isom _E , ( R i^i ( ran f X. ran f ) ) ( y , ran f ) <-> f Isom _E , ( ( R i^i ( ran f X. ran f ) ) \ _I ) ( y , ran f ) ) )
68 62 67 syl 
 |-  ( ( y e. On /\ f : y -1-1-> A ) -> ( f Isom _E , ( R i^i ( ran f X. ran f ) ) ( y , ran f ) <-> f Isom _E , ( ( R i^i ( ran f X. ran f ) ) \ _I ) ( y , ran f ) ) )
69 46 68 mpbid 
 |-  ( ( y e. On /\ f : y -1-1-> A ) -> f Isom _E , ( ( R i^i ( ran f X. ran f ) ) \ _I ) ( y , ran f ) )
70 vex 
 |-  f e. _V
71 70 rnex 
 |-  ran f e. _V
72 exse 
 |-  ( ran f e. _V -> ( ( R i^i ( ran f X. ran f ) ) \ _I ) Se ran f )
73 71 72 ax-mp 
 |-  ( ( R i^i ( ran f X. ran f ) ) \ _I ) Se ran f
74 eqid 
 |-  OrdIso ( ( ( R i^i ( ran f X. ran f ) ) \ _I ) , ran f ) = OrdIso ( ( ( R i^i ( ran f X. ran f ) ) \ _I ) , ran f )
75 74 oieu 
 |-  ( ( ( ( R i^i ( ran f X. ran f ) ) \ _I ) We ran f /\ ( ( R i^i ( ran f X. ran f ) ) \ _I ) Se ran f ) -> ( ( Ord y /\ f Isom _E , ( ( R i^i ( ran f X. ran f ) ) \ _I ) ( y , ran f ) ) <-> ( y = dom OrdIso ( ( ( R i^i ( ran f X. ran f ) ) \ _I ) , ran f ) /\ f = OrdIso ( ( ( R i^i ( ran f X. ran f ) ) \ _I ) , ran f ) ) ) )
76 65 73 75 sylancl 
 |-  ( ( y e. On /\ f : y -1-1-> A ) -> ( ( Ord y /\ f Isom _E , ( ( R i^i ( ran f X. ran f ) ) \ _I ) ( y , ran f ) ) <-> ( y = dom OrdIso ( ( ( R i^i ( ran f X. ran f ) ) \ _I ) , ran f ) /\ f = OrdIso ( ( ( R i^i ( ran f X. ran f ) ) \ _I ) , ran f ) ) ) )
77 66 69 76 mpbi2and 
 |-  ( ( y e. On /\ f : y -1-1-> A ) -> ( y = dom OrdIso ( ( ( R i^i ( ran f X. ran f ) ) \ _I ) , ran f ) /\ f = OrdIso ( ( ( R i^i ( ran f X. ran f ) ) \ _I ) , ran f ) ) )
78 77 simpld 
 |-  ( ( y e. On /\ f : y -1-1-> A ) -> y = dom OrdIso ( ( ( R i^i ( ran f X. ran f ) ) \ _I ) , ran f ) )
79 71 71 xpex 
 |-  ( ran f X. ran f ) e. _V
80 79 inex2 
 |-  ( ( R u. _I ) i^i ( ran f X. ran f ) ) e. _V
81 sseq1 
 |-  ( r = ( ( R u. _I ) i^i ( ran f X. ran f ) ) -> ( r C_ ( ran f X. ran f ) <-> ( ( R u. _I ) i^i ( ran f X. ran f ) ) C_ ( ran f X. ran f ) ) )
82 34 81 mpbiri 
 |-  ( r = ( ( R u. _I ) i^i ( ran f X. ran f ) ) -> r C_ ( ran f X. ran f ) )
83 dmss 
 |-  ( r C_ ( ran f X. ran f ) -> dom r C_ dom ( ran f X. ran f ) )
84 82 83 syl 
 |-  ( r = ( ( R u. _I ) i^i ( ran f X. ran f ) ) -> dom r C_ dom ( ran f X. ran f ) )
85 dmxpid 
 |-  dom ( ran f X. ran f ) = ran f
86 84 85 sseqtrdi 
 |-  ( r = ( ( R u. _I ) i^i ( ran f X. ran f ) ) -> dom r C_ ran f )
87 dmresi 
 |-  dom ( _I |` ran f ) = ran f
88 sseq2 
 |-  ( r = ( ( R u. _I ) i^i ( ran f X. ran f ) ) -> ( ( _I |` ran f ) C_ r <-> ( _I |` ran f ) C_ ( ( R u. _I ) i^i ( ran f X. ran f ) ) ) )
89 32 88 mpbiri 
 |-  ( r = ( ( R u. _I ) i^i ( ran f X. ran f ) ) -> ( _I |` ran f ) C_ r )
90 dmss 
 |-  ( ( _I |` ran f ) C_ r -> dom ( _I |` ran f ) C_ dom r )
91 89 90 syl 
 |-  ( r = ( ( R u. _I ) i^i ( ran f X. ran f ) ) -> dom ( _I |` ran f ) C_ dom r )
92 87 91 eqsstrrid 
 |-  ( r = ( ( R u. _I ) i^i ( ran f X. ran f ) ) -> ran f C_ dom r )
93 86 92 eqssd 
 |-  ( r = ( ( R u. _I ) i^i ( ran f X. ran f ) ) -> dom r = ran f )
94 93 sseq1d 
 |-  ( r = ( ( R u. _I ) i^i ( ran f X. ran f ) ) -> ( dom r C_ A <-> ran f C_ A ) )
95 93 reseq2d 
 |-  ( r = ( ( R u. _I ) i^i ( ran f X. ran f ) ) -> ( _I |` dom r ) = ( _I |` ran f ) )
96 id 
 |-  ( r = ( ( R u. _I ) i^i ( ran f X. ran f ) ) -> r = ( ( R u. _I ) i^i ( ran f X. ran f ) ) )
97 95 96 sseq12d 
 |-  ( r = ( ( R u. _I ) i^i ( ran f X. ran f ) ) -> ( ( _I |` dom r ) C_ r <-> ( _I |` ran f ) C_ ( ( R u. _I ) i^i ( ran f X. ran f ) ) ) )
98 93 sqxpeqd 
 |-  ( r = ( ( R u. _I ) i^i ( ran f X. ran f ) ) -> ( dom r X. dom r ) = ( ran f X. ran f ) )
99 96 98 sseq12d 
 |-  ( r = ( ( R u. _I ) i^i ( ran f X. ran f ) ) -> ( r C_ ( dom r X. dom r ) <-> ( ( R u. _I ) i^i ( ran f X. ran f ) ) C_ ( ran f X. ran f ) ) )
100 94 97 99 3anbi123d 
 |-  ( r = ( ( R u. _I ) i^i ( ran f X. ran f ) ) -> ( ( dom r C_ A /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) <-> ( ran f C_ A /\ ( _I |` ran f ) C_ ( ( R u. _I ) i^i ( ran f X. ran f ) ) /\ ( ( R u. _I ) i^i ( ran f X. ran f ) ) C_ ( ran f X. ran f ) ) ) )
101 difeq1 
 |-  ( r = ( ( R u. _I ) i^i ( ran f X. ran f ) ) -> ( r \ _I ) = ( ( ( R u. _I ) i^i ( ran f X. ran f ) ) \ _I ) )
102 difun2 
 |-  ( ( R u. _I ) \ _I ) = ( R \ _I )
103 102 ineq1i 
 |-  ( ( ( R u. _I ) \ _I ) i^i ( ran f X. ran f ) ) = ( ( R \ _I ) i^i ( ran f X. ran f ) )
104 indif1 
 |-  ( ( ( R u. _I ) \ _I ) i^i ( ran f X. ran f ) ) = ( ( ( R u. _I ) i^i ( ran f X. ran f ) ) \ _I )
105 indif1 
 |-  ( ( R \ _I ) i^i ( ran f X. ran f ) ) = ( ( R i^i ( ran f X. ran f ) ) \ _I )
106 103 104 105 3eqtr3i 
 |-  ( ( ( R u. _I ) i^i ( ran f X. ran f ) ) \ _I ) = ( ( R i^i ( ran f X. ran f ) ) \ _I )
107 101 106 eqtrdi 
 |-  ( r = ( ( R u. _I ) i^i ( ran f X. ran f ) ) -> ( r \ _I ) = ( ( R i^i ( ran f X. ran f ) ) \ _I ) )
108 107 93 weeq12d 
 |-  ( r = ( ( R u. _I ) i^i ( ran f X. ran f ) ) -> ( ( r \ _I ) We dom r <-> ( ( R i^i ( ran f X. ran f ) ) \ _I ) We ran f ) )
109 100 108 anbi12d 
 |-  ( r = ( ( R u. _I ) i^i ( ran f X. ran f ) ) -> ( ( ( dom r C_ A /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) <-> ( ( ran f C_ A /\ ( _I |` ran f ) C_ ( ( R u. _I ) i^i ( ran f X. ran f ) ) /\ ( ( R u. _I ) i^i ( ran f X. ran f ) ) C_ ( ran f X. ran f ) ) /\ ( ( R i^i ( ran f X. ran f ) ) \ _I ) We ran f ) ) )
110 oieq1 
 |-  ( ( r \ _I ) = ( ( R i^i ( ran f X. ran f ) ) \ _I ) -> OrdIso ( ( r \ _I ) , dom r ) = OrdIso ( ( ( R i^i ( ran f X. ran f ) ) \ _I ) , dom r ) )
111 107 110 syl 
 |-  ( r = ( ( R u. _I ) i^i ( ran f X. ran f ) ) -> OrdIso ( ( r \ _I ) , dom r ) = OrdIso ( ( ( R i^i ( ran f X. ran f ) ) \ _I ) , dom r ) )
112 oieq2 
 |-  ( dom r = ran f -> OrdIso ( ( ( R i^i ( ran f X. ran f ) ) \ _I ) , dom r ) = OrdIso ( ( ( R i^i ( ran f X. ran f ) ) \ _I ) , ran f ) )
113 93 112 syl 
 |-  ( r = ( ( R u. _I ) i^i ( ran f X. ran f ) ) -> OrdIso ( ( ( R i^i ( ran f X. ran f ) ) \ _I ) , dom r ) = OrdIso ( ( ( R i^i ( ran f X. ran f ) ) \ _I ) , ran f ) )
114 111 113 eqtrd 
 |-  ( r = ( ( R u. _I ) i^i ( ran f X. ran f ) ) -> OrdIso ( ( r \ _I ) , dom r ) = OrdIso ( ( ( R i^i ( ran f X. ran f ) ) \ _I ) , ran f ) )
115 114 dmeqd 
 |-  ( r = ( ( R u. _I ) i^i ( ran f X. ran f ) ) -> dom OrdIso ( ( r \ _I ) , dom r ) = dom OrdIso ( ( ( R i^i ( ran f X. ran f ) ) \ _I ) , ran f ) )
116 115 eqeq2d 
 |-  ( r = ( ( R u. _I ) i^i ( ran f X. ran f ) ) -> ( y = dom OrdIso ( ( r \ _I ) , dom r ) <-> y = dom OrdIso ( ( ( R i^i ( ran f X. ran f ) ) \ _I ) , ran f ) ) )
117 109 116 anbi12d 
 |-  ( r = ( ( R u. _I ) i^i ( ran f X. ran f ) ) -> ( ( ( ( dom r C_ A /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) <-> ( ( ( ran f C_ A /\ ( _I |` ran f ) C_ ( ( R u. _I ) i^i ( ran f X. ran f ) ) /\ ( ( R u. _I ) i^i ( ran f X. ran f ) ) C_ ( ran f X. ran f ) ) /\ ( ( R i^i ( ran f X. ran f ) ) \ _I ) We ran f ) /\ y = dom OrdIso ( ( ( R i^i ( ran f X. ran f ) ) \ _I ) , ran f ) ) ) )
118 80 117 spcev 
 |-  ( ( ( ( ran f C_ A /\ ( _I |` ran f ) C_ ( ( R u. _I ) i^i ( ran f X. ran f ) ) /\ ( ( R u. _I ) i^i ( ran f X. ran f ) ) C_ ( ran f X. ran f ) ) /\ ( ( R i^i ( ran f X. ran f ) ) \ _I ) We ran f ) /\ y = dom OrdIso ( ( ( R i^i ( ran f X. ran f ) ) \ _I ) , ran f ) ) -> E. r ( ( ( dom r C_ A /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) )
119 36 65 78 118 syl21anc 
 |-  ( ( y e. On /\ f : y -1-1-> A ) -> E. r ( ( ( dom r C_ A /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) )
120 119 ex 
 |-  ( y e. On -> ( f : y -1-1-> A -> E. r ( ( ( dom r C_ A /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) ) )
121 120 exlimdv 
 |-  ( y e. On -> ( E. f f : y -1-1-> A -> E. r ( ( ( dom r C_ A /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) ) )
122 brdomi 
 |-  ( y ~<_ A -> E. f f : y -1-1-> A )
123 121 122 impel 
 |-  ( ( y e. On /\ y ~<_ A ) -> E. r ( ( ( dom r C_ A /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) )
124 simpr 
 |-  ( ( ( ( dom r C_ A /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) -> y = dom OrdIso ( ( r \ _I ) , dom r ) )
125 vex 
 |-  r e. _V
126 125 dmex 
 |-  dom r e. _V
127 eqid 
 |-  OrdIso ( ( r \ _I ) , dom r ) = OrdIso ( ( r \ _I ) , dom r )
128 127 oion 
 |-  ( dom r e. _V -> dom OrdIso ( ( r \ _I ) , dom r ) e. On )
129 126 128 ax-mp 
 |-  dom OrdIso ( ( r \ _I ) , dom r ) e. On
130 124 129 eqeltrdi 
 |-  ( ( ( ( dom r C_ A /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) -> y e. On )
131 130 adantl 
 |-  ( ( A e. V /\ ( ( ( dom r C_ A /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) ) -> y e. On )
132 simplr 
 |-  ( ( ( ( dom r C_ A /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) -> ( r \ _I ) We dom r )
133 127 oien 
 |-  ( ( dom r e. _V /\ ( r \ _I ) We dom r ) -> dom OrdIso ( ( r \ _I ) , dom r ) ~~ dom r )
134 126 132 133 sylancr 
 |-  ( ( ( ( dom r C_ A /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) -> dom OrdIso ( ( r \ _I ) , dom r ) ~~ dom r )
135 124 134 eqbrtrd 
 |-  ( ( ( ( dom r C_ A /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) -> y ~~ dom r )
136 ssdomg 
 |-  ( A e. V -> ( dom r C_ A -> dom r ~<_ A ) )
137 simpll1 
 |-  ( ( ( ( dom r C_ A /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) -> dom r C_ A )
138 136 137 impel 
 |-  ( ( A e. V /\ ( ( ( dom r C_ A /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) ) -> dom r ~<_ A )
139 endomtr 
 |-  ( ( y ~~ dom r /\ dom r ~<_ A ) -> y ~<_ A )
140 135 138 139 syl2an2 
 |-  ( ( A e. V /\ ( ( ( dom r C_ A /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) ) -> y ~<_ A )
141 131 140 jca 
 |-  ( ( A e. V /\ ( ( ( dom r C_ A /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) ) -> ( y e. On /\ y ~<_ A ) )
142 141 ex 
 |-  ( A e. V -> ( ( ( ( dom r C_ A /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) -> ( y e. On /\ y ~<_ A ) ) )
143 142 exlimdv 
 |-  ( A e. V -> ( E. r ( ( ( dom r C_ A /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) -> ( y e. On /\ y ~<_ A ) ) )
144 123 143 impbid2 
 |-  ( A e. V -> ( ( y e. On /\ y ~<_ A ) <-> E. r ( ( ( dom r C_ A /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) ) )
145 24 144 bitrid 
 |-  ( A e. V -> ( y e. { x e. On | x ~<_ A } <-> E. r ( ( ( dom r C_ A /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) ) )
146 145 eqabdv 
 |-  ( A e. V -> { x e. On | x ~<_ A } = { y | E. r ( ( ( dom r C_ A /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) } )
147 22 146 eqtr4id 
 |-  ( A e. V -> ran F = { x e. On | x ~<_ A } )
148 16 19 147 3pm3.2i 
 |-  ( dom F C_ ~P ( A X. A ) /\ Fun F /\ ( A e. V -> ran F = { x e. On | x ~<_ A } ) )