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 𝐵 ) ‘ ( 𝐵 × { ∅ } ) ) = ∅ )