Definition df-ackbij

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cackbij	⊢ ackBij
1		vx	⊢ 𝑥
2		cvv	⊢ V
3		vy	⊢ 𝑦
4	1	cv	⊢ 𝑥
5	4	cdm	⊢ dom 𝑥
6	5	cpw	⊢ 𝒫 dom 𝑥
7		vz	⊢ 𝑧
8		com	⊢ ω
9	8	cpw	⊢ 𝒫 ω
10		cfn	⊢ Fin
11	9 10	cin	⊢ ( 𝒫 ω ∩ Fin )
12		ccrd	⊢ card
13		vw	⊢ 𝑤
14	7	cv	⊢ 𝑧
15	13	cv	⊢ 𝑤
16	15	csn	⊢ { 𝑤 }
17	15	cpw	⊢ 𝒫 𝑤
18	16 17	cxp	⊢ ( { 𝑤 } × 𝒫 𝑤 )
19	13 14 18	ciun	⊢ ∪ 𝑤 ∈ 𝑧 ( { 𝑤 } × 𝒫 𝑤 )
20	19 12	cfv	⊢ ( card ‘ ∪ 𝑤 ∈ 𝑧 ( { 𝑤 } × 𝒫 𝑤 ) )
21	7 11 20	cmpt	⊢ ( 𝑧 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑤 ∈ 𝑧 ( { 𝑤 } × 𝒫 𝑤 ) ) )
22	3	cv	⊢ 𝑦
23	4 22	cima	⊢ ( 𝑥 “ 𝑦 )
24	23 21	cfv	⊢ ( ( 𝑧 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑤 ∈ 𝑧 ( { 𝑤 } × 𝒫 𝑤 ) ) ) ‘ ( 𝑥 “ 𝑦 ) )
25	3 6 24	cmpt	⊢ ( 𝑦 ∈ 𝒫 dom 𝑥 ↦ ( ( 𝑧 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑤 ∈ 𝑧 ( { 𝑤 } × 𝒫 𝑤 ) ) ) ‘ ( 𝑥 “ 𝑦 ) ) )
26	1 2 25	cmpt	⊢ ( 𝑥 ∈ V ↦ ( 𝑦 ∈ 𝒫 dom 𝑥 ↦ ( ( 𝑧 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑤 ∈ 𝑧 ( { 𝑤 } × 𝒫 𝑤 ) ) ) ‘ ( 𝑥 “ 𝑦 ) ) ) )
27		c0	⊢ ∅
28	26 27	crdg	⊢ rec ( ( 𝑥 ∈ V ↦ ( 𝑦 ∈ 𝒫 dom 𝑥 ↦ ( ( 𝑧 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑤 ∈ 𝑧 ( { 𝑤 } × 𝒫 𝑤 ) ) ) ‘ ( 𝑥 “ 𝑦 ) ) ) ) , ∅ )
29	28 8	cima	⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑦 ∈ 𝒫 dom 𝑥 ↦ ( ( 𝑧 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑤 ∈ 𝑧 ( { 𝑤 } × 𝒫 𝑤 ) ) ) ‘ ( 𝑥 “ 𝑦 ) ) ) ) , ∅ ) “ ω )
30	29	cuni	⊢ ∪ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑦 ∈ 𝒫 dom 𝑥 ↦ ( ( 𝑧 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑤 ∈ 𝑧 ( { 𝑤 } × 𝒫 𝑤 ) ) ) ‘ ( 𝑥 “ 𝑦 ) ) ) ) , ∅ ) “ ω )
31	0 30	wceq	⊢ ackBij = ∪ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑦 ∈ 𝒫 dom 𝑥 ↦ ( ( 𝑧 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑤 ∈ 𝑧 ( { 𝑤 } × 𝒫 𝑤 ) ) ) ‘ ( 𝑥 “ 𝑦 ) ) ) ) , ∅ ) “ ω )