Theorem hfom

Description: The set of hereditarily finite sets is countable. See ackbij2 for an explicit bijection that works without Infinity. See also hfomALT . (Contributed by Stefan O'Rear, 18-Nov-2014) Restate using the defined HF symbol. (Revised by Eric Schmidt, 24-Sep-2026)

	Ref	Expression
Assertion	hfom	⊢ HF ≈ ω

Proof

Step	Hyp	Ref	Expression
1		iuneq1	⊢ ( 𝑒 = 𝑎 → ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) = ∪ 𝑓 ∈ 𝑎 ( { 𝑓 } × 𝒫 𝑓 ) )
2		sneq	⊢ ( 𝑓 = 𝑏 → { 𝑓 } = { 𝑏 } )
3		pweq	⊢ ( 𝑓 = 𝑏 → 𝒫 𝑓 = 𝒫 𝑏 )
4	2 3	xpeq12d	⊢ ( 𝑓 = 𝑏 → ( { 𝑓 } × 𝒫 𝑓 ) = ( { 𝑏 } × 𝒫 𝑏 ) )
5	4	cbviunv	⊢ ∪ 𝑓 ∈ 𝑎 ( { 𝑓 } × 𝒫 𝑓 ) = ∪ 𝑏 ∈ 𝑎 ( { 𝑏 } × 𝒫 𝑏 )
6	1 5	eqtrdi	⊢ ( 𝑒 = 𝑎 → ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) = ∪ 𝑏 ∈ 𝑎 ( { 𝑏 } × 𝒫 𝑏 ) )
7	6	fveq2d	⊢ ( 𝑒 = 𝑎 → ( card ‘ ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) ) = ( card ‘ ∪ 𝑏 ∈ 𝑎 ( { 𝑏 } × 𝒫 𝑏 ) ) )
8	7	cbvmptv	⊢ ( 𝑒 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) ) ) = ( 𝑎 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑏 ∈ 𝑎 ( { 𝑏 } × 𝒫 𝑏 ) ) )
9		dmeq	⊢ ( 𝑐 = 𝑎 → dom 𝑐 = dom 𝑎 )
10	9	pweqd	⊢ ( 𝑐 = 𝑎 → 𝒫 dom 𝑐 = 𝒫 dom 𝑎 )
11		imaeq1	⊢ ( 𝑐 = 𝑎 → ( 𝑐 “ 𝑑 ) = ( 𝑎 “ 𝑑 ) )
12	11	fveq2d	⊢ ( 𝑐 = 𝑎 → ( ( 𝑒 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) ) ) ‘ ( 𝑐 “ 𝑑 ) ) = ( ( 𝑒 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) ) ) ‘ ( 𝑎 “ 𝑑 ) ) )
13	10 12	mpteq12dv	⊢ ( 𝑐 = 𝑎 → ( 𝑑 ∈ 𝒫 dom 𝑐 ↦ ( ( 𝑒 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) ) ) ‘ ( 𝑐 “ 𝑑 ) ) ) = ( 𝑑 ∈ 𝒫 dom 𝑎 ↦ ( ( 𝑒 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) ) ) ‘ ( 𝑎 “ 𝑑 ) ) ) )
14		imaeq2	⊢ ( 𝑑 = 𝑏 → ( 𝑎 “ 𝑑 ) = ( 𝑎 “ 𝑏 ) )
15	14	fveq2d	⊢ ( 𝑑 = 𝑏 → ( ( 𝑒 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) ) ) ‘ ( 𝑎 “ 𝑑 ) ) = ( ( 𝑒 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) ) ) ‘ ( 𝑎 “ 𝑏 ) ) )
16	15	cbvmptv	⊢ ( 𝑑 ∈ 𝒫 dom 𝑎 ↦ ( ( 𝑒 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) ) ) ‘ ( 𝑎 “ 𝑑 ) ) ) = ( 𝑏 ∈ 𝒫 dom 𝑎 ↦ ( ( 𝑒 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) ) ) ‘ ( 𝑎 “ 𝑏 ) ) )
17	13 16	eqtrdi	⊢ ( 𝑐 = 𝑎 → ( 𝑑 ∈ 𝒫 dom 𝑐 ↦ ( ( 𝑒 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) ) ) ‘ ( 𝑐 “ 𝑑 ) ) ) = ( 𝑏 ∈ 𝒫 dom 𝑎 ↦ ( ( 𝑒 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) ) ) ‘ ( 𝑎 “ 𝑏 ) ) ) )
18	17	cbvmptv	⊢ ( 𝑐 ∈ V ↦ ( 𝑑 ∈ 𝒫 dom 𝑐 ↦ ( ( 𝑒 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) ) ) ‘ ( 𝑐 “ 𝑑 ) ) ) ) = ( 𝑎 ∈ V ↦ ( 𝑏 ∈ 𝒫 dom 𝑎 ↦ ( ( 𝑒 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) ) ) ‘ ( 𝑎 “ 𝑏 ) ) ) )
19		eqid	⊢ ∪ ( rec ( ( 𝑐 ∈ V ↦ ( 𝑑 ∈ 𝒫 dom 𝑐 ↦ ( ( 𝑒 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) ) ) ‘ ( 𝑐 “ 𝑑 ) ) ) ) , ∅ ) “ ω ) = ∪ ( rec ( ( 𝑐 ∈ V ↦ ( 𝑑 ∈ 𝒫 dom 𝑐 ↦ ( ( 𝑒 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) ) ) ‘ ( 𝑐 “ 𝑑 ) ) ) ) , ∅ ) “ ω )
20	8 18 19	ackbij2	⊢ ∪ ( rec ( ( 𝑐 ∈ V ↦ ( 𝑑 ∈ 𝒫 dom 𝑐 ↦ ( ( 𝑒 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) ) ) ‘ ( 𝑐 “ 𝑑 ) ) ) ) , ∅ ) “ ω ) : HF –1-1-onto→ ω
21		dfhf2	⊢ HF = ( 𝑅1 ‘ ω )
22	21	fvexi	⊢ HF ∈ V
23	22	f1oen	⊢ ( ∪ ( rec ( ( 𝑐 ∈ V ↦ ( 𝑑 ∈ 𝒫 dom 𝑐 ↦ ( ( 𝑒 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑓 ∈ 𝑒 ( { 𝑓 } × 𝒫 𝑓 ) ) ) ‘ ( 𝑐 “ 𝑑 ) ) ) ) , ∅ ) “ ω ) : HF –1-1-onto→ ω → HF ≈ ω )
24	20 23	ax-mp	⊢ HF ≈ ω