Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 iuneq1 ⊢ z = u → ⋃ w ∈ z w × 𝒫 w = ⋃ w ∈ u w × 𝒫 w
2 1 fveq2d ⊢ z = u → card ⁡ ⋃ w ∈ z w × 𝒫 w = card ⁡ ⋃ w ∈ u w × 𝒫 w
3 2 cbvmptv ⊢ z ∈ 𝒫 ω ∩ Fin ⟼ card ⁡ ⋃ w ∈ z w × 𝒫 w = u ∈ 𝒫 ω ∩ Fin ⟼ card ⁡ ⋃ w ∈ u w × 𝒫 w
4 sneq ⊢ w = v → w = v
5 pweq ⊢ w = v → 𝒫 w = 𝒫 v
6 4 5 xpeq12d ⊢ w = v → w × 𝒫 w = v × 𝒫 v
7 6 cbviunv ⊢ ⋃ w ∈ u w × 𝒫 w = ⋃ v ∈ u v × 𝒫 v
8 7 fveq2i ⊢ card ⁡ ⋃ w ∈ u w × 𝒫 w = card ⁡ ⋃ v ∈ u v × 𝒫 v
9 8 mpteq2i ⊢ u ∈ 𝒫 ω ∩ Fin ⟼ card ⁡ ⋃ w ∈ u w × 𝒫 w = u ∈ 𝒫 ω ∩ Fin ⟼ card ⁡ ⋃ v ∈ u v × 𝒫 v
10 3 9 eqtri ⊢ z ∈ 𝒫 ω ∩ Fin ⟼ card ⁡ ⋃ w ∈ z w × 𝒫 w = u ∈ 𝒫 ω ∩ Fin ⟼ card ⁡ ⋃ v ∈ u v × 𝒫 v
11 dmeq ⊢ x = u → dom ⁡ x = dom ⁡ u
12 11 pweqd ⊢ x = u → 𝒫 dom ⁡ x = 𝒫 dom ⁡ u
13 imaeq1 ⊢ x = u → x y = u y
14 13 fveq2d ⊢ x = u → z ∈ 𝒫 ω ∩ Fin ⟼ card ⁡ ⋃ w ∈ z w × 𝒫 w ⁡ x y = z ∈ 𝒫 ω ∩ Fin ⟼ card ⁡ ⋃ w ∈ z w × 𝒫 w ⁡ u y
15 12 14 mpteq12dv ⊢ x = u → y ∈ 𝒫 dom ⁡ x ⟼ z ∈ 𝒫 ω ∩ Fin ⟼ card ⁡ ⋃ w ∈ z w × 𝒫 w ⁡ x y = y ∈ 𝒫 dom ⁡ u ⟼ z ∈ 𝒫 ω ∩ Fin ⟼ card ⁡ ⋃ w ∈ z w × 𝒫 w ⁡ u y
16 15 cbvmptv ⊢ x ∈ V ⟼ y ∈ 𝒫 dom ⁡ x ⟼ z ∈ 𝒫 ω ∩ Fin ⟼ card ⁡ ⋃ w ∈ z w × 𝒫 w ⁡ x y = u ∈ V ⟼ y ∈ 𝒫 dom ⁡ u ⟼ z ∈ 𝒫 ω ∩ Fin ⟼ card ⁡ ⋃ w ∈ z w × 𝒫 w ⁡ u y
17 imaeq2 ⊢ y = v → u y = u v
18 17 fveq2d ⊢ y = v → z ∈ 𝒫 ω ∩ Fin ⟼ card ⁡ ⋃ w ∈ z w × 𝒫 w ⁡ u y = z ∈ 𝒫 ω ∩ Fin ⟼ card ⁡ ⋃ w ∈ z w × 𝒫 w ⁡ u v
19 18 cbvmptv ⊢ y ∈ 𝒫 dom ⁡ u ⟼ z ∈ 𝒫 ω ∩ Fin ⟼ card ⁡ ⋃ w ∈ z w × 𝒫 w ⁡ u y = v ∈ 𝒫 dom ⁡ u ⟼ z ∈ 𝒫 ω ∩ Fin ⟼ card ⁡ ⋃ w ∈ z w × 𝒫 w ⁡ u v
20 19 mpteq2i ⊢ u ∈ V ⟼ y ∈ 𝒫 dom ⁡ u ⟼ z ∈ 𝒫 ω ∩ Fin ⟼ card ⁡ ⋃ w ∈ z w × 𝒫 w ⁡ u y = u ∈ V ⟼ v ∈ 𝒫 dom ⁡ u ⟼ z ∈ 𝒫 ω ∩ Fin ⟼ card ⁡ ⋃ w ∈ z w × 𝒫 w ⁡ u v
21 16 20 eqtri ⊢ x ∈ V ⟼ y ∈ 𝒫 dom ⁡ x ⟼ z ∈ 𝒫 ω ∩ Fin ⟼ card ⁡ ⋃ w ∈ z w × 𝒫 w ⁡ x y = u ∈ V ⟼ v ∈ 𝒫 dom ⁡ u ⟼ z ∈ 𝒫 ω ∩ Fin ⟼ card ⁡ ⋃ w ∈ z w × 𝒫 w ⁡ u v
22 df-ackbij Could not format ackBij = U. ( rec ( ( x e. _V |-> ( y e. ~P dom x |-> ( ( z e. ( ~P _om i^i Fin ) |-> ( card ` U_ w e. z ( { w } X. ~P w ) ) ) ` ( x " y ) ) ) ) , (/) ) " _om ) : No typesetting found for |- ackBij = U. ( rec ( ( x e. _V |-> ( y e. ~P dom x |-> ( ( z e. ( ~P _om i^i Fin ) |-> ( card ` U_ w e. z ( { w } X. ~P w ) ) ) ` ( x " y ) ) ) ) , (/) ) " _om ) with typecode |-
23 10 21 22 ackbij2 Could not format ackBij : HF -1-1-onto-> _om : No typesetting found for |- ackBij : HF -1-1-onto-> _om with typecode |-