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∈AB|finSupp∅⁡g
cantnffval.a ⊢φ→A∈On
cantnffval.b ⊢φ→B∈On
Assertion cantnfdm ⊢φ→dom⁡ACNFB=S

Proof

Step Hyp Ref Expression
1 cantnffval.s ⊢S=g∈AB|finSupp∅⁡g
2 cantnffval.a ⊢φ→A∈On
3 cantnffval.b ⊢φ→B∈On
4 1 2 3 cantnffval ⊢φ→ACNFB=f∈S⟼⦋OrdIsoEfsupp∅/h⦌seqωk∈V,z∈V⟼A↑𝑜h⁡k⋅𝑜f⁡h⁡k+𝑜z∅⁡dom⁡h
5 4 dmeqd ⊢φ→dom⁡ACNFB=dom⁡f∈S⟼⦋OrdIsoEfsupp∅/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 ⊢⦋OrdIsoEfsupp∅/h⦌seqωk∈V,z∈V⟼A↑𝑜h⁡k⋅𝑜f⁡h⁡k+𝑜z∅⁡dom⁡h∈V
8 7 rgenw ⊢∀f∈S⦋OrdIsoEfsupp∅/h⦌seqωk∈V,z∈V⟼A↑𝑜h⁡k⋅𝑜f⁡h⁡k+𝑜z∅⁡dom⁡h∈V
9 dmmptg ⊢∀f∈S⦋OrdIsoEfsupp∅/h⦌seqωk∈V,z∈V⟼A↑𝑜h⁡k⋅𝑜f⁡h⁡k+𝑜z∅⁡dom⁡h∈V→dom⁡f∈S⟼⦋OrdIsoEfsupp∅/h⦌seqωk∈V,z∈V⟼A↑𝑜h⁡k⋅𝑜f⁡h⁡k+𝑜z∅⁡dom⁡h=S
10 8 9 ax-mp ⊢dom⁡f∈S⟼⦋OrdIsoEfsupp∅/h⦌seqωk∈V,z∈V⟼A↑𝑜h⁡k⋅𝑜f⁡h⁡k+𝑜z∅⁡dom⁡h=S
11 5 10 eqtrdi ⊢φ→dom⁡ACNFB=S