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 syl6eq ⊢ φ → 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 × ∅ = ∅