This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cantnf0

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

Ref Expression
Hypotheses cantnfs.s ⊢ 𝑆 = dom ( 𝐴 CNF 𝐵 )
cantnfs.a ⊢ ( 𝜑 → 𝐴 ∈ On )
cantnfs.b ⊢ ( 𝜑 → 𝐵 ∈ On )
cantnf0.a ⊢ ( 𝜑 → ∅ ∈ 𝐴 )
Assertion cantnf0 ( 𝜑 → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝐵 × { ∅ } ) ) = ∅ )

Proof

Step Hyp Ref Expression
1 cantnfs.s ⊢ 𝑆 = dom ( 𝐴 CNF 𝐵 )
2 cantnfs.a ⊢ ( 𝜑 → 𝐴 ∈ On )
3 cantnfs.b ⊢ ( 𝜑 → 𝐵 ∈ On )
4 cantnf0.a ⊢ ( 𝜑 → ∅ ∈ 𝐴 )
5 eqid ⊢ OrdIso ( E , ( ( 𝐵 × { ∅ } ) supp ∅ ) ) = OrdIso ( E , ( ( 𝐵 × { ∅ } ) supp ∅ ) )
6 fconst6g ⊢ ( ∅ ∈ 𝐴 → ( 𝐵 × { ∅ } ) : 𝐵 ⟶ 𝐴 )
7 4 6 syl ⊢ ( 𝜑 → ( 𝐵 × { ∅ } ) : 𝐵 ⟶ 𝐴 )
8 3 4 fczfsuppd ⊢ ( 𝜑 → ( 𝐵 × { ∅ } ) finSupp ∅ )
9 1 2 3 cantnfs ⊢ ( 𝜑 → ( ( 𝐵 × { ∅ } ) ∈ 𝑆 ↔ ( ( 𝐵 × { ∅ } ) : 𝐵 ⟶ 𝐴 ∧ ( 𝐵 × { ∅ } ) finSupp ∅ ) ) )
10 7 8 9 mpbir2and ⊢ ( 𝜑 → ( 𝐵 × { ∅ } ) ∈ 𝑆 )
11 eqid ⊢ seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( OrdIso ( E , ( ( 𝐵 × { ∅ } ) supp ∅ ) ) ‘ 𝑘 ) ) ·o ( ( 𝐵 × { ∅ } ) ‘ ( OrdIso ( E , ( ( 𝐵 × { ∅ } ) supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) = seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( OrdIso ( E , ( ( 𝐵 × { ∅ } ) supp ∅ ) ) ‘ 𝑘 ) ) ·o ( ( 𝐵 × { ∅ } ) ‘ ( OrdIso ( E , ( ( 𝐵 × { ∅ } ) supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ )
12 1 2 3 5 10 11 cantnfval ⊢ ( 𝜑 → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝐵 × { ∅ } ) ) = ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( OrdIso ( E , ( ( 𝐵 × { ∅ } ) supp ∅ ) ) ‘ 𝑘 ) ) ·o ( ( 𝐵 × { ∅ } ) ‘ ( OrdIso ( E , ( ( 𝐵 × { ∅ } ) supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom OrdIso ( E , ( ( 𝐵 × { ∅ } ) supp ∅ ) ) ) )
13 eqidd ⊢ ( 𝜑 → ( 𝐵 × { ∅ } ) = ( 𝐵 × { ∅ } ) )
14 0ex ⊢ ∅ ∈ V
15 fnconstg ⊢ ( ∅ ∈ V → ( 𝐵 × { ∅ } ) Fn 𝐵 )
16 14 15 mp1i ⊢ ( 𝜑 → ( 𝐵 × { ∅ } ) Fn 𝐵 )
17 14 a1i ⊢ ( 𝜑 → ∅ ∈ V )
18 fnsuppeq0 ⊢ ( ( ( 𝐵 × { ∅ } ) Fn 𝐵 ∧ 𝐵 ∈ On ∧ ∅ ∈ V ) → ( ( ( 𝐵 × { ∅ } ) supp ∅ ) = ∅ ↔ ( 𝐵 × { ∅ } ) = ( 𝐵 × { ∅ } ) ) )
19 16 3 17 18 syl3anc ⊢ ( 𝜑 → ( ( ( 𝐵 × { ∅ } ) supp ∅ ) = ∅ ↔ ( 𝐵 × { ∅ } ) = ( 𝐵 × { ∅ } ) ) )
20 13 19 mpbird ⊢ ( 𝜑 → ( ( 𝐵 × { ∅ } ) supp ∅ ) = ∅ )
21 oieq2 ⊢ ( ( ( 𝐵 × { ∅ } ) supp ∅ ) = ∅ → OrdIso ( E , ( ( 𝐵 × { ∅ } ) supp ∅ ) ) = OrdIso ( E , ∅ ) )
22 20 21 syl ⊢ ( 𝜑 → OrdIso ( E , ( ( 𝐵 × { ∅ } ) supp ∅ ) ) = OrdIso ( E , ∅ ) )
23 22 dmeqd ⊢ ( 𝜑 → dom OrdIso ( E , ( ( 𝐵 × { ∅ } ) 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 , ( ( 𝐵 × { ∅ } ) supp ∅ ) ) = ∅ )
31 30 fveq2d ⊢ ( 𝜑 → ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( OrdIso ( E , ( ( 𝐵 × { ∅ } ) supp ∅ ) ) ‘ 𝑘 ) ) ·o ( ( 𝐵 × { ∅ } ) ‘ ( OrdIso ( E , ( ( 𝐵 × { ∅ } ) supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom OrdIso ( E , ( ( 𝐵 × { ∅ } ) supp ∅ ) ) ) = ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( OrdIso ( E , ( ( 𝐵 × { ∅ } ) supp ∅ ) ) ‘ 𝑘 ) ) ·o ( ( 𝐵 × { ∅ } ) ‘ ( OrdIso ( E , ( ( 𝐵 × { ∅ } ) supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ ∅ ) )
32 11 seqom0g ⊢ ( ∅ ∈ V → ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( OrdIso ( E , ( ( 𝐵 × { ∅ } ) supp ∅ ) ) ‘ 𝑘 ) ) ·o ( ( 𝐵 × { ∅ } ) ‘ ( OrdIso ( E , ( ( 𝐵 × { ∅ } ) supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ ∅ ) = ∅ )
33 14 32 mp1i ⊢ ( 𝜑 → ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( OrdIso ( E , ( ( 𝐵 × { ∅ } ) supp ∅ ) ) ‘ 𝑘 ) ) ·o ( ( 𝐵 × { ∅ } ) ‘ ( OrdIso ( E , ( ( 𝐵 × { ∅ } ) supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ ∅ ) = ∅ )
34 12 31 33 3eqtrd ⊢ ( 𝜑 → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝐵 × { ∅ } ) ) = ∅ )