| 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 2
|
hartogslem1 |
|- ( dom F C_ ~P ( A X. A ) /\ Fun F /\ ( A e. V -> ran F = { x e. On | x ~<_ A } ) ) |
| 4 |
3
|
simp3i |
|- ( A e. V -> ran F = { x e. On | x ~<_ A } ) |
| 5 |
3
|
simp2i |
|- Fun F |
| 6 |
3
|
simp1i |
|- dom F C_ ~P ( A X. A ) |
| 7 |
|
sqxpexg |
|- ( A e. V -> ( A X. A ) e. _V ) |
| 8 |
7
|
pwexd |
|- ( A e. V -> ~P ( A X. A ) e. _V ) |
| 9 |
|
ssexg |
|- ( ( dom F C_ ~P ( A X. A ) /\ ~P ( A X. A ) e. _V ) -> dom F e. _V ) |
| 10 |
6 8 9
|
sylancr |
|- ( A e. V -> dom F e. _V ) |
| 11 |
|
funex |
|- ( ( Fun F /\ dom F e. _V ) -> F e. _V ) |
| 12 |
5 10 11
|
sylancr |
|- ( A e. V -> F e. _V ) |
| 13 |
|
rnexg |
|- ( F e. _V -> ran F e. _V ) |
| 14 |
12 13
|
syl |
|- ( A e. V -> ran F e. _V ) |
| 15 |
4 14
|
eqeltrrd |
|- ( A e. V -> { x e. On | x ~<_ A } e. _V ) |