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