Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 breq2 ⊢a=X→x≼a↔x≼X
2 1 ralbidv ⊢a=X→∀x∈TC⁡sx≼a↔∀x∈TC⁡sx≼X
3 2 rabbidv ⊢a=X→s∈⋃R1On|∀x∈TC⁡sx≼a=s∈⋃R1On|∀x∈TC⁡sx≼X
4 3 eleq1d ⊢a=X→s∈⋃R1On|∀x∈TC⁡sx≼a∈V↔s∈⋃R1On|∀x∈TC⁡sx≼X∈V
5 vex ⊢a∈V
6 eqid ⊢rec⁡d∈V⟼har⁡𝒫a×dhar⁡𝒫a↾ω=rec⁡d∈V⟼har⁡𝒫a×dhar⁡𝒫a↾ω
7 rdgeq2 ⊢e=b→rec⁡f∈V⟼⋃fe=rec⁡f∈V⟼⋃fb
8 unieq ⊢f=c→⋃f=⋃c
9 8 cbvmptv ⊢f∈V⟼⋃f=c∈V⟼⋃c
10 rdgeq1 ⊢f∈V⟼⋃f=c∈V⟼⋃c→rec⁡f∈V⟼⋃fb=rec⁡c∈V⟼⋃cb
11 9 10 ax-mp ⊢rec⁡f∈V⟼⋃fb=rec⁡c∈V⟼⋃cb
12 7 11 eqtrdi ⊢e=b→rec⁡f∈V⟼⋃fe=rec⁡c∈V⟼⋃cb
13 12 reseq1d ⊢e=b→rec⁡f∈V⟼⋃fe↾ω=rec⁡c∈V⟼⋃cb↾ω
14 13 cbvmptv ⊢e∈V⟼rec⁡f∈V⟼⋃fe↾ω=b∈V⟼rec⁡c∈V⟼⋃cb↾ω
15 eqid ⊢s∈⋃R1On|∀x∈TC⁡sx≼a=s∈⋃R1On|∀x∈TC⁡sx≼a
16 eqid ⊢OrdIsoEranke∈V⟼rec⁡f∈V⟼⋃fe↾ω⁡z⁡y=OrdIsoEranke∈V⟼rec⁡f∈V⟼⋃fe↾ω⁡z⁡y
17 5 6 14 15 16 hsmexlem6 ⊢s∈⋃R1On|∀x∈TC⁡sx≼a∈V
18 4 17 vtoclg ⊢X∈V→s∈⋃R1On|∀x∈TC⁡sx≼X∈V