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 ( 𝑋𝑉 → { 𝑠 ( 𝑅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 syl6eq ( 𝑒 = 𝑏 → 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 )