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 ⁡ s x ≺ X ∈ V

Proof

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