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	⊢ ( 𝑋 ∈ 𝑉 → { 𝑠 ∣ ∀ 𝑥 ∈ ( TC ‘ { 𝑠 } ) 𝑥 ≺ 𝑋 } ∈ V )

Proof

Step	Hyp	Ref	Expression
1		sdomdom	⊢ ( 𝑥 ≺ 𝑋 → 𝑥 ≼ 𝑋 )
2	1	ralimi	⊢ ( ∀ 𝑥 ∈ ( TC ‘ { 𝑠 } ) 𝑥 ≺ 𝑋 → ∀ 𝑥 ∈ ( TC ‘ { 𝑠 } ) 𝑥 ≼ 𝑋 )
3	2	ss2abi	⊢ { 𝑠 ∣ ∀ 𝑥 ∈ ( TC ‘ { 𝑠 } ) 𝑥 ≺ 𝑋 } ⊆ { 𝑠 ∣ ∀ 𝑥 ∈ ( TC ‘ { 𝑠 } ) 𝑥 ≼ 𝑋 }
4		hsmex2	⊢ ( 𝑋 ∈ 𝑉 → { 𝑠 ∣ ∀ 𝑥 ∈ ( TC ‘ { 𝑠 } ) 𝑥 ≼ 𝑋 } ∈ V )
5		ssexg	⊢ ( ( { 𝑠 ∣ ∀ 𝑥 ∈ ( TC ‘ { 𝑠 } ) 𝑥 ≺ 𝑋 } ⊆ { 𝑠 ∣ ∀ 𝑥 ∈ ( TC ‘ { 𝑠 } ) 𝑥 ≼ 𝑋 } ∧ { 𝑠 ∣ ∀ 𝑥 ∈ ( TC ‘ { 𝑠 } ) 𝑥 ≼ 𝑋 } ∈ V ) → { 𝑠 ∣ ∀ 𝑥 ∈ ( TC ‘ { 𝑠 } ) 𝑥 ≺ 𝑋 } ∈ V )
6	3 4 5	sylancr	⊢ ( 𝑋 ∈ 𝑉 → { 𝑠 ∣ ∀ 𝑥 ∈ ( TC ‘ { 𝑠 } ) 𝑥 ≺ 𝑋 } ∈ V )