Metamath Proof Explorer

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∈V→s|∀x∈TC⁡sx≺X∈V

Proof

Step Hyp Ref Expression
1 sdomdom ⊢x≺X→x≼X
2 1 ralimi ⊢∀x∈TC⁡sx≺X→∀x∈TC⁡sx≼X
3 2 ss2abi ⊢s|∀x∈TC⁡sx≺X⊆s|∀x∈TC⁡sx≼X
4 hsmex2 ⊢X∈V→s|∀x∈TC⁡sx≼X∈V
5 ssexg ⊢s|∀x∈TC⁡sx≺X⊆s|∀x∈TC⁡sx≼X∧s|∀x∈TC⁡sx≼X∈V→s|∀x∈TC⁡sx≺X∈V
6 3 4 5 sylancr ⊢X∈V→s|∀x∈TC⁡sx≺X∈V