zrninitoringc

Description: The zero ring is not an initial object in the category of unital rings (if the universe contains at least one unital ring different from the zero ring). (Contributed by AV, 18-Apr-2020)

	Ref	Expression
Hypotheses	zrtermoringc.u	$⊢ φ \to U \in V$
	zrtermoringc.c	$⊢ C = RingCat (U)$
	zrtermoringc.z	$⊢ φ \to Z \in (Ring ∖ NzRing)$
	zrtermoringc.e	$⊢ φ \to Z \in U$
	zrninitoringc.e	$⊢ φ \to \exists r \in {Base}_{C} r \in NzRing$
Assertion	zrninitoringc	$⊢ φ \to Z \notin InitO (C)$

Proof

Step	Hyp	Ref	Expression
1		zrtermoringc.u	$⊢ φ \to U \in V$
2		zrtermoringc.c	$⊢ C = RingCat (U)$
3		zrtermoringc.z	$⊢ φ \to Z \in (Ring ∖ NzRing)$
4		zrtermoringc.e	$⊢ φ \to Z \in U$
5		zrninitoringc.e	$⊢ φ \to \exists r \in {Base}_{C} r \in NzRing$
6		eqid	$⊢ {Base}_{C} = {Base}_{C}$
7	1	ad2antrr	$⊢ ((φ \land r \in {Base}_{C}) \land r \in NzRing) \to U \in V$
8		eqid	$⊢ Hom (C) = Hom (C)$
9	3	eldifad	$⊢ φ \to Z \in Ring$
10	4 9	elind	$⊢ φ \to Z \in (U \cap Ring)$
11	2 6 1	ringcbas	$⊢ φ \to {Base}_{C} = U \cap Ring$
12	10 11	eleqtrrd	$⊢ φ \to Z \in {Base}_{C}$
13	12	ad2antrr	$⊢ ((φ \land r \in {Base}_{C}) \land r \in NzRing) \to Z \in {Base}_{C}$
14		simplr	$⊢ ((φ \land r \in {Base}_{C}) \land r \in NzRing) \to r \in {Base}_{C}$
15	2 6 7 8 13 14	ringchom	$⊢ ((φ \land r \in {Base}_{C}) \land r \in NzRing) \to Z Hom (C) r = Z RingHom r$
16	3	adantr	$⊢ (φ \land r \in {Base}_{C}) \to Z \in (Ring ∖ NzRing)$
17		nrhmzr	$⊢ (Z \in (Ring ∖ NzRing) \land r \in NzRing) \to Z RingHom r = \emptyset$
18	16 17	sylan	$⊢ ((φ \land r \in {Base}_{C}) \land r \in NzRing) \to Z RingHom r = \emptyset$
19	15 18	eqtrd	$⊢ ((φ \land r \in {Base}_{C}) \land r \in NzRing) \to Z Hom (C) r = \emptyset$
20		eq0	$⊢ Z Hom (C) r = \emptyset \leftrightarrow \forall h \neg h \in (Z Hom (C) r)$
21	19 20	sylib	$⊢ ((φ \land r \in {Base}_{C}) \land r \in NzRing) \to \forall h \neg h \in (Z Hom (C) r)$
22		alnex	$⊢ \forall h \neg h \in (Z Hom (C) r) \leftrightarrow \neg \exists h h \in (Z Hom (C) r)$
23	21 22	sylib	$⊢ ((φ \land r \in {Base}_{C}) \land r \in NzRing) \to \neg \exists h h \in (Z Hom (C) r)$
24		euex	$⊢ \exists! h h \in (Z Hom (C) r) \to \exists h h \in (Z Hom (C) r)$
25	23 24	nsyl	$⊢ ((φ \land r \in {Base}_{C}) \land r \in NzRing) \to \neg \exists! h h \in (Z Hom (C) r)$
26	25	ex	$⊢ (φ \land r \in {Base}_{C}) \to (r \in NzRing \to \neg \exists! h h \in (Z Hom (C) r))$
27	26	reximdva	$⊢ φ \to (\exists r \in {Base}_{C} r \in NzRing \to \exists r \in {Base}_{C} \neg \exists! h h \in (Z Hom (C) r))$
28	5 27	mpd	$⊢ φ \to \exists r \in {Base}_{C} \neg \exists! h h \in (Z Hom (C) r)$
29		rexnal	$⊢ \exists r \in {Base}_{C} \neg \exists! h h \in (Z Hom (C) r) \leftrightarrow \neg \forall r \in {Base}_{C} \exists! h h \in (Z Hom (C) r)$
30	28 29	sylib	$⊢ φ \to \neg \forall r \in {Base}_{C} \exists! h h \in (Z Hom (C) r)$
31		df-nel	$⊢ Z \notin InitO (C) \leftrightarrow \neg Z \in InitO (C)$
32	2	ringccat	$⊢ U \in V \to C \in Cat$
33	1 32	syl	$⊢ φ \to C \in Cat$
34	6 8 33 12	isinito	$⊢ φ \to (Z \in InitO (C) \leftrightarrow \forall r \in {Base}_{C} \exists! h h \in (Z Hom (C) r))$
35	34	notbid	$⊢ φ \to (\neg Z \in InitO (C) \leftrightarrow \neg \forall r \in {Base}_{C} \exists! h h \in (Z Hom (C) r))$
36	31 35	syl5bb	$⊢ φ \to (Z \notin InitO (C) \leftrightarrow \neg \forall r \in {Base}_{C} \exists! h h \in (Z Hom (C) r))$
37	30 36	mpbird	$⊢ φ \to Z \notin InitO (C)$

Metamath Proof Explorer

Theorem zrninitoringc

Proof