Metamath Proof Explorer

Theorem cantnfdm

Description: The domain of the Cantor normal form function (in later lemmas we will use dom ( A CNF B ) to abbreviate "the set of finitely supported functions from B to A "). (Contributed by Mario Carneiro, 25-May-2015) (Revised by AV, 28-Jun-2019)

Ref Expression
Hypotheses cantnffval.s ⊢ S = g ∈ A B | finSupp ∅⁡ g
cantnffval.a ⊢ φ → A ∈ On
cantnffval.b ⊢ φ → B ∈ On
Assertion cantnfdm ⊢ φ → dom ⁡ A CNF B = S

Proof

Step Hyp Ref Expression
1 cantnffval.s ⊢ S = g ∈ A B | finSupp ∅⁡ g
2 cantnffval.a ⊢ φ → A ∈ On
3 cantnffval.b ⊢ φ → B ∈ On
4 1 2 3 cantnffval ⊢ φ → A CNF B = f ∈ S ⟼ ⦋ OrdIso E f supp ∅ / h⦌ seq ω k ∈ V , z ∈ V ⟼ A ↑ 𝑜 h ⁡ k ⋅ 𝑜 f ⁡ h ⁡ k + 𝑜 z ∅ ⁡ dom ⁡ h
5 4 dmeqd ⊢ φ → dom ⁡ A CNF B = dom ⁡ f ∈ S ⟼ ⦋ OrdIso E f supp ∅ / h⦌ seq ω k ∈ V , z ∈ V ⟼ A ↑ 𝑜 h ⁡ k ⋅ 𝑜 f ⁡ h ⁡ k + 𝑜 z ∅ ⁡ dom ⁡ h
6 fvex ⊢ seq ω k ∈ V , z ∈ V ⟼ A ↑ 𝑜 h ⁡ k ⋅ 𝑜 f ⁡ h ⁡ k + 𝑜 z ∅ ⁡ dom ⁡ h ∈ V
7 6 csbex ⊢ ⦋ OrdIso E f supp ∅ / h⦌ seq ω k ∈ V , z ∈ V ⟼ A ↑ 𝑜 h ⁡ k ⋅ 𝑜 f ⁡ h ⁡ k + 𝑜 z ∅ ⁡ dom ⁡ h ∈ V
8 7 rgenw ⊢ ∀ f ∈ S ⦋ OrdIso E f supp ∅ / h⦌ seq ω k ∈ V , z ∈ V ⟼ A ↑ 𝑜 h ⁡ k ⋅ 𝑜 f ⁡ h ⁡ k + 𝑜 z ∅ ⁡ dom ⁡ h ∈ V
9 dmmptg ⊢ ∀ f ∈ S ⦋ OrdIso E f supp ∅ / h⦌ seq ω k ∈ V , z ∈ V ⟼ A ↑ 𝑜 h ⁡ k ⋅ 𝑜 f ⁡ h ⁡ k + 𝑜 z ∅ ⁡ dom ⁡ h ∈ V → dom ⁡ f ∈ S ⟼ ⦋ OrdIso E f supp ∅ / h⦌ seq ω k ∈ V , z ∈ V ⟼ A ↑ 𝑜 h ⁡ k ⋅ 𝑜 f ⁡ h ⁡ k + 𝑜 z ∅ ⁡ dom ⁡ h = S
10 8 9 ax-mp ⊢ dom ⁡ f ∈ S ⟼ ⦋ OrdIso E f supp ∅ / h⦌ seq ω k ∈ V , z ∈ V ⟼ A ↑ 𝑜 h ⁡ k ⋅ 𝑜 f ⁡ h ⁡ k + 𝑜 z ∅ ⁡ dom ⁡ h = S
11 5 10 eqtrdi ⊢ φ → dom ⁡ A CNF B = S