This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem r1om

Description: The set of hereditarily finite sets is countable. See ackbij2 for an explicit bijection that works without Infinity. See also r1omALT . (Contributed by Stefan O'Rear, 18-Nov-2014)

Ref Expression
Assertion r1om ( 𝑅1 ‘ ω ) ≈ ω

Proof

Step Hyp Ref Expression
1 omex ⊢ ω ∈ V
2 limom ⊢ Lim ω
3 r1lim ⊢ ( ( ω ∈ V ∧ Lim ω ) → ( 𝑅1 ‘ ω ) = ∪ 𝑎 ∈ ω ( 𝑅1 ‘ 𝑎 ) )
4 1 2 3 mp2an ⊢ ( 𝑅1 ‘ ω ) = ∪ 𝑎 ∈ ω ( 𝑅1 ‘ 𝑎 )
5 r1fnon ⊢ 𝑅1 Fn On
6 fnfun ⊢ ( 𝑅1 Fn On → Fun 𝑅1 )
7 funiunfv ⊢ ( Fun 𝑅1 → ∪ 𝑎 ∈ ω ( 𝑅1 ‘ 𝑎 ) = ∪ ( 𝑅1 “ ω ) )
8 5 6 7 mp2b ⊢ ∪ 𝑎 ∈ ω ( 𝑅1 ‘ 𝑎 ) = ∪ ( 𝑅1 “ ω )
9 4 8 eqtri ⊢ ( 𝑅1 ‘ ω ) = ∪ ( 𝑅1 “ ω )
10 iuneq1 ⊢ ( 𝑒 = 𝑎 → ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) = ∪ 𝑓 ∈ 𝑎 ( { 𝑓 } × 𝒫 𝑓 ) )
11 sneq ⊢ ( 𝑓 = 𝑏 → { 𝑓 } = { 𝑏 } )
12 pweq ⊢ ( 𝑓 = 𝑏 → 𝒫 𝑓 = 𝒫 𝑏 )
13 11 12 xpeq12d ⊢ ( 𝑓 = 𝑏 → ( { 𝑓 } × 𝒫 𝑓 ) = ( { 𝑏 } × 𝒫 𝑏 ) )
14 13 cbviunv ⊢ ∪ 𝑓 ∈ 𝑎 ( { 𝑓 } × 𝒫 𝑓 ) = ∪ 𝑏 ∈ 𝑎 ( { 𝑏 } × 𝒫 𝑏 )
15 10 14 eqtrdi ⊢ ( 𝑒 = 𝑎 → ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) = ∪ 𝑏 ∈ 𝑎 ( { 𝑏 } × 𝒫 𝑏 ) )
16 15 fveq2d ⊢ ( 𝑒 = 𝑎 → ( card ‘ ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) ) = ( card ‘ ∪ 𝑏 ∈ 𝑎 ( { 𝑏 } × 𝒫 𝑏 ) ) )
17 16 cbvmptv ⊢ ( 𝑒 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) ) ) = ( 𝑎 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑏 ∈ 𝑎 ( { 𝑏 } × 𝒫 𝑏 ) ) )
18 dmeq ⊢ ( 𝑐 = 𝑎 → dom 𝑐 = dom 𝑎 )
19 18 pweqd ⊢ ( 𝑐 = 𝑎 → 𝒫 dom 𝑐 = 𝒫 dom 𝑎 )
20 imaeq1 ⊢ ( 𝑐 = 𝑎 → ( 𝑐 “ 𝑑 ) = ( 𝑎 “ 𝑑 ) )
21 20 fveq2d ⊢ ( 𝑐 = 𝑎 → ( ( 𝑒 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) ) ) ‘ ( 𝑐 “ 𝑑 ) ) = ( ( 𝑒 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) ) ) ‘ ( 𝑎 “ 𝑑 ) ) )
22 19 21 mpteq12dv ⊢ ( 𝑐 = 𝑎 → ( 𝑑 ∈ 𝒫 dom 𝑐 ↦ ( ( 𝑒 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) ) ) ‘ ( 𝑐 “ 𝑑 ) ) ) = ( 𝑑 ∈ 𝒫 dom 𝑎 ↦ ( ( 𝑒 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) ) ) ‘ ( 𝑎 “ 𝑑 ) ) ) )
23 imaeq2 ⊢ ( 𝑑 = 𝑏 → ( 𝑎 “ 𝑑 ) = ( 𝑎 “ 𝑏 ) )
24 23 fveq2d ⊢ ( 𝑑 = 𝑏 → ( ( 𝑒 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) ) ) ‘ ( 𝑎 “ 𝑑 ) ) = ( ( 𝑒 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) ) ) ‘ ( 𝑎 “ 𝑏 ) ) )
25 24 cbvmptv ⊢ ( 𝑑 ∈ 𝒫 dom 𝑎 ↦ ( ( 𝑒 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) ) ) ‘ ( 𝑎 “ 𝑑 ) ) ) = ( 𝑏 ∈ 𝒫 dom 𝑎 ↦ ( ( 𝑒 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) ) ) ‘ ( 𝑎 “ 𝑏 ) ) )
26 22 25 eqtrdi ⊢ ( 𝑐 = 𝑎 → ( 𝑑 ∈ 𝒫 dom 𝑐 ↦ ( ( 𝑒 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) ) ) ‘ ( 𝑐 “ 𝑑 ) ) ) = ( 𝑏 ∈ 𝒫 dom 𝑎 ↦ ( ( 𝑒 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) ) ) ‘ ( 𝑎 “ 𝑏 ) ) ) )
27 26 cbvmptv ⊢ ( 𝑐 ∈ V ↦ ( 𝑑 ∈ 𝒫 dom 𝑐 ↦ ( ( 𝑒 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) ) ) ‘ ( 𝑐 “ 𝑑 ) ) ) ) = ( 𝑎 ∈ V ↦ ( 𝑏 ∈ 𝒫 dom 𝑎 ↦ ( ( 𝑒 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) ) ) ‘ ( 𝑎 “ 𝑏 ) ) ) )
28 eqid ⊢ ∪ ( rec ( ( 𝑐 ∈ V ↦ ( 𝑑 ∈ 𝒫 dom 𝑐 ↦ ( ( 𝑒 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) ) ) ‘ ( 𝑐 “ 𝑑 ) ) ) ) , ∅ ) “ ω ) = ∪ ( rec ( ( 𝑐 ∈ V ↦ ( 𝑑 ∈ 𝒫 dom 𝑐 ↦ ( ( 𝑒 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) ) ) ‘ ( 𝑐 “ 𝑑 ) ) ) ) , ∅ ) “ ω )
29 17 27 28 ackbij2 ⊢ ∪ ( rec ( ( 𝑐 ∈ V ↦ ( 𝑑 ∈ 𝒫 dom 𝑐 ↦ ( ( 𝑒 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) ) ) ‘ ( 𝑐 “ 𝑑 ) ) ) ) , ∅ ) “ ω ) : ∪ ( 𝑅1 “ ω ) –1-1-onto→ ω
30 fvex ⊢ ( 𝑅1 ‘ ω ) ∈ V
31 9 30 eqeltrri ⊢ ∪ ( 𝑅1 “ ω ) ∈ V
32 31 f1oen ⊢ ( ∪ ( rec ( ( 𝑐 ∈ V ↦ ( 𝑑 ∈ 𝒫 dom 𝑐 ↦ ( ( 𝑒 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) ) ) ‘ ( 𝑐 “ 𝑑 ) ) ) ) , ∅ ) “ ω ) : ∪ ( 𝑅1 “ ω ) –1-1-onto→ ω → ∪ ( 𝑅1 “ ω ) ≈ ω )
33 29 32 ax-mp ⊢ ∪ ( 𝑅1 “ ω ) ≈ ω
34 9 33 eqbrtri ⊢ ( 𝑅1 ‘ ω ) ≈ ω