Definition df-ackbij 46217

Description: Define the Ackermann bijection from hereditarily finite sets to ω. This definition is derived from ackbij2 10344. (Contributed by Eric Schmidt, 24-Oct-2026.)

Assertion

Ref	Expression
df-ackbij	⊢ ackBij = ∪ (rec((𝑥 ∈ V ↦ (𝑦 ∈ 𝒫 dom 𝑥 ↦ ((𝑧 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑤 ∈ 𝑧 ({𝑤} × 𝒫 𝑤)))‘(𝑥 “ 𝑦)))), ∅) “ ω)

Distinct variable group:   𝑥,𝑦,𝑧,𝑤

Detailed syntax breakdown of Definition df-ackbij

Step	Hyp	Ref	Expression
1		cackbij 46216	. 2 class ackBij
2		vx	. . . . . 6 setvar 𝑥
3		cvv 3454	. . . . . 6 class V
4		vy	. . . . . . 7 setvar 𝑦
5	2	cv 1569	. . . . . . . . 9 class 𝑥
6	5	cdm 5655	. . . . . . . 8 class dom 𝑥
7	6	cpw 4560	. . . . . . 7 class 𝒫 dom 𝑥
8	4	cv 1569	. . . . . . . . 9 class 𝑦
9	5, 8	cima 5658	. . . . . . . 8 class (𝑥 “ 𝑦)
10		vz	. . . . . . . . 9 setvar 𝑧
11		com 7898	. . . . . . . . . . 11 class ω
12	11	cpw 4560	. . . . . . . . . 10 class 𝒫 ω
13		cfn 8998	. . . . . . . . . 10 class Fin
14	12, 13	cin 4092	. . . . . . . . 9 class (𝒫 ω ∩ Fin)
15		vw	. . . . . . . . . . 11 setvar 𝑤
16	10	cv 1569	. . . . . . . . . . 11 class 𝑧
17	15	cv 1569	. . . . . . . . . . . . 13 class 𝑤
18	17	csn 4588	. . . . . . . . . . . 12 class {𝑤}
19	17	cpw 4560	. . . . . . . . . . . 12 class 𝒫 𝑤
20	18, 19	cxp 5653	. . . . . . . . . . 11 class ({𝑤} × 𝒫 𝑤)
21	15, 16, 20	ciun 4954	. . . . . . . . . 10 class ∪ 𝑤 ∈ 𝑧 ({𝑤} × 𝒫 𝑤)
22		ccrd 10040	. . . . . . . . . 10 class card
23	21, 22	cfv 6555	. . . . . . . . 9 class (card‘∪ 𝑤 ∈ 𝑧 ({𝑤} × 𝒫 𝑤))
24	10, 14, 23	cmpt 5189	. . . . . . . 8 class (𝑧 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑤 ∈ 𝑧 ({𝑤} × 𝒫 𝑤)))
25	9, 24	cfv 6555	. . . . . . 7 class ((𝑧 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑤 ∈ 𝑧 ({𝑤} × 𝒫 𝑤)))‘(𝑥 “ 𝑦))
26	4, 7, 25	cmpt 5189	. . . . . 6 class (𝑦 ∈ 𝒫 dom 𝑥 ↦ ((𝑧 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑤 ∈ 𝑧 ({𝑤} × 𝒫 𝑤)))‘(𝑥 “ 𝑦)))
27	2, 3, 26	cmpt 5189	. . . . 5 class (𝑥 ∈ V ↦ (𝑦 ∈ 𝒫 dom 𝑥 ↦ ((𝑧 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑤 ∈ 𝑧 ({𝑤} × 𝒫 𝑤)))‘(𝑥 “ 𝑦))))
28		c0 4281	. . . . 5 class ∅
29	27, 28	crdg 8442	. . . 4 class rec((𝑥 ∈ V ↦ (𝑦 ∈ 𝒫 dom 𝑥 ↦ ((𝑧 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑤 ∈ 𝑧 ({𝑤} × 𝒫 𝑤)))‘(𝑥 “ 𝑦)))), ∅)
30	29, 11	cima 5658	. . 3 class (rec((𝑥 ∈ V ↦ (𝑦 ∈ 𝒫 dom 𝑥 ↦ ((𝑧 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑤 ∈ 𝑧 ({𝑤} × 𝒫 𝑤)))‘(𝑥 “ 𝑦)))), ∅) “ ω)
31	30	cuni 4870	. 2 class ∪ (rec((𝑥 ∈ V ↦ (𝑦 ∈ 𝒫 dom 𝑥 ↦ ((𝑧 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑤 ∈ 𝑧 ({𝑤} × 𝒫 𝑤)))‘(𝑥 “ 𝑦)))), ∅) “ ω)
32	1, 31	wceq 1570	1 wff ackBij = ∪ (rec((𝑥 ∈ V ↦ (𝑦 ∈ 𝒫 dom 𝑥 ↦ ((𝑧 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑤 ∈ 𝑧 ({𝑤} × 𝒫 𝑤)))‘(𝑥 “ 𝑦)))), ∅) “ ω)

This definition is used by:  ackbij3  46218