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	Could not format assertion : No typesetting found for |- HF ~~ _om with typecode |-

Proof

Step	Hyp	Ref	Expression
1		iuneq1	$$⊢e=a\to \bigcup _{f\in e}\left(\left\{f\right\}\times 𝒫f\right)=\bigcup _{f\in a}\left(\left\{f\right\}\times 𝒫f\right)$$
2		sneq	$$⊢f=b\to \left\{f\right\}=\left\{b\right\}$$
3		pweq	$$⊢f=b\to 𝒫f=𝒫b$$
4	2 3	xpeq12d	$$⊢f=b\to \left\{f\right\}\times 𝒫f=\left\{b\right\}\times 𝒫b$$
5	4	cbviunv	$$⊢\bigcup _{f\in a}\left(\left\{f\right\}\times 𝒫f\right)=\bigcup _{b\in a}\left(\left\{b\right\}\times 𝒫b\right)$$
6	1 5	eqtrdi	$$⊢e=a\to \bigcup _{f\in e}\left(\left\{f\right\}\times 𝒫f\right)=\bigcup _{b\in a}\left(\left\{b\right\}\times 𝒫b\right)$$
7	6	fveq2d	$$⊢e=a\to \mathrm{card}\left(\bigcup _{f\in e}\left(\left\{f\right\}\times 𝒫f\right)\right)=\mathrm{card}\left(\bigcup _{b\in a}\left(\left\{b\right\}\times 𝒫b\right)\right)$$
8	7	cbvmptv	$$⊢\left(e\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)⟼\mathrm{card}\left(\bigcup _{f\in e}\left(\left\{f\right\}\times 𝒫f\right)\right)\right)=\left(a\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)⟼\mathrm{card}\left(\bigcup _{b\in a}\left(\left\{b\right\}\times 𝒫b\right)\right)\right)$$
9		dmeq	$$⊢c=a\to \mathrm{dom}c=\mathrm{dom}a$$
10	9	pweqd	$$⊢c=a\to 𝒫\mathrm{dom}c=𝒫\mathrm{dom}a$$
11		imaeq1	$$⊢c=a\to c\left[d\right]=a\left[d\right]$$
12	11	fveq2d	$$⊢c=a\to \left(e\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)⟼\mathrm{card}\left(\bigcup _{f\in e}\left(\left\{f\right\}\times 𝒫f\right)\right)\right)\left(c\left[d\right]\right)=\left(e\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)⟼\mathrm{card}\left(\bigcup _{f\in e}\left(\left\{f\right\}\times 𝒫f\right)\right)\right)\left(a\left[d\right]\right)$$
13	10 12	mpteq12dv	$$⊢c=a\to \left(d\in 𝒫\mathrm{dom}c⟼\left(e\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)⟼\mathrm{card}\left(\bigcup _{f\in e}\left(\left\{f\right\}\times 𝒫f\right)\right)\right)\left(c\left[d\right]\right)\right)=\left(d\in 𝒫\mathrm{dom}a⟼\left(e\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)⟼\mathrm{card}\left(\bigcup _{f\in e}\left(\left\{f\right\}\times 𝒫f\right)\right)\right)\left(a\left[d\right]\right)\right)$$
14		imaeq2	$$⊢d=b\to a\left[d\right]=a\left[b\right]$$
15	14	fveq2d	$$⊢d=b\to \left(e\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)⟼\mathrm{card}\left(\bigcup _{f\in e}\left(\left\{f\right\}\times 𝒫f\right)\right)\right)\left(a\left[d\right]\right)=\left(e\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)⟼\mathrm{card}\left(\bigcup _{f\in e}\left(\left\{f\right\}\times 𝒫f\right)\right)\right)\left(a\left[b\right]\right)$$
16	15	cbvmptv	$$⊢\left(d\in 𝒫\mathrm{dom}a⟼\left(e\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)⟼\mathrm{card}\left(\bigcup _{f\in e}\left(\left\{f\right\}\times 𝒫f\right)\right)\right)\left(a\left[d\right]\right)\right)=\left(b\in 𝒫\mathrm{dom}a⟼\left(e\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)⟼\mathrm{card}\left(\bigcup _{f\in e}\left(\left\{f\right\}\times 𝒫f\right)\right)\right)\left(a\left[b\right]\right)\right)$$
17	13 16	eqtrdi	$$⊢c=a\to \left(d\in 𝒫\mathrm{dom}c⟼\left(e\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)⟼\mathrm{card}\left(\bigcup _{f\in e}\left(\left\{f\right\}\times 𝒫f\right)\right)\right)\left(c\left[d\right]\right)\right)=\left(b\in 𝒫\mathrm{dom}a⟼\left(e\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)⟼\mathrm{card}\left(\bigcup _{f\in e}\left(\left\{f\right\}\times 𝒫f\right)\right)\right)\left(a\left[b\right]\right)\right)$$
18	17	cbvmptv	$$⊢\left(c\in \mathrm{V}⟼\left(d\in 𝒫\mathrm{dom}c⟼\left(e\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)⟼\mathrm{card}\left(\bigcup _{f\in e}\left(\left\{f\right\}\times 𝒫f\right)\right)\right)\left(c\left[d\right]\right)\right)\right)=\left(a\in \mathrm{V}⟼\left(b\in 𝒫\mathrm{dom}a⟼\left(e\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)⟼\mathrm{card}\left(\bigcup _{f\in e}\left(\left\{f\right\}\times 𝒫f\right)\right)\right)\left(a\left[b\right]\right)\right)\right)$$
19		eqid	$$⊢\bigcup \mathrm{rec}\left(\left(c\in \mathrm{V}⟼\left(d\in 𝒫\mathrm{dom}c⟼\left(e\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)⟼\mathrm{card}\left(\bigcup _{f\in e}\left(\left\{f\right\}\times 𝒫f\right)\right)\right)\left(c\left[d\right]\right)\right)\right),\varnothing \right)\left[\mathrm{\omega }\right]=\bigcup \mathrm{rec}\left(\left(c\in \mathrm{V}⟼\left(d\in 𝒫\mathrm{dom}c⟼\left(e\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)⟼\mathrm{card}\left(\bigcup _{f\in e}\left(\left\{f\right\}\times 𝒫f\right)\right)\right)\left(c\left[d\right]\right)\right)\right),\varnothing \right)\left[\mathrm{\omega }\right]$$
20	8 18 19	ackbij2	Could not format U. ( rec ( ( c e. _V |-> ( d e. ~P dom c |-> ( ( e e. ( ~P _om i^i Fin ) |-> ( card ` U_ f e. e ( { f } X. ~P f ) ) ) ` ( c " d ) ) ) ) , (/) ) " _om ) : HF -1-1-onto-> _om : No typesetting found for |- U. ( rec ( ( c e. _V |-> ( d e. ~P dom c |-> ( ( e e. ( ~P _om i^i Fin ) |-> ( card ` U_ f e. e ( { f } X. ~P f ) ) ) ` ( c " d ) ) ) ) , (/) ) " _om ) : HF -1-1-onto-> _om with typecode |-
21		dfhf2	Could not format HF = ( R1 ` _om ) : No typesetting found for |- HF = ( R1 ` _om ) with typecode |-
22	21	fvexi	Could not format HF e. _V : No typesetting found for |- HF e. _V with typecode |-
23	22	f1oen	Could not format ( U. ( rec ( ( c e. _V |-> ( d e. ~P dom c |-> ( ( e e. ( ~P _om i^i Fin ) |-> ( card ` U_ f e. e ( { f } X. ~P f ) ) ) ` ( c " d ) ) ) ) , (/) ) " _om ) : HF -1-1-onto-> _om -> HF ~~ _om ) : No typesetting found for |- ( U. ( rec ( ( c e. _V |-> ( d e. ~P dom c |-> ( ( e e. ( ~P _om i^i Fin ) |-> ( card ` U_ f e. e ( { f } X. ~P f ) ) ) ` ( c " d ) ) ) ) , (/) ) " _om ) : HF -1-1-onto-> _om -> HF ~~ _om ) with typecode |-
24	20 23	ax-mp	Could not format HF ~~ _om : No typesetting found for |- HF ~~ _om with typecode |-