nzerooringczr

Description: There is no zero object in the category of unital rings (at least in a universe which contains the zero ring and the ring of integers). Example 7.9 (3) in Adamek p. 103. (Contributed by AV, 18-Apr-2020)

	Ref	Expression
Hypotheses	nzerooringczr.u	$⊢ φ \to U \in V$
	nzerooringczr.c	$⊢ C = RingCat (U)$
	nzerooringczr.z	$⊢ φ \to Z \in (Ring ∖ NzRing)$
	nzerooringczr.e	$⊢ φ \to Z \in U$
	nzerooringczr.i	$⊢ φ \to ℤ_{ring} \in U$
Assertion	nzerooringczr	$⊢ φ \to ZeroO (C) = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		nzerooringczr.u	$⊢ φ \to U \in V$
2		nzerooringczr.c	$⊢ C = RingCat (U)$
3		nzerooringczr.z	$⊢ φ \to Z \in (Ring ∖ NzRing)$
4		nzerooringczr.e	$⊢ φ \to Z \in U$
5		nzerooringczr.i	$⊢ φ \to ℤ_{ring} \in U$
6		ax-1	$⊢ ZeroO (C) = \emptyset \to (φ \to ZeroO (C) = \emptyset)$
7		neq0	$⊢ \neg ZeroO (C) = \emptyset \leftrightarrow \exists h h \in ZeroO (C)$
8	2	ringccat	$⊢ U \in V \to C \in Cat$
9	1 8	syl	$⊢ φ \to C \in Cat$
10		iszeroi	$⊢ (C \in Cat \land h \in ZeroO (C)) \to (h \in {Base}_{C} \land (h \in InitO (C) \land h \in TermO (C)))$
11	9 10	sylan	$⊢ (φ \land h \in ZeroO (C)) \to (h \in {Base}_{C} \land (h \in InitO (C) \land h \in TermO (C)))$
12	1 2 3 4	zrtermoringc	$⊢ φ \to Z \in TermO (C)$
13	1 5 2	irinitoringc	$⊢ φ \to ℤ_{ring} \in InitO (C)$
14	9	ad2antrr	$⊢ ((φ \land h \in InitO (C)) \land ℤ_{ring} \in InitO (C)) \to C \in Cat$
15		simplr	$⊢ ((φ \land h \in InitO (C)) \land ℤ_{ring} \in InitO (C)) \to h \in InitO (C)$
16		simpr	$⊢ ((φ \land h \in InitO (C)) \land ℤ_{ring} \in InitO (C)) \to ℤ_{ring} \in InitO (C)$
17	14 15 16	initoeu1w	$⊢ ((φ \land h \in InitO (C)) \land ℤ_{ring} \in InitO (C)) \to h ≃_{𝑐} (C) ℤ_{ring}$
18	9	ad2antrr	$⊢ ((φ \land h \in TermO (C)) \land Z \in TermO (C)) \to C \in Cat$
19		simpr	$⊢ ((φ \land h \in TermO (C)) \land Z \in TermO (C)) \to Z \in TermO (C)$
20		simplr	$⊢ ((φ \land h \in TermO (C)) \land Z \in TermO (C)) \to h \in TermO (C)$
21	18 19 20	termoeu1w	$⊢ ((φ \land h \in TermO (C)) \land Z \in TermO (C)) \to Z ≃_{𝑐} (C) h$
22		cictr	$⊢ (C \in Cat \land Z ≃_{𝑐} (C) h \land h ≃_{𝑐} (C) ℤ_{ring}) \to Z ≃_{𝑐} (C) ℤ_{ring}$
23	9 22	syl3an1	$⊢ (φ \land Z ≃_{𝑐} (C) h \land h ≃_{𝑐} (C) ℤ_{ring}) \to Z ≃_{𝑐} (C) ℤ_{ring}$
24		eqid	$⊢ Iso (C) = Iso (C)$
25		eqid	$⊢ {Base}_{C} = {Base}_{C}$
26	3	eldifad	$⊢ φ \to Z \in Ring$
27	4 26	elind	$⊢ φ \to Z \in (U \cap Ring)$
28	2 25 1	ringcbas	$⊢ φ \to {Base}_{C} = U \cap Ring$
29	27 28	eleqtrrd	$⊢ φ \to Z \in {Base}_{C}$
30		zringring	$⊢ ℤ_{ring} \in Ring$
31	30	a1i	$⊢ φ \to ℤ_{ring} \in Ring$
32	5 31	elind	$⊢ φ \to ℤ_{ring} \in (U \cap Ring)$
33	32 28	eleqtrrd	$⊢ φ \to ℤ_{ring} \in {Base}_{C}$
34	24 25 9 29 33	cic	$⊢ φ \to (Z ≃_{𝑐} (C) ℤ_{ring} \leftrightarrow \exists f f \in (Z Iso (C) ℤ_{ring}))$
35		n0	$⊢ Z Iso (C) ℤ_{ring} \neq \emptyset \leftrightarrow \exists f f \in (Z Iso (C) ℤ_{ring})$
36		eqid	$⊢ Hom (C) = Hom (C)$
37	25 36 24 9 29 33	isohom	$⊢ φ \to Z Iso (C) ℤ_{ring} \subseteq Z Hom (C) ℤ_{ring}$
38		ssn0	$⊢ (Z Iso (C) ℤ_{ring} \subseteq Z Hom (C) ℤ_{ring} \land Z Iso (C) ℤ_{ring} \neq \emptyset) \to Z Hom (C) ℤ_{ring} \neq \emptyset$
39	2 25 1 36 29 33	ringchom	$⊢ φ \to Z Hom (C) ℤ_{ring} = Z RingHom ℤ_{ring}$
40	39	neeq1d	$⊢ φ \to (Z Hom (C) ℤ_{ring} \neq \emptyset \leftrightarrow Z RingHom ℤ_{ring} \neq \emptyset)$
41		zringnzr	$⊢ ℤ_{ring} \in NzRing$
42		nrhmzr	$⊢ (Z \in (Ring ∖ NzRing) \land ℤ_{ring} \in NzRing) \to Z RingHom ℤ_{ring} = \emptyset$
43	3 41 42	sylancl	$⊢ φ \to Z RingHom ℤ_{ring} = \emptyset$
44		eqneqall	$⊢ Z RingHom ℤ_{ring} = \emptyset \to (Z RingHom ℤ_{ring} \neq \emptyset \to ZeroO (C) = \emptyset)$
45	43 44	syl	$⊢ φ \to (Z RingHom ℤ_{ring} \neq \emptyset \to ZeroO (C) = \emptyset)$
46	40 45	sylbid	$⊢ φ \to (Z Hom (C) ℤ_{ring} \neq \emptyset \to ZeroO (C) = \emptyset)$
47	38 46	syl5com	$⊢ (Z Iso (C) ℤ_{ring} \subseteq Z Hom (C) ℤ_{ring} \land Z Iso (C) ℤ_{ring} \neq \emptyset) \to (φ \to ZeroO (C) = \emptyset)$
48	47	expcom	$⊢ Z Iso (C) ℤ_{ring} \neq \emptyset \to (Z Iso (C) ℤ_{ring} \subseteq Z Hom (C) ℤ_{ring} \to (φ \to ZeroO (C) = \emptyset))$
49	48	com13	$⊢ φ \to (Z Iso (C) ℤ_{ring} \subseteq Z Hom (C) ℤ_{ring} \to (Z Iso (C) ℤ_{ring} \neq \emptyset \to ZeroO (C) = \emptyset))$
50	37 49	mpd	$⊢ φ \to (Z Iso (C) ℤ_{ring} \neq \emptyset \to ZeroO (C) = \emptyset)$
51	35 50	biimtrrid	$⊢ φ \to (\exists f f \in (Z Iso (C) ℤ_{ring}) \to ZeroO (C) = \emptyset)$
52	34 51	sylbid	$⊢ φ \to (Z ≃_{𝑐} (C) ℤ_{ring} \to ZeroO (C) = \emptyset)$
53	52	3ad2ant1	$⊢ (φ \land Z ≃_{𝑐} (C) h \land h ≃_{𝑐} (C) ℤ_{ring}) \to (Z ≃_{𝑐} (C) ℤ_{ring} \to ZeroO (C) = \emptyset)$
54	23 53	mpd	$⊢ (φ \land Z ≃_{𝑐} (C) h \land h ≃_{𝑐} (C) ℤ_{ring}) \to ZeroO (C) = \emptyset$
55	54	3exp	$⊢ φ \to (Z ≃_{𝑐} (C) h \to (h ≃_{𝑐} (C) ℤ_{ring} \to ZeroO (C) = \emptyset))$
56	55	a1dd	$⊢ φ \to (Z ≃_{𝑐} (C) h \to (h \in {Base}_{C} \to (h ≃_{𝑐} (C) ℤ_{ring} \to ZeroO (C) = \emptyset)))$
57	56	ad2antrr	$⊢ ((φ \land h \in TermO (C)) \land Z \in TermO (C)) \to (Z ≃_{𝑐} (C) h \to (h \in {Base}_{C} \to (h ≃_{𝑐} (C) ℤ_{ring} \to ZeroO (C) = \emptyset)))$
58	21 57	mpd	$⊢ ((φ \land h \in TermO (C)) \land Z \in TermO (C)) \to (h \in {Base}_{C} \to (h ≃_{𝑐} (C) ℤ_{ring} \to ZeroO (C) = \emptyset))$
59	58	exp31	$⊢ φ \to (h \in TermO (C) \to (Z \in TermO (C) \to (h \in {Base}_{C} \to (h ≃_{𝑐} (C) ℤ_{ring} \to ZeroO (C) = \emptyset))))$
60	59	com34	$⊢ φ \to (h \in TermO (C) \to (h \in {Base}_{C} \to (Z \in TermO (C) \to (h ≃_{𝑐} (C) ℤ_{ring} \to ZeroO (C) = \emptyset))))$
61	60	com25	$⊢ φ \to (h ≃_{𝑐} (C) ℤ_{ring} \to (h \in {Base}_{C} \to (Z \in TermO (C) \to (h \in TermO (C) \to ZeroO (C) = \emptyset))))$
62	61	ad2antrr	$⊢ ((φ \land h \in InitO (C)) \land ℤ_{ring} \in InitO (C)) \to (h ≃_{𝑐} (C) ℤ_{ring} \to (h \in {Base}_{C} \to (Z \in TermO (C) \to (h \in TermO (C) \to ZeroO (C) = \emptyset))))$
63	17 62	mpd	$⊢ ((φ \land h \in InitO (C)) \land ℤ_{ring} \in InitO (C)) \to (h \in {Base}_{C} \to (Z \in TermO (C) \to (h \in TermO (C) \to ZeroO (C) = \emptyset)))$
64	63	ex	$⊢ (φ \land h \in InitO (C)) \to (ℤ_{ring} \in InitO (C) \to (h \in {Base}_{C} \to (Z \in TermO (C) \to (h \in TermO (C) \to ZeroO (C) = \emptyset))))$
65	64	com25	$⊢ (φ \land h \in InitO (C)) \to (h \in TermO (C) \to (h \in {Base}_{C} \to (Z \in TermO (C) \to (ℤ_{ring} \in InitO (C) \to ZeroO (C) = \emptyset))))$
66	65	expimpd	$⊢ φ \to ((h \in InitO (C) \land h \in TermO (C)) \to (h \in {Base}_{C} \to (Z \in TermO (C) \to (ℤ_{ring} \in InitO (C) \to ZeroO (C) = \emptyset))))$
67	66	com23	$⊢ φ \to (h \in {Base}_{C} \to ((h \in InitO (C) \land h \in TermO (C)) \to (Z \in TermO (C) \to (ℤ_{ring} \in InitO (C) \to ZeroO (C) = \emptyset))))$
68	67	impd	$⊢ φ \to ((h \in {Base}_{C} \land (h \in InitO (C) \land h \in TermO (C))) \to (Z \in TermO (C) \to (ℤ_{ring} \in InitO (C) \to ZeroO (C) = \emptyset)))$
69	68	com24	$⊢ φ \to (ℤ_{ring} \in InitO (C) \to (Z \in TermO (C) \to ((h \in {Base}_{C} \land (h \in InitO (C) \land h \in TermO (C))) \to ZeroO (C) = \emptyset)))$
70	13 69	mpd	$⊢ φ \to (Z \in TermO (C) \to ((h \in {Base}_{C} \land (h \in InitO (C) \land h \in TermO (C))) \to ZeroO (C) = \emptyset))$
71	12 70	mpd	$⊢ φ \to ((h \in {Base}_{C} \land (h \in InitO (C) \land h \in TermO (C))) \to ZeroO (C) = \emptyset)$
72	71	adantr	$⊢ (φ \land h \in ZeroO (C)) \to ((h \in {Base}_{C} \land (h \in InitO (C) \land h \in TermO (C))) \to ZeroO (C) = \emptyset)$
73	11 72	mpd	$⊢ (φ \land h \in ZeroO (C)) \to ZeroO (C) = \emptyset$
74	73	expcom	$⊢ h \in ZeroO (C) \to (φ \to ZeroO (C) = \emptyset)$
75	74	exlimiv	$⊢ \exists h h \in ZeroO (C) \to (φ \to ZeroO (C) = \emptyset)$
76	7 75	sylbi	$⊢ \neg ZeroO (C) = \emptyset \to (φ \to ZeroO (C) = \emptyset)$
77	6 76	pm2.61i	$⊢ φ \to ZeroO (C) = \emptyset$

Metamath Proof Explorer

Theorem nzerooringczr

Proof