Theorem hartogslem2

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

	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	hartogslem2	|- ( A e. V -> { x e. On | x ~<_ A } e. _V )

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 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 )