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 R1ωω

Proof

Step Hyp Ref Expression
1 omex ωV
2 limom Limω
3 r1lim ωVLimωR1ω=aωR1a
4 1 2 3 mp2an R1ω=aωR1a
5 r1fnon R1FnOn
6 fnfun R1FnOnFunR1
7 funiunfv FunR1aωR1a=R1ω
8 5 6 7 mp2b aωR1a=R1ω
9 4 8 eqtri R1ω=R1ω
10 iuneq1 e=afef×𝒫f=faf×𝒫f
11 sneq f=bf=b
12 pweq f=b𝒫f=𝒫b
13 11 12 xpeq12d f=bf×𝒫f=b×𝒫b
14 13 cbviunv faf×𝒫f=bab×𝒫b
15 10 14 eqtrdi e=afef×𝒫f=bab×𝒫b
16 15 fveq2d e=acardfef×𝒫f=cardbab×𝒫b
17 16 cbvmptv e𝒫ωFincardfef×𝒫f=a𝒫ωFincardbab×𝒫b
18 dmeq c=adomc=doma
19 18 pweqd c=a𝒫domc=𝒫doma
20 imaeq1 c=acd=ad
21 20 fveq2d c=ae𝒫ωFincardfef×𝒫fcd=e𝒫ωFincardfef×𝒫fad
22 19 21 mpteq12dv c=ad𝒫domce𝒫ωFincardfef×𝒫fcd=d𝒫domae𝒫ωFincardfef×𝒫fad
23 imaeq2 d=bad=ab
24 23 fveq2d d=be𝒫ωFincardfef×𝒫fad=e𝒫ωFincardfef×𝒫fab
25 24 cbvmptv d𝒫domae𝒫ωFincardfef×𝒫fad=b𝒫domae𝒫ωFincardfef×𝒫fab
26 22 25 eqtrdi c=ad𝒫domce𝒫ωFincardfef×𝒫fcd=b𝒫domae𝒫ωFincardfef×𝒫fab
27 26 cbvmptv cVd𝒫domce𝒫ωFincardfef×𝒫fcd=aVb𝒫domae𝒫ωFincardfef×𝒫fab
28 eqid reccVd𝒫domce𝒫ωFincardfef×𝒫fcdω=reccVd𝒫domce𝒫ωFincardfef×𝒫fcdω
29 17 27 28 ackbij2 reccVd𝒫domce𝒫ωFincardfef×𝒫fcdω:R1ω1-1 ontoω
30 fvex R1ωV
31 9 30 eqeltrri R1ωV
32 31 f1oen reccVd𝒫domce𝒫ωFincardfef×𝒫fcdω:R1ω1-1 ontoωR1ωω
33 29 32 ax-mp R1ωω
34 9 33 eqbrtri R1ωω