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 A CNF B
cantnfs.a φ A On
cantnfs.b φ B On
cantnf0.a φ A
Assertion cantnf0 φ A CNF B B × =

Proof

Step Hyp Ref Expression
1 cantnfs.s S = dom A CNF B
2 cantnfs.a φ A On
3 cantnfs.b φ B On
4 cantnf0.a φ A
5 eqid OrdIso E B × supp = OrdIso E B × 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 𝑜 OrdIso E B × supp k 𝑜 B × OrdIso E B × supp k + 𝑜 z = seq ω k V , z V A 𝑜 OrdIso E B × supp k 𝑜 B × OrdIso E B × supp k + 𝑜 z
12 1 2 3 5 10 11 cantnfval φ A CNF B B × = seq ω k V , z V A 𝑜 OrdIso E B × supp k 𝑜 B × OrdIso E B × supp k + 𝑜 z dom OrdIso E B × supp
13 eqidd φ B × = B ×
14 0ex V
15 fnconstg V B × Fn B
16 14 15 mp1i φ B × Fn B
17 14 a1i φ V
18 fnsuppeq0 B × Fn B 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 = OrdIso E B × supp = OrdIso E
22 20 21 syl φ OrdIso E B × supp = OrdIso E
23 22 dmeqd φ dom OrdIso E B × supp = dom OrdIso E
24 we0 E We
25 eqid OrdIso E = OrdIso E
26 25 oien V E We dom OrdIso E
27 14 24 26 mp2an dom OrdIso E
28 en0 dom OrdIso E dom OrdIso E =
29 27 28 mpbi dom OrdIso E =
30 23 29 eqtrdi φ dom OrdIso E B × supp =
31 30 fveq2d φ seq ω k V , z V A 𝑜 OrdIso E B × supp k 𝑜 B × OrdIso E B × supp k + 𝑜 z dom OrdIso E B × supp = seq ω k V , z V A 𝑜 OrdIso E B × supp k 𝑜 B × OrdIso E B × supp k + 𝑜 z
32 11 seqom0g V seq ω k V , z V A 𝑜 OrdIso E B × supp k 𝑜 B × OrdIso E B × supp k + 𝑜 z =
33 14 32 mp1i φ seq ω k V , z V A 𝑜 OrdIso E B × supp k 𝑜 B × OrdIso E B × supp k + 𝑜 z =
34 12 31 33 3eqtrd φ A CNF B B × =