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

Proof

Step	Hyp	Ref	Expression
1		unir1	⊢ ∪ ( 𝑅1 “ On ) = V
2	1	rabeqi	⊢ { 𝑠 ∈ ∪ ( 𝑅1 “ On ) ∣ ∀ 𝑥 ∈ ( TC ‘ { 𝑠 } ) 𝑥 ≼ 𝑋 } = { 𝑠 ∈ V ∣ ∀ 𝑥 ∈ ( TC ‘ { 𝑠 } ) 𝑥 ≼ 𝑋 }
3		rabab	⊢ { 𝑠 ∈ V ∣ ∀ 𝑥 ∈ ( TC ‘ { 𝑠 } ) 𝑥 ≼ 𝑋 } = { 𝑠 ∣ ∀ 𝑥 ∈ ( TC ‘ { 𝑠 } ) 𝑥 ≼ 𝑋 }
4	2 3	eqtr2i	⊢ { 𝑠 ∣ ∀ 𝑥 ∈ ( TC ‘ { 𝑠 } ) 𝑥 ≼ 𝑋 } = { 𝑠 ∈ ∪ ( 𝑅1 “ On ) ∣ ∀ 𝑥 ∈ ( TC ‘ { 𝑠 } ) 𝑥 ≼ 𝑋 }
5		hsmex	⊢ ( 𝑋 ∈ 𝑉 → { 𝑠 ∈ ∪ ( 𝑅1 “ On ) ∣ ∀ 𝑥 ∈ ( TC ‘ { 𝑠 } ) 𝑥 ≼ 𝑋 } ∈ V )
6	4 5	eqeltrid	⊢ ( 𝑋 ∈ 𝑉 → { 𝑠 ∣ ∀ 𝑥 ∈ ( TC ‘ { 𝑠 } ) 𝑥 ≼ 𝑋 } ∈ V )