Theorem hsmex2

Description: The set of hereditary size-limited sets, assuming ax-reg . (Contributed by Stefan O'Rear, 11-Feb-2015)

	Ref	Expression
Assertion	hsmex2	|- ( X e. V -> { s | A. x e. ( TC ` { s } ) x ~<_ X } e. _V )

Proof

Step	Hyp	Ref	Expression
1		unir1	|- U. ( R1 " On ) = _V
2	1	rabeqi	|- { s e. U. ( R1 " On ) | A. x e. ( TC ` { s } ) x ~<_ X } = { s e. _V | A. x e. ( TC ` { s } ) x ~<_ X }
3		rabab	|- { s e. _V | A. x e. ( TC ` { s } ) x ~<_ X } = { s | A. x e. ( TC ` { s } ) x ~<_ X }
4	2 3	eqtr2i	|- { s | A. x e. ( TC ` { s } ) x ~<_ X } = { s e. U. ( R1 " On ) | A. x e. ( TC ` { s } ) x ~<_ X }
5		hsmex	|- ( X e. V -> { s e. U. ( R1 " On ) | A. x e. ( TC ` { s } ) x ~<_ X } e. _V )
6	4 5	eqeltrid	|- ( X e. V -> { s | A. x e. ( TC ` { s } ) x ~<_ X } e. _V )