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 ‘ ω ) ≈ ω