Theorem hsmex

Description: The collection of hereditarily size-limited well-founded sets comprise a set. The proof is that of Randall Holmes at http://math.boisestate.edu/~holmes/holmes/hereditary.pdf , with modifications to use Hartogs' theorem instead of the weak variant (inconsequentially weakening some intermediate results), and making the well-foundedness condition explicit to avoid a direct dependence on ax-reg . (Contributed by Stefan O'Rear, 14-Feb-2015)

	Ref	Expression
Assertion	hsmex	|- ( X e. V -> { s e. U. ( R1 " On ) | A. x e. ( TC ` { s } ) x ~<_ X } e. _V )

Proof

Step	Hyp	Ref	Expression
1		breq2	|- ( a = X -> ( x ~<_ a <-> x ~<_ X ) )
2	1	ralbidv	|- ( a = X -> ( A. x e. ( TC ` { s } ) x ~<_ a <-> A. x e. ( TC ` { s } ) x ~<_ X ) )
3	2	rabbidv	|- ( a = X -> { s e. U. ( R1 " On ) | A. x e. ( TC ` { s } ) x ~<_ a } = { s e. U. ( R1 " On ) | A. x e. ( TC ` { s } ) x ~<_ X } )
4	3	eleq1d	|- ( a = X -> ( { s e. U. ( R1 " On ) | A. x e. ( TC ` { s } ) x ~<_ a } e. _V <-> { s e. U. ( R1 " On ) | A. x e. ( TC ` { s } ) x ~<_ X } e. _V ) )
5		vex	|- a e. _V
6		eqid	|- ( rec ( ( d e. _V |-> ( har ` ~P ( a X. d ) ) ) , ( har ` ~P a ) ) |` _om ) = ( rec ( ( d e. _V |-> ( har ` ~P ( a X. d ) ) ) , ( har ` ~P a ) ) |` _om )
7		rdgeq2	|- ( e = b -> rec ( ( f e. _V |-> U. f ) , e ) = rec ( ( f e. _V |-> U. f ) , b ) )
8		unieq	|- ( f = c -> U. f = U. c )
9	8	cbvmptv	|- ( f e. _V |-> U. f ) = ( c e. _V |-> U. c )
10		rdgeq1	|- ( ( f e. _V |-> U. f ) = ( c e. _V |-> U. c ) -> rec ( ( f e. _V |-> U. f ) , b ) = rec ( ( c e. _V |-> U. c ) , b ) )
11	9 10	ax-mp	|- rec ( ( f e. _V |-> U. f ) , b ) = rec ( ( c e. _V |-> U. c ) , b )
12	7 11	syl6eq	|- ( e = b -> rec ( ( f e. _V |-> U. f ) , e ) = rec ( ( c e. _V |-> U. c ) , b ) )
13	12	reseq1d	|- ( e = b -> ( rec ( ( f e. _V |-> U. f ) , e ) |` _om ) = ( rec ( ( c e. _V |-> U. c ) , b ) |` _om ) )
14	13	cbvmptv	|- ( e e. _V |-> ( rec ( ( f e. _V |-> U. f ) , e ) |` _om ) ) = ( b e. _V |-> ( rec ( ( c e. _V |-> U. c ) , b ) |` _om ) )
15		eqid	|- { s e. U. ( R1 " On ) | A. x e. ( TC ` { s } ) x ~<_ a } = { s e. U. ( R1 " On ) | A. x e. ( TC ` { s } ) x ~<_ a }
16		eqid	|- OrdIso ( _E , ( rank " ( ( ( e e. _V |-> ( rec ( ( f e. _V |-> U. f ) , e ) |` _om ) ) ` z ) ` y ) ) ) = OrdIso ( _E , ( rank " ( ( ( e e. _V |-> ( rec ( ( f e. _V |-> U. f ) , e ) |` _om ) ) ` z ) ` y ) ) )
17	5 6 14 15 16	hsmexlem6	|- { s e. U. ( R1 " On ) | A. x e. ( TC ` { s } ) x ~<_ a } e. _V
18	4 17	vtoclg	|- ( X e. V -> { s e. U. ( R1 " On ) | A. x e. ( TC ` { s } ) x ~<_ X } e. _V )