Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 unir1 ⊢ ⋃ R1 On = V
2 1 rabeqi ⊢ s ∈ ⋃ R1 On | ∀ x ∈ TC ⁡ s x ≼ X = s ∈ V | ∀ x ∈ TC ⁡ s x ≼ X
3 rabab ⊢ s ∈ V | ∀ x ∈ TC ⁡ s x ≼ X = s | ∀ x ∈ TC ⁡ s x ≼ X
4 2 3 eqtr2i ⊢ s | ∀ x ∈ TC ⁡ s x ≼ X = s ∈ ⋃ R1 On | ∀ x ∈ TC ⁡ s x ≼ X
5 hsmex ⊢ X ∈ V → s ∈ ⋃ R1 On | ∀ x ∈ TC ⁡ s x ≼ X ∈ V
6 4 5 eqeltrid ⊢ X ∈ V → s | ∀ x ∈ TC ⁡ s x ≼ X ∈ V