Theorem hsmex

Description: The collection of hereditarily size-limited well-founded sets comprise a set. The proof is that of Randall Holmes at http://math.boisestate.edu/~holmes/holmes/hereditary.pdf , with modifications to use Hartogs' theorem instead of the weak variant (inconsequentially weakening some intermediate results), and making the well-foundedness condition explicit to avoid a direct dependence on ax-reg . (Contributed by Stefan O'Rear, 14-Feb-2015)

	Ref	Expression
Assertion	hsmex	⊢ ( 𝑋 ∈ 𝑉 → { 𝑠 ∈ ∪ ( 𝑅1 “ On ) ∣ ∀ 𝑥 ∈ ( TC ‘ { 𝑠 } ) 𝑥 ≼ 𝑋 } ∈ V )

Proof

Step	Hyp	Ref	Expression
1		breq2	⊢ ( 𝑎 = 𝑋 → ( 𝑥 ≼ 𝑎 ↔ 𝑥 ≼ 𝑋 ) )
2	1	ralbidv	⊢ ( 𝑎 = 𝑋 → ( ∀ 𝑥 ∈ ( TC ‘ { 𝑠 } ) 𝑥 ≼ 𝑎 ↔ ∀ 𝑥 ∈ ( TC ‘ { 𝑠 } ) 𝑥 ≼ 𝑋 ) )
3	2	rabbidv	⊢ ( 𝑎 = 𝑋 → { 𝑠 ∈ ∪ ( 𝑅1 “ On ) ∣ ∀ 𝑥 ∈ ( TC ‘ { 𝑠 } ) 𝑥 ≼ 𝑎 } = { 𝑠 ∈ ∪ ( 𝑅1 “ On ) ∣ ∀ 𝑥 ∈ ( TC ‘ { 𝑠 } ) 𝑥 ≼ 𝑋 } )
4	3	eleq1d	⊢ ( 𝑎 = 𝑋 → ( { 𝑠 ∈ ∪ ( 𝑅1 “ On ) ∣ ∀ 𝑥 ∈ ( TC ‘ { 𝑠 } ) 𝑥 ≼ 𝑎 } ∈ V ↔ { 𝑠 ∈ ∪ ( 𝑅1 “ On ) ∣ ∀ 𝑥 ∈ ( TC ‘ { 𝑠 } ) 𝑥 ≼ 𝑋 } ∈ V ) )
5		vex	⊢ 𝑎 ∈ V
6		eqid	⊢ ( rec ( ( 𝑑 ∈ V ↦ ( har ‘ 𝒫 ( 𝑎 × 𝑑 ) ) ) , ( har ‘ 𝒫 𝑎 ) ) ↾ ω ) = ( rec ( ( 𝑑 ∈ V ↦ ( har ‘ 𝒫 ( 𝑎 × 𝑑 ) ) ) , ( har ‘ 𝒫 𝑎 ) ) ↾ ω )
7		rdgeq2	⊢ ( 𝑒 = 𝑏 → rec ( ( 𝑓 ∈ V ↦ ∪ 𝑓 ) , 𝑒 ) = rec ( ( 𝑓 ∈ V ↦ ∪ 𝑓 ) , 𝑏 ) )
8		unieq	⊢ ( 𝑓 = 𝑐 → ∪ 𝑓 = ∪ 𝑐 )
9	8	cbvmptv	⊢ ( 𝑓 ∈ V ↦ ∪ 𝑓 ) = ( 𝑐 ∈ V ↦ ∪ 𝑐 )
10		rdgeq1	⊢ ( ( 𝑓 ∈ V ↦ ∪ 𝑓 ) = ( 𝑐 ∈ V ↦ ∪ 𝑐 ) → rec ( ( 𝑓 ∈ V ↦ ∪ 𝑓 ) , 𝑏 ) = rec ( ( 𝑐 ∈ V ↦ ∪ 𝑐 ) , 𝑏 ) )
11	9 10	ax-mp	⊢ rec ( ( 𝑓 ∈ V ↦ ∪ 𝑓 ) , 𝑏 ) = rec ( ( 𝑐 ∈ V ↦ ∪ 𝑐 ) , 𝑏 )
12	7 11	eqtrdi	⊢ ( 𝑒 = 𝑏 → rec ( ( 𝑓 ∈ V ↦ ∪ 𝑓 ) , 𝑒 ) = rec ( ( 𝑐 ∈ V ↦ ∪ 𝑐 ) , 𝑏 ) )
13	12	reseq1d	⊢ ( 𝑒 = 𝑏 → ( rec ( ( 𝑓 ∈ V ↦ ∪ 𝑓 ) , 𝑒 ) ↾ ω ) = ( rec ( ( 𝑐 ∈ V ↦ ∪ 𝑐 ) , 𝑏 ) ↾ ω ) )
14	13	cbvmptv	⊢ ( 𝑒 ∈ V ↦ ( rec ( ( 𝑓 ∈ V ↦ ∪ 𝑓 ) , 𝑒 ) ↾ ω ) ) = ( 𝑏 ∈ V ↦ ( rec ( ( 𝑐 ∈ V ↦ ∪ 𝑐 ) , 𝑏 ) ↾ ω ) )
15		eqid	⊢ { 𝑠 ∈ ∪ ( 𝑅1 “ On ) ∣ ∀ 𝑥 ∈ ( TC ‘ { 𝑠 } ) 𝑥 ≼ 𝑎 } = { 𝑠 ∈ ∪ ( 𝑅1 “ On ) ∣ ∀ 𝑥 ∈ ( TC ‘ { 𝑠 } ) 𝑥 ≼ 𝑎 }
16		eqid	⊢ OrdIso ( E , ( rank “ ( ( ( 𝑒 ∈ V ↦ ( rec ( ( 𝑓 ∈ V ↦ ∪ 𝑓 ) , 𝑒 ) ↾ ω ) ) ‘ 𝑧 ) ‘ 𝑦 ) ) ) = OrdIso ( E , ( rank “ ( ( ( 𝑒 ∈ V ↦ ( rec ( ( 𝑓 ∈ V ↦ ∪ 𝑓 ) , 𝑒 ) ↾ ω ) ) ‘ 𝑧 ) ‘ 𝑦 ) ) )
17	5 6 14 15 16	hsmexlem6	⊢ { 𝑠 ∈ ∪ ( 𝑅1 “ On ) ∣ ∀ 𝑥 ∈ ( TC ‘ { 𝑠 } ) 𝑥 ≼ 𝑎 } ∈ V
18	4 17	vtoclg	⊢ ( 𝑋 ∈ 𝑉 → { 𝑠 ∈ ∪ ( 𝑅1 “ On ) ∣ ∀ 𝑥 ∈ ( TC ‘ { 𝑠 } ) 𝑥 ≼ 𝑋 } ∈ V )