MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  hartogslem1 Structured version   Unicode version

Theorem hartogslem1 7513
Description: Lemma for hartogs 7515. (Contributed by Mario Carneiro, 14-Jan-2013.) (Revised by Mario Carneiro, 15-May-2015.)
Hypotheses
Ref Expression
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
Ref Expression
hartogslem1  |-  ( dom 
F  C_  ~P ( A  X.  A )  /\  Fun  F  /\  ( A  e.  V  ->  ran  F  =  { x  e.  On  |  x  ~<_  A } ) )
Distinct variable groups:    f, s,
t, w, y, z   
f, r, x, A, y    R, r, x    V, r, y
Allowed substitution hints:    A( z, w, t, s)    R( y, z, w, t, f, s)    F( x, y, z, w, t, f, s, r)    V( x, z, w, t, f, s)

Proof of Theorem hartogslem1
StepHypRef Expression
1 hartogslem.2 . . . . 5  |-  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 ) ) }
21dmeqi 5073 . . . 4  |-  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 ) ) }
3 dmopab 5082 . . . 4  |-  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 ) ) }
42, 3eqtri 2458 . . 3  |-  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 ) ) }
5 simp3 960 . . . . . . . 8  |-  ( ( dom  r  C_  A  /\  (  _I  |`  dom  r
)  C_  r  /\  r  C_  ( dom  r  X.  dom  r ) )  ->  r  C_  ( dom  r  X.  dom  r
) )
6 simp1 958 . . . . . . . . 9  |-  ( ( dom  r  C_  A  /\  (  _I  |`  dom  r
)  C_  r  /\  r  C_  ( dom  r  X.  dom  r ) )  ->  dom  r  C_  A )
7 xpss12 4983 . . . . . . . . 9  |-  ( ( dom  r  C_  A  /\  dom  r  C_  A
)  ->  ( dom  r  X.  dom  r ) 
C_  ( A  X.  A ) )
86, 6, 7syl2anc 644 . . . . . . . 8  |-  ( ( 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
) )
95, 8sstrd 3360 . . . . . . 7  |-  ( ( dom  r  C_  A  /\  (  _I  |`  dom  r
)  C_  r  /\  r  C_  ( dom  r  X.  dom  r ) )  ->  r  C_  ( A  X.  A ) )
10 vex 2961 . . . . . . . 8  |-  r  e. 
_V
1110elpw 3807 . . . . . . 7  |-  ( r  e.  ~P ( A  X.  A )  <->  r  C_  ( A  X.  A
) )
129, 11sylibr 205 . . . . . 6  |-  ( ( dom  r  C_  A  /\  (  _I  |`  dom  r
)  C_  r  /\  r  C_  ( dom  r  X.  dom  r ) )  ->  r  e.  ~P ( A  X.  A
) )
1312ad2antrr 708 . . . . 5  |-  ( ( ( ( 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
) )
1413exlimiv 1645 . . . 4  |-  ( 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
) )
1514abssi 3420 . . 3  |-  { 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 )
164, 15eqsstri 3380 . 2  |-  dom  F  C_ 
~P ( A  X.  A )
17 funopab4 5490 . . 3  |-  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 ) ) }
181funeqi 5476 . . 3  |-  ( 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 ) ) } )
1917, 18mpbir 202 . 2  |-  Fun  F
20 breq1 4217 . . . . . 6  |-  ( x  =  y  ->  (
x  ~<_  A  <->  y  ~<_  A ) )
2120elrab 3094 . . . . 5  |-  ( y  e.  { x  e.  On  |  x  ~<_  A }  <->  ( y  e.  On  /\  y  ~<_  A ) )
22 brdomi 7121 . . . . . . 7  |-  ( y  ~<_  A  ->  E. f 
f : y -1-1-> A
)
23 f1f 5641 . . . . . . . . . . . . . 14  |-  ( f : y -1-1-> A  -> 
f : y --> A )
2423adantl 454 . . . . . . . . . . . . 13  |-  ( ( y  e.  On  /\  f : y -1-1-> A )  ->  f : y --> A )
25 frn 5599 . . . . . . . . . . . . 13  |-  ( f : y --> A  ->  ran  f  C_  A )
2624, 25syl 16 . . . . . . . . . . . 12  |-  ( ( y  e.  On  /\  f : y -1-1-> A )  ->  ran  f  C_  A )
27 resss 5172 . . . . . . . . . . . . . . 15  |-  (  _I  |`  ran  f )  C_  _I
28 ssun2 3513 . . . . . . . . . . . . . . 15  |-  _I  C_  ( R  u.  _I  )
2927, 28sstri 3359 . . . . . . . . . . . . . 14  |-  (  _I  |`  ran  f )  C_  ( R  u.  _I  )
30 f1oi 5715 . . . . . . . . . . . . . . 15  |-  (  _I  |`  ran  f ) : ran  f -1-1-onto-> ran  f
31 f1of 5676 . . . . . . . . . . . . . . 15  |-  ( (  _I  |`  ran  f ) : ran  f -1-1-onto-> ran  f  ->  (  _I  |`  ran  f
) : ran  f --> ran  f )
32 fssxp 5604 . . . . . . . . . . . . . . 15  |-  ( (  _I  |`  ran  f ) : ran  f --> ran  f  ->  (  _I  |` 
ran  f )  C_  ( ran  f  X.  ran  f ) )
3330, 31, 32mp2b 10 . . . . . . . . . . . . . 14  |-  (  _I  |`  ran  f )  C_  ( ran  f  X.  ran  f )
3429, 33ssini 3566 . . . . . . . . . . . . 13  |-  (  _I  |`  ran  f )  C_  ( ( R  u.  _I  )  i^i  ( ran  f  X.  ran  f
) )
3534a1i 11 . . . . . . . . . . . 12  |-  ( ( y  e.  On  /\  f : y -1-1-> A )  ->  (  _I  |`  ran  f
)  C_  ( ( R  u.  _I  )  i^i  ( ran  f  X. 
ran  f ) ) )
36 inss2 3564 . . . . . . . . . . . . 13  |-  ( ( R  u.  _I  )  i^i  ( ran  f  X. 
ran  f ) ) 
C_  ( ran  f  X.  ran  f )
3736a1i 11 . . . . . . . . . . . 12  |-  ( ( y  e.  On  /\  f : y -1-1-> A )  ->  ( ( R  u.  _I  )  i^i  ( ran  f  X. 
ran  f ) ) 
C_  ( ran  f  X.  ran  f ) )
3826, 35, 373jca 1135 . . . . . . . . . . 11  |-  ( ( 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 ) ) )
39 eloni 4593 . . . . . . . . . . . . . . 15  |-  ( y  e.  On  ->  Ord  y )
40 ordwe 4596 . . . . . . . . . . . . . . 15  |-  ( Ord  y  ->  _E  We  y )
4139, 40syl 16 . . . . . . . . . . . . . 14  |-  ( y  e.  On  ->  _E  We  y )
4241adantr 453 . . . . . . . . . . . . 13  |-  ( ( y  e.  On  /\  f : y -1-1-> A )  ->  _E  We  y
)
43 f1f1orn 5687 . . . . . . . . . . . . . . . . 17  |-  ( f : y -1-1-> A  -> 
f : y -1-1-onto-> ran  f
)
4443adantl 454 . . . . . . . . . . . . . . . 16  |-  ( ( y  e.  On  /\  f : y -1-1-> A )  ->  f : y -1-1-onto-> ran  f )
45 hartogslem.3 . . . . . . . . . . . . . . . 16  |-  R  =  { <. s ,  t
>.  |  E. w  e.  y  E. z  e.  y  ( (
s  =  ( f `
 w )  /\  t  =  ( f `  z ) )  /\  w  _E  z ) }
46 f1oiso 6073 . . . . . . . . . . . . . . . 16  |-  ( ( 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 ) )
4744, 45, 46sylancl 645 . . . . . . . . . . . . . . 15  |-  ( ( y  e.  On  /\  f : y -1-1-> A )  ->  f  Isom  _E  ,  R  ( y ,  ran  f ) )
48 isores2 6055 . . . . . . . . . . . . . . 15  |-  ( f 
Isom  _E  ,  R  ( y ,  ran  f )  <->  f  Isom  _E  ,  ( R  i^i  ( ran  f  X.  ran  f ) ) ( y ,  ran  f
) )
4947, 48sylib 190 . . . . . . . . . . . . . 14  |-  ( ( y  e.  On  /\  f : y -1-1-> A )  ->  f  Isom  _E  , 
( R  i^i  ( ran  f  X.  ran  f
) ) ( y ,  ran  f ) )
50 isowe 6071 . . . . . . . . . . . . . 14  |-  ( 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 ) )
5149, 50syl 16 . . . . . . . . . . . . 13  |-  ( ( y  e.  On  /\  f : y -1-1-> A )  ->  (  _E  We  y 
<->  ( R  i^i  ( ran  f  X.  ran  f
) )  We  ran  f ) )
5242, 51mpbid 203 . . . . . . . . . . . 12  |-  ( ( y  e.  On  /\  f : y -1-1-> A )  ->  ( R  i^i  ( ran  f  X.  ran  f ) )  We 
ran  f )
53 weso 4575 . . . . . . . . . . . . . . . . . . 19  |-  ( ( R  i^i  ( ran  f  X.  ran  f
) )  We  ran  f  ->  ( R  i^i  ( ran  f  X.  ran  f ) )  Or 
ran  f )
5452, 53syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ( y  e.  On  /\  f : y -1-1-> A )  ->  ( R  i^i  ( ran  f  X.  ran  f ) )  Or 
ran  f )
55 inss2 3564 . . . . . . . . . . . . . . . . . . . 20  |-  ( R  i^i  ( ran  f  X.  ran  f ) ) 
C_  ( ran  f  X.  ran  f )
5655brel 4928 . . . . . . . . . . . . . . . . . . 19  |-  ( x ( R  i^i  ( ran  f  X.  ran  f
) ) x  -> 
( x  e.  ran  f  /\  x  e.  ran  f ) )
5756simpld 447 . . . . . . . . . . . . . . . . . 18  |-  ( x ( R  i^i  ( ran  f  X.  ran  f
) ) x  ->  x  e.  ran  f )
58 sonr 4526 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 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 )
5954, 57, 58syl2an 465 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 )
6059pm2.01da 431 . . . . . . . . . . . . . . . 16  |-  ( ( y  e.  On  /\  f : y -1-1-> A )  ->  -.  x ( R  i^i  ( ran  f  X.  ran  f ) ) x )
6160alrimiv 1642 . . . . . . . . . . . . . . 15  |-  ( ( y  e.  On  /\  f : y -1-1-> A )  ->  A. x  -.  x
( R  i^i  ( ran  f  X.  ran  f
) ) x )
62 intirr 5254 . . . . . . . . . . . . . . 15  |-  ( ( ( R  i^i  ( ran  f  X.  ran  f
) )  i^i  _I  )  =  (/)  <->  A. x  -.  x ( R  i^i  ( ran  f  X.  ran  f ) ) x )
6361, 62sylibr 205 . . . . . . . . . . . . . 14  |-  ( ( y  e.  On  /\  f : y -1-1-> A )  ->  ( ( R  i^i  ( ran  f  X.  ran  f ) )  i^i  _I  )  =  (/) )
64 disj3 3674 . . . . . . . . . . . . . 14  |-  ( ( ( 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  ) )
6563, 64sylib 190 . . . . . . . . . . . . 13  |-  ( ( 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  ) )
66 weeq1 4572 . . . . . . . . . . . . 13  |-  ( ( 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 ) )
6765, 66syl 16 . . . . . . . . . . . 12  |-  ( ( 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 ) )
6852, 67mpbid 203 . . . . . . . . . . 11  |-  ( ( y  e.  On  /\  f : y -1-1-> A )  ->  ( ( R  i^i  ( ran  f  X.  ran  f ) ) 
\  _I  )  We 
ran  f )
6939adantr 453 . . . . . . . . . . . . 13  |-  ( ( y  e.  On  /\  f : y -1-1-> A )  ->  Ord  y )
70 isoeq3 6043 . . . . . . . . . . . . . . 15  |-  ( ( 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 ) ) )
7165, 70syl 16 . . . . . . . . . . . . . 14  |-  ( ( 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 ) ) )
7249, 71mpbid 203 . . . . . . . . . . . . 13  |-  ( ( y  e.  On  /\  f : y -1-1-> A )  ->  f  Isom  _E  , 
(  ( R  i^i  ( ran  f  X.  ran  f ) )  \  _I  ) ( y ,  ran  f ) )
73 vex 2961 . . . . . . . . . . . . . . . 16  |-  f  e. 
_V
7473rnex 5135 . . . . . . . . . . . . . . 15  |-  ran  f  e.  _V
75 exse 4548 . . . . . . . . . . . . . . 15  |-  ( ran  f  e.  _V  ->  ( ( R  i^i  ( ran  f  X.  ran  f
) )  \  _I  ) Se  ran  f )
7674, 75ax-mp 8 . . . . . . . . . . . . . 14  |-  ( ( R  i^i  ( ran  f  X.  ran  f
) )  \  _I  ) Se  ran  f
77 eqid 2438 . . . . . . . . . . . . . . 15  |- OrdIso ( ( ( R  i^i  ( ran  f  X.  ran  f
) )  \  _I  ) ,  ran  f )  = OrdIso ( ( ( R  i^i  ( ran  f  X.  ran  f
) )  \  _I  ) ,  ran  f )
7877oieu 7510 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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
) ) ) )
7968, 76, 78sylancl 645 . . . . . . . . . . . . 13  |-  ( ( 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
) ) ) )
8069, 72, 79mpbi2and 889 . . . . . . . . . . . 12  |-  ( ( 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
) ) )
8180simpld 447 . . . . . . . . . . 11  |-  ( ( y  e.  On  /\  f : y -1-1-> A )  ->  y  =  dom OrdIso ( ( ( R  i^i  ( ran  f  X.  ran  f ) )  \  _I  ) ,  ran  f
) )
8274, 74xpex 4992 . . . . . . . . . . . . 13  |-  ( ran  f  X.  ran  f
)  e.  _V
8382inex2 4347 . . . . . . . . . . . 12  |-  ( ( R  u.  _I  )  i^i  ( ran  f  X. 
ran  f ) )  e.  _V
84 sseq1 3371 . . . . . . . . . . . . . . . . . . . 20  |-  ( 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 ) ) )
8536, 84mpbiri 226 . . . . . . . . . . . . . . . . . . 19  |-  ( r  =  ( ( R  u.  _I  )  i^i  ( ran  f  X. 
ran  f ) )  ->  r  C_  ( ran  f  X.  ran  f
) )
86 dmss 5071 . . . . . . . . . . . . . . . . . . 19  |-  ( r 
C_  ( ran  f  X.  ran  f )  ->  dom  r  C_  dom  ( ran  f  X.  ran  f
) )
8785, 86syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( r  =  ( ( R  u.  _I  )  i^i  ( ran  f  X. 
ran  f ) )  ->  dom  r  C_  dom  ( ran  f  X. 
ran  f ) )
88 dmxpid 5091 . . . . . . . . . . . . . . . . . 18  |-  dom  ( ran  f  X.  ran  f
)  =  ran  f
8987, 88syl6sseq 3396 . . . . . . . . . . . . . . . . 17  |-  ( r  =  ( ( R  u.  _I  )  i^i  ( ran  f  X. 
ran  f ) )  ->  dom  r  C_  ran  f )
90 dmresi 5198 . . . . . . . . . . . . . . . . . 18  |-  dom  (  _I  |`  ran  f )  =  ran  f
91 sseq2 3372 . . . . . . . . . . . . . . . . . . . 20  |-  ( 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 ) ) ) )
9234, 91mpbiri 226 . . . . . . . . . . . . . . . . . . 19  |-  ( r  =  ( ( R  u.  _I  )  i^i  ( ran  f  X. 
ran  f ) )  ->  (  _I  |`  ran  f
)  C_  r )
93 dmss 5071 . . . . . . . . . . . . . . . . . . 19  |-  ( (  _I  |`  ran  f ) 
C_  r  ->  dom  (  _I  |`  ran  f
)  C_  dom  r )
9492, 93syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( r  =  ( ( R  u.  _I  )  i^i  ( ran  f  X. 
ran  f ) )  ->  dom  (  _I  |` 
ran  f )  C_  dom  r )
9590, 94syl5eqssr 3395 . . . . . . . . . . . . . . . . 17  |-  ( r  =  ( ( R  u.  _I  )  i^i  ( ran  f  X. 
ran  f ) )  ->  ran  f  C_  dom  r )
9689, 95eqssd 3367 . . . . . . . . . . . . . . . 16  |-  ( r  =  ( ( R  u.  _I  )  i^i  ( ran  f  X. 
ran  f ) )  ->  dom  r  =  ran  f )
9796sseq1d 3377 . . . . . . . . . . . . . . 15  |-  ( r  =  ( ( R  u.  _I  )  i^i  ( ran  f  X. 
ran  f ) )  ->  ( dom  r  C_  A  <->  ran  f  C_  A
) )
9896reseq2d 5148 . . . . . . . . . . . . . . . 16  |-  ( r  =  ( ( R  u.  _I  )  i^i  ( ran  f  X. 
ran  f ) )  ->  (  _I  |`  dom  r
)  =  (  _I  |`  ran  f ) )
99 id 21 . . . . . . . . . . . . . . . 16  |-  ( r  =  ( ( R  u.  _I  )  i^i  ( ran  f  X. 
ran  f ) )  ->  r  =  ( ( R  u.  _I  )  i^i  ( ran  f  X.  ran  f ) ) )
10098, 99sseq12d 3379 . . . . . . . . . . . . . . 15  |-  ( 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 ) ) ) )
10196, 96xpeq12d 4905 . . . . . . . . . . . . . . . 16  |-  ( r  =  ( ( R  u.  _I  )  i^i  ( ran  f  X. 
ran  f ) )  ->  ( dom  r  X.  dom  r )  =  ( ran  f  X. 
ran  f ) )
10299, 101sseq12d 3379 . . . . . . . . . . . . . . 15  |-  ( 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 ) ) )
10397, 100, 1023anbi123d 1255 . . . . . . . . . . . . . 14  |-  ( 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 ) ) ) )
104 difeq1 3460 . . . . . . . . . . . . . . . . 17  |-  ( r  =  ( ( R  u.  _I  )  i^i  ( ran  f  X. 
ran  f ) )  ->  ( r  \  _I  )  =  (
( ( R  u.  _I  )  i^i  ( ran  f  X.  ran  f
) )  \  _I  ) )
105 difun2 3709 . . . . . . . . . . . . . . . . . . 19  |-  ( ( R  u.  _I  )  \  _I  )  =  ( R  \  _I  )
106105ineq1i 3540 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( R  u.  _I  )  \  _I  )  i^i  ( ran  f  X. 
ran  f ) )  =  ( ( R 
\  _I  )  i^i  ( ran  f  X. 
ran  f ) )
107 indif1 3587 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( R  u.  _I  )  \  _I  )  i^i  ( ran  f  X. 
ran  f ) )  =  ( ( ( R  u.  _I  )  i^i  ( ran  f  X. 
ran  f ) ) 
\  _I  )
108 indif1 3587 . . . . . . . . . . . . . . . . . 18  |-  ( ( R  \  _I  )  i^i  ( ran  f  X. 
ran  f ) )  =  ( ( R  i^i  ( ran  f  X.  ran  f ) ) 
\  _I  )
109106, 107, 1083eqtr3i 2466 . . . . . . . . . . . . . . . . 17  |-  ( ( ( R  u.  _I  )  i^i  ( ran  f  X.  ran  f ) ) 
\  _I  )  =  ( ( R  i^i  ( ran  f  X.  ran  f ) )  \  _I  )
110104, 109syl6eq 2486 . . . . . . . . . . . . . . . 16  |-  ( r  =  ( ( R  u.  _I  )  i^i  ( ran  f  X. 
ran  f ) )  ->  ( r  \  _I  )  =  (
( R  i^i  ( ran  f  X.  ran  f
) )  \  _I  ) )
111 weeq1 4572 . . . . . . . . . . . . . . . 16  |-  ( ( r  \  _I  )  =  ( ( R  i^i  ( ran  f  X.  ran  f ) ) 
\  _I  )  -> 
( ( r  \  _I  )  We  dom  r 
<->  ( ( R  i^i  ( ran  f  X.  ran  f ) )  \  _I  )  We  dom  r ) )
112110, 111syl 16 . . . . . . . . . . . . . . 15  |-  ( 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 
dom  r ) )
113 weeq2 4573 . . . . . . . . . . . . . . . 16  |-  ( dom  r  =  ran  f  ->  ( ( ( R  i^i  ( ran  f  X.  ran  f ) ) 
\  _I  )  We 
dom  r  <->  ( ( R  i^i  ( ran  f  X.  ran  f ) ) 
\  _I  )  We 
ran  f ) )
11496, 113syl 16 . . . . . . . . . . . . . . 15  |-  ( r  =  ( ( R  u.  _I  )  i^i  ( ran  f  X. 
ran  f ) )  ->  ( ( ( R  i^i  ( ran  f  X.  ran  f
) )  \  _I  )  We  dom  r  <->  ( ( R  i^i  ( ran  f  X.  ran  f ) ) 
\  _I  )  We 
ran  f ) )
115112, 114bitrd 246 . . . . . . . . . . . . . 14  |-  ( 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 ) )
116103, 115anbi12d 693 . . . . . . . . . . . . 13  |-  ( 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 ) ) )
117 oieq1 7483 . . . . . . . . . . . . . . . . 17  |-  ( ( 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 ) )
118110, 117syl 16 . . . . . . . . . . . . . . . 16  |-  ( 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 ) )
119 oieq2 7484 . . . . . . . . . . . . . . . . 17  |-  ( 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 ) )
12096, 119syl 16 . . . . . . . . . . . . . . . 16  |-  ( 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 ) )
121118, 120eqtrd 2470 . . . . . . . . . . . . . . 15  |-  ( 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 ) )
122121dmeqd 5074 . . . . . . . . . . . . . 14  |-  ( 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 ) )
123122eqeq2d 2449 . . . . . . . . . . . . 13  |-  ( 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 ) ) )
124116, 123anbi12d 693 . . . . . . . . . . . 12  |-  ( 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 ) ) ) )
12583, 124spcev 3045 . . . . . . . . . . 11  |-  ( ( ( ( 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 ) ) )
12638, 68, 81, 125syl21anc 1184 . . . . . . . . . 10  |-  ( ( 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 ) ) )
127126ex 425 . . . . . . . . 9  |-  ( 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 ) ) ) )
128127exlimdv 1647 . . . . . . . 8  |-  ( 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 ) ) ) )
129128imp 420 . . . . . . 7  |-  ( ( 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 ) ) )
13022, 129sylan2 462 . . . . . 6  |-  ( ( 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 ) ) )
131 simpr 449 . . . . . . . . . . 11  |-  ( ( ( ( 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 ) )
13210dmex 5134 . . . . . . . . . . . 12  |-  dom  r  e.  _V
133 eqid 2438 . . . . . . . . . . . . 13  |- OrdIso ( ( r  \  _I  ) ,  dom  r )  = OrdIso
( ( r  \  _I  ) ,  dom  r
)
134133oion 7507 . . . . . . . . . . . 12  |-  ( dom  r  e.  _V  ->  dom OrdIso ( ( r  \  _I  ) ,  dom  r
)  e.  On )
135132, 134ax-mp 8 . . . . . . . . . . 11  |-  dom OrdIso ( ( r  \  _I  ) ,  dom  r )  e.  On
136131, 135syl6eqel 2526 . . . . . . . . . 10  |-  ( ( ( ( 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 )
137136adantl 454 . . . . . . . . 9  |-  ( ( 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 )
138 simplr 733 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 )
139133oien 7509 . . . . . . . . . . . . 13  |-  ( ( dom  r  e.  _V  /\  ( r  \  _I  )  We  dom  r )  ->  dom OrdIso ( (
r  \  _I  ) ,  dom  r )  ~~  dom  r )
140132, 138, 139sylancr 646 . . . . . . . . . . . 12  |-  ( ( ( ( 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 )
141131, 140eqbrtrd 4234 . . . . . . . . . . 11  |-  ( ( ( ( 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 )
142141adantl 454 . . . . . . . . . 10  |-  ( ( 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  ~~  dom  r )
143 simpll1 997 . . . . . . . . . . 11  |-  ( ( ( ( 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 )
144 ssdomg 7155 . . . . . . . . . . . 12  |-  ( A  e.  V  ->  ( dom  r  C_  A  ->  dom  r  ~<_  A )
)
145144imp 420 . . . . . . . . . . 11  |-  ( ( A  e.  V  /\  dom  r  C_  A )  ->  dom  r  ~<_  A )
146143, 145sylan2 462 . . . . . . . . . 10  |-  ( ( 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 )
147 endomtr 7167 . . . . . . . . . 10  |-  ( ( y  ~~  dom  r  /\  dom  r  ~<_  A )  ->  y  ~<_  A )
148142, 146, 147syl2anc 644 . . . . . . . . 9  |-  ( ( 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 )
149137, 148jca 520 . . . . . . . 8  |-  ( ( 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 ) )
150149ex 425 . . . . . . 7  |-  ( 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 ) ) )
151150exlimdv 1647 . . . . . 6  |-  ( 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 ) ) )
152130, 151impbid2 197 . . . . 5  |-  ( 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 ) ) ) )
15321, 152syl5bb 250 . . . 4  |-  ( 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 ) ) ) )
154153abbi2dv 2553 . . 3  |-  ( 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 ) ) } )
1551rneqi 5098 . . . 4  |-  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 ) ) }
156 rnopab 5117 . . . 4  |-  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 ) ) }
157155, 156eqtri 2458 . . 3  |-  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 ) ) }
158154, 157syl6reqr 2489 . 2  |-  ( A  e.  V  ->  ran  F  =  { x  e.  On  |  x  ~<_  A } )
15916, 19, 1583pm3.2i 1133 1  |-  ( dom 
F  C_  ~P ( A  X.  A )  /\  Fun  F  /\  ( A  e.  V  ->  ran  F  =  { x  e.  On  |  x  ~<_  A } ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 178    /\ wa 360    /\ w3a 937   A.wal 1550   E.wex 1551    = wceq 1653    e. wcel 1726   {cab 2424   E.wrex 2708   {crab 2711   _Vcvv 2958    \ cdif 3319    u. cun 3320    i^i cin 3321    C_ wss 3322   (/)c0 3630   ~Pcpw 3801   class class class wbr 4214   {copab 4267    _E cep 4494    _I cid 4495    Or wor 4504   Se wse 4541    We wwe 4542   Ord word 4582   Oncon0 4583    X. cxp 4878   dom cdm 4880   ran crn 4881    |` cres 4882   Fun wfun 5450   -->wf 5452   -1-1->wf1 5453   -1-1-onto->wf1o 5455   ` cfv 5456    Isom wiso 5457    ~~ cen 7108    ~<_ cdom 7109  OrdIsocoi 7480
This theorem is referenced by:  hartogslem2  7514  harwdom  7560
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-rep 4322  ax-sep 4332  ax-nul 4340  ax-pow 4379  ax-pr 4405  ax-un 4703
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-reu 2714  df-rmo 2715  df-rab 2716  df-v 2960  df-sbc 3164  df-csb 3254  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-pss 3338  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-tp 3824  df-op 3825  df-uni 4018  df-iun 4097  df-br 4215  df-opab 4269  df-mpt 4270  df-tr 4305  df-eprel 4496  df-id 4500  df-po 4505  df-so 4506  df-fr 4543  df-se 4544  df-we 4545  df-ord 4586  df-on 4587  df-lim 4588  df-suc 4589  df-xp 4886  df-rel 4887  df-cnv 4888  df-co 4889  df-dm 4890  df-rn 4891  df-res 4892  df-ima 4893  df-iota 5420  df-fun 5458  df-fn 5459  df-f 5460  df-f1 5461  df-fo 5462  df-f1o 5463  df-fv 5464  df-isom 5465  df-riota 6551  df-recs 6635  df-en 7112  df-dom 7113  df-oi 7481
  Copyright terms: Public domain W3C validator