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

Proof

Step Hyp Ref Expression
1 breq2 ⊢ a = X → x ≼ a ↔ x ≼ X
2 1 ralbidv ⊢ a = X → ∀ x ∈ TC ⁡ s x ≼ a ↔ ∀ x ∈ TC ⁡ s x ≼ X
3 2 rabbidv ⊢ a = X → s ∈ ⋃ R1 On | ∀ x ∈ TC ⁡ s x ≼ a = s ∈ ⋃ R1 On | ∀ x ∈ TC ⁡ s x ≼ X
4 3 eleq1d ⊢ a = X → s ∈ ⋃ R1 On | ∀ x ∈ TC ⁡ s x ≼ a ∈ V ↔ s ∈ ⋃ R1 On | ∀ x ∈ TC ⁡ s x ≼ X ∈ V
5 vex ⊢ a ∈ V
6 eqid ⊢ rec ⁡ d ∈ V ⟼ har ⁡ 𝒫 a × d har ⁡ 𝒫 a ↾ ω = rec ⁡ d ∈ V ⟼ har ⁡ 𝒫 a × d har ⁡ 𝒫 a ↾ ω
7 rdgeq2 ⊢ e = b → rec ⁡ f ∈ V ⟼ ⋃ f e = rec ⁡ f ∈ V ⟼ ⋃ f b
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 ⟼ ⋃ f b = rec ⁡ c ∈ V ⟼ ⋃ c b
11 9 10 ax-mp ⊢ rec ⁡ f ∈ V ⟼ ⋃ f b = rec ⁡ c ∈ V ⟼ ⋃ c b
12 7 11 eqtrdi ⊢ e = b → rec ⁡ f ∈ V ⟼ ⋃ f e = rec ⁡ c ∈ V ⟼ ⋃ c b
13 12 reseq1d ⊢ e = b → rec ⁡ f ∈ V ⟼ ⋃ f e ↾ ω = rec ⁡ c ∈ V ⟼ ⋃ c b ↾ ω
14 13 cbvmptv ⊢ e ∈ V ⟼ rec ⁡ f ∈ V ⟼ ⋃ f e ↾ ω = b ∈ V ⟼ rec ⁡ c ∈ V ⟼ ⋃ c b ↾ ω
15 eqid ⊢ s ∈ ⋃ R1 On | ∀ x ∈ TC ⁡ s x ≼ a = s ∈ ⋃ R1 On | ∀ x ∈ TC ⁡ s x ≼ a
16 eqid ⊢ OrdIso E rank e ∈ V ⟼ rec ⁡ f ∈ V ⟼ ⋃ f e ↾ ω ⁡ z ⁡ y = OrdIso E rank e ∈ V ⟼ rec ⁡ f ∈ V ⟼ ⋃ f e ↾ ω ⁡ z ⁡ y
17 5 6 14 15 16 hsmexlem6 ⊢ s ∈ ⋃ R1 On | ∀ x ∈ TC ⁡ s x ≼ a ∈ V
18 4 17 vtoclg ⊢ X ∈ V → s ∈ ⋃ R1 On | ∀ x ∈ TC ⁡ s x ≼ X ∈ V