Theorem hsmex3

Description: The set of hereditary size-limited sets, assuming ax-reg , using strict comparison (an easy corollary by separation). (Contributed by Stefan O'Rear, 11-Feb-2015)

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

Proof

Step	Hyp	Ref	Expression
1		sdomdom	|- ( x ~< X -> x ~<_ X )
2	1	ralimi	|- ( A. x e. ( TC ` { s } ) x ~< X -> A. x e. ( TC ` { s } ) x ~<_ X )
3	2	ss2abi	|- { s | A. x e. ( TC ` { s } ) x ~< X } C_ { s | A. x e. ( TC ` { s } ) x ~<_ X }
4		hsmex2	|- ( X e. V -> { s | A. x e. ( TC ` { s } ) x ~<_ X } e. _V )
5		ssexg	|- ( ( { s | A. x e. ( TC ` { s } ) x ~< X } C_ { s | A. x e. ( TC ` { s } ) x ~<_ X } /\ { s | A. x e. ( TC ` { s } ) x ~<_ X } e. _V ) -> { s | A. x e. ( TC ` { s } ) x ~< X } e. _V )
6	3 4 5	sylancr	|- ( X e. V -> { s | A. x e. ( TC ` { s } ) x ~< X } e. _V )