Theorem ackbij3

Description: The Ackermann bijection is a bijection. This is just a restatement of ackbij2 . (Contributed by Eric Schmidt, 24-Oct-2026)

	Ref	Expression
Assertion	ackbij3	⊢ ackBij : HF ⟶1-1onto ω

Proof

Step	Hyp	Ref	Expression
1		iuneq1	⊢ ( 𝑧 = 𝑢 → ∪ 𝑤 ∈ 𝑧 ( { 𝑤 } × 𝒫 𝑤 ) = ∪ 𝑤 ∈ 𝑢 ( { 𝑤 } × 𝒫 𝑤 ) )
2	1	fveq2d	⊢ ( 𝑧 = 𝑢 → ( card ‘ ∪ 𝑤 ∈ 𝑧 ( { 𝑤 } × 𝒫 𝑤 ) ) = ( card ‘ ∪ 𝑤 ∈ 𝑢 ( { 𝑤 } × 𝒫 𝑤 ) ) )
3	2	cbvmptv	⊢ ( 𝑧 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑤 ∈ 𝑧 ( { 𝑤 } × 𝒫 𝑤 ) ) ) = ( 𝑢 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑤 ∈ 𝑢 ( { 𝑤 } × 𝒫 𝑤 ) ) )
4		sneq	⊢ ( 𝑤 = 𝑣 → { 𝑤 } = { 𝑣 } )
5		pweq	⊢ ( 𝑤 = 𝑣 → 𝒫 𝑤 = 𝒫 𝑣 )
6	4 5	xpeq12d	⊢ ( 𝑤 = 𝑣 → ( { 𝑤 } × 𝒫 𝑤 ) = ( { 𝑣 } × 𝒫 𝑣 ) )
7	6	cbviunv	⊢ ∪ 𝑤 ∈ 𝑢 ( { 𝑤 } × 𝒫 𝑤 ) = ∪ 𝑣 ∈ 𝑢 ( { 𝑣 } × 𝒫 𝑣 )
8	7	fveq2i	⊢ ( card ‘ ∪ 𝑤 ∈ 𝑢 ( { 𝑤 } × 𝒫 𝑤 ) ) = ( card ‘ ∪ 𝑣 ∈ 𝑢 ( { 𝑣 } × 𝒫 𝑣 ) )
9	8	mpteq2i	⊢ ( 𝑢 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑤 ∈ 𝑢 ( { 𝑤 } × 𝒫 𝑤 ) ) ) = ( 𝑢 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑣 ∈ 𝑢 ( { 𝑣 } × 𝒫 𝑣 ) ) )
10	3 9	eqtri	⊢ ( 𝑧 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑤 ∈ 𝑧 ( { 𝑤 } × 𝒫 𝑤 ) ) ) = ( 𝑢 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑣 ∈ 𝑢 ( { 𝑣 } × 𝒫 𝑣 ) ) )
11		dmeq	⊢ ( 𝑥 = 𝑢 → dom 𝑥 = dom 𝑢 )
12	11	pweqd	⊢ ( 𝑥 = 𝑢 → 𝒫 dom 𝑥 = 𝒫 dom 𝑢 )
13		imaeq1	⊢ ( 𝑥 = 𝑢 → ( 𝑥 “ 𝑦 ) = ( 𝑢 “ 𝑦 ) )
14	13	fveq2d	⊢ ( 𝑥 = 𝑢 → ( ( 𝑧 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑤 ∈ 𝑧 ( { 𝑤 } × 𝒫 𝑤 ) ) ) ‘ ( 𝑥 “ 𝑦 ) ) = ( ( 𝑧 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑤 ∈ 𝑧 ( { 𝑤 } × 𝒫 𝑤 ) ) ) ‘ ( 𝑢 “ 𝑦 ) ) )
15	12 14	mpteq12dv	⊢ ( 𝑥 = 𝑢 → ( 𝑦 ∈ 𝒫 dom 𝑥 ↦ ( ( 𝑧 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑤 ∈ 𝑧 ( { 𝑤 } × 𝒫 𝑤 ) ) ) ‘ ( 𝑥 “ 𝑦 ) ) ) = ( 𝑦 ∈ 𝒫 dom 𝑢 ↦ ( ( 𝑧 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑤 ∈ 𝑧 ( { 𝑤 } × 𝒫 𝑤 ) ) ) ‘ ( 𝑢 “ 𝑦 ) ) ) )
16	15	cbvmptv	⊢ ( 𝑥 ∈ V ↦ ( 𝑦 ∈ 𝒫 dom 𝑥 ↦ ( ( 𝑧 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑤 ∈ 𝑧 ( { 𝑤 } × 𝒫 𝑤 ) ) ) ‘ ( 𝑥 “ 𝑦 ) ) ) ) = ( 𝑢 ∈ V ↦ ( 𝑦 ∈ 𝒫 dom 𝑢 ↦ ( ( 𝑧 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑤 ∈ 𝑧 ( { 𝑤 } × 𝒫 𝑤 ) ) ) ‘ ( 𝑢 “ 𝑦 ) ) ) )
17		imaeq2	⊢ ( 𝑦 = 𝑣 → ( 𝑢 “ 𝑦 ) = ( 𝑢 “ 𝑣 ) )
18	17	fveq2d	⊢ ( 𝑦 = 𝑣 → ( ( 𝑧 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑤 ∈ 𝑧 ( { 𝑤 } × 𝒫 𝑤 ) ) ) ‘ ( 𝑢 “ 𝑦 ) ) = ( ( 𝑧 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑤 ∈ 𝑧 ( { 𝑤 } × 𝒫 𝑤 ) ) ) ‘ ( 𝑢 “ 𝑣 ) ) )
19	18	cbvmptv	⊢ ( 𝑦 ∈ 𝒫 dom 𝑢 ↦ ( ( 𝑧 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑤 ∈ 𝑧 ( { 𝑤 } × 𝒫 𝑤 ) ) ) ‘ ( 𝑢 “ 𝑦 ) ) ) = ( 𝑣 ∈ 𝒫 dom 𝑢 ↦ ( ( 𝑧 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑤 ∈ 𝑧 ( { 𝑤 } × 𝒫 𝑤 ) ) ) ‘ ( 𝑢 “ 𝑣 ) ) )
20	19	mpteq2i	⊢ ( 𝑢 ∈ V ↦ ( 𝑦 ∈ 𝒫 dom 𝑢 ↦ ( ( 𝑧 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑤 ∈ 𝑧 ( { 𝑤 } × 𝒫 𝑤 ) ) ) ‘ ( 𝑢 “ 𝑦 ) ) ) ) = ( 𝑢 ∈ V ↦ ( 𝑣 ∈ 𝒫 dom 𝑢 ↦ ( ( 𝑧 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑤 ∈ 𝑧 ( { 𝑤 } × 𝒫 𝑤 ) ) ) ‘ ( 𝑢 “ 𝑣 ) ) ) )
21	16 20	eqtri	⊢ ( 𝑥 ∈ V ↦ ( 𝑦 ∈ 𝒫 dom 𝑥 ↦ ( ( 𝑧 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑤 ∈ 𝑧 ( { 𝑤 } × 𝒫 𝑤 ) ) ) ‘ ( 𝑥 “ 𝑦 ) ) ) ) = ( 𝑢 ∈ V ↦ ( 𝑣 ∈ 𝒫 dom 𝑢 ↦ ( ( 𝑧 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑤 ∈ 𝑧 ( { 𝑤 } × 𝒫 𝑤 ) ) ) ‘ ( 𝑢 “ 𝑣 ) ) ) )
22		df-ackbij	⊢ ackBij = ∪ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑦 ∈ 𝒫 dom 𝑥 ↦ ( ( 𝑧 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑤 ∈ 𝑧 ( { 𝑤 } × 𝒫 𝑤 ) ) ) ‘ ( 𝑥 “ 𝑦 ) ) ) ) , ∅ ) “ ω )
23	10 21 22	ackbij2	⊢ ackBij : HF ⟶1-1onto ω