Metamath Proof Explorer

Theorem cantnf0

Description: The value of the zero function. (Contributed by Mario Carneiro, 30-May-2015)

Ref Expression
Hypotheses cantnfs.s ⊢S=dom⁡ACNFB
cantnfs.a ⊢φ→A∈On
cantnfs.b ⊢φ→B∈On
cantnf0.a ⊢φ→∅∈A
Assertion cantnf0 ⊢φ→ACNFB⁡B×∅=∅

Proof

Step Hyp Ref Expression
1 cantnfs.s ⊢S=dom⁡ACNFB
2 cantnfs.a ⊢φ→A∈On
3 cantnfs.b ⊢φ→B∈On
4 cantnf0.a ⊢φ→∅∈A
5 eqid ⊢OrdIsoEB×∅supp∅=OrdIsoEB×∅supp∅
6 fconst6g ⊢∅∈A→B×∅:B⟶A
7 4 6 syl ⊢φ→B×∅:B⟶A
8 3 4 fczfsuppd ⊢φ→finSupp∅⁡B×∅
9 1 2 3 cantnfs ⊢φ→B×∅∈S↔B×∅:B⟶A∧finSupp∅⁡B×∅
10 7 8 9 mpbir2and ⊢φ→B×∅∈S
11 eqid ⊢seqωk∈V,z∈V⟼A↑𝑜OrdIsoEB×∅supp∅⁡k⋅𝑜B×∅⁡OrdIsoEB×∅supp∅⁡k+𝑜z∅=seqωk∈V,z∈V⟼A↑𝑜OrdIsoEB×∅supp∅⁡k⋅𝑜B×∅⁡OrdIsoEB×∅supp∅⁡k+𝑜z∅
12 1 2 3 5 10 11 cantnfval ⊢φ→ACNFB⁡B×∅=seqωk∈V,z∈V⟼A↑𝑜OrdIsoEB×∅supp∅⁡k⋅𝑜B×∅⁡OrdIsoEB×∅supp∅⁡k+𝑜z∅⁡dom⁡OrdIsoEB×∅supp∅
13 eqidd ⊢φ→B×∅=B×∅
14 0ex ⊢∅∈V
15 fnconstg ⊢∅∈V→B×∅FnB
16 14 15 mp1i ⊢φ→B×∅FnB
17 14 a1i ⊢φ→∅∈V
18 fnsuppeq0 ⊢B×∅FnB∧B∈On∧∅∈V→B×∅supp∅=∅↔B×∅=B×∅
19 16 3 17 18 syl3anc ⊢φ→B×∅supp∅=∅↔B×∅=B×∅
20 13 19 mpbird ⊢φ→B×∅supp∅=∅
21 oieq2 ⊢B×∅supp∅=∅→OrdIsoEB×∅supp∅=OrdIsoE∅
22 20 21 syl ⊢φ→OrdIsoEB×∅supp∅=OrdIsoE∅
23 22 dmeqd ⊢φ→dom⁡OrdIsoEB×∅supp∅=dom⁡OrdIsoE∅
24 we0 ⊢EWe∅
25 eqid ⊢OrdIsoE∅=OrdIsoE∅
26 25 oien ⊢∅∈V∧EWe∅→dom⁡OrdIsoE∅≈∅
27 14 24 26 mp2an ⊢dom⁡OrdIsoE∅≈∅
28 en0 ⊢dom⁡OrdIsoE∅≈∅↔dom⁡OrdIsoE∅=∅
29 27 28 mpbi ⊢dom⁡OrdIsoE∅=∅
30 23 29 eqtrdi ⊢φ→dom⁡OrdIsoEB×∅supp∅=∅
31 30 fveq2d ⊢φ→seqωk∈V,z∈V⟼A↑𝑜OrdIsoEB×∅supp∅⁡k⋅𝑜B×∅⁡OrdIsoEB×∅supp∅⁡k+𝑜z∅⁡dom⁡OrdIsoEB×∅supp∅=seqωk∈V,z∈V⟼A↑𝑜OrdIsoEB×∅supp∅⁡k⋅𝑜B×∅⁡OrdIsoEB×∅supp∅⁡k+𝑜z∅⁡∅
32 11 seqom0g ⊢∅∈V→seqωk∈V,z∈V⟼A↑𝑜OrdIsoEB×∅supp∅⁡k⋅𝑜B×∅⁡OrdIsoEB×∅supp∅⁡k+𝑜z∅⁡∅=∅
33 14 32 mp1i ⊢φ→seqωk∈V,z∈V⟼A↑𝑜OrdIsoEB×∅supp∅⁡k⋅𝑜B×∅⁡OrdIsoEB×∅supp∅⁡k+𝑜z∅⁡∅=∅
34 12 31 33 3eqtrd ⊢φ→ACNFB⁡B×∅=∅