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	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
	zrtermoringc.c	⊢ 𝐶 = ( RingCat ‘ 𝑈 )
	zrtermoringc.z	⊢ ( 𝜑 → 𝑍 ∈ ( Ring ∖ NzRing ) )
	zrtermoringc.e	⊢ ( 𝜑 → 𝑍 ∈ 𝑈 )
	zrninitoringc.e	⊢ ( 𝜑 → ∃ 𝑟 ∈ ( Base ‘ 𝐶 ) 𝑟 ∈ NzRing )
Assertion	zrninitoringc	⊢ ( 𝜑 → 𝑍 ∉ ( InitO ‘ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		zrtermoringc.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
2		zrtermoringc.c	⊢ 𝐶 = ( RingCat ‘ 𝑈 )
3		zrtermoringc.z	⊢ ( 𝜑 → 𝑍 ∈ ( Ring ∖ NzRing ) )
4		zrtermoringc.e	⊢ ( 𝜑 → 𝑍 ∈ 𝑈 )
5		zrninitoringc.e	⊢ ( 𝜑 → ∃ 𝑟 ∈ ( Base ‘ 𝐶 ) 𝑟 ∈ NzRing )
6		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
7	1	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑟 ∈ NzRing ) → 𝑈 ∈ 𝑉 )
8		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
9	3	eldifad	⊢ ( 𝜑 → 𝑍 ∈ Ring )
10	4 9	elind	⊢ ( 𝜑 → 𝑍 ∈ ( 𝑈 ∩ Ring ) )
11	2 6 1	ringcbas	⊢ ( 𝜑 → ( Base ‘ 𝐶 ) = ( 𝑈 ∩ Ring ) )
12	10 11	eleqtrrd	⊢ ( 𝜑 → 𝑍 ∈ ( Base ‘ 𝐶 ) )
13	12	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑟 ∈ NzRing ) → 𝑍 ∈ ( Base ‘ 𝐶 ) )
14		simplr	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑟 ∈ NzRing ) → 𝑟 ∈ ( Base ‘ 𝐶 ) )
15	2 6 7 8 13 14	ringchom	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑟 ∈ NzRing ) → ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) = ( 𝑍 RingHom 𝑟 ) )
16	3	adantr	⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) → 𝑍 ∈ ( Ring ∖ NzRing ) )
17		nrhmzr	⊢ ( ( 𝑍 ∈ ( Ring ∖ NzRing ) ∧ 𝑟 ∈ NzRing ) → ( 𝑍 RingHom 𝑟 ) = ∅ )
18	16 17	sylan	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑟 ∈ NzRing ) → ( 𝑍 RingHom 𝑟 ) = ∅ )
19	15 18	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑟 ∈ NzRing ) → ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) = ∅ )
20		eq0	⊢ ( ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) = ∅ ↔ ∀ ℎ ¬ ℎ ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) )
21	19 20	sylib	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑟 ∈ NzRing ) → ∀ ℎ ¬ ℎ ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) )
22		alnex	⊢ ( ∀ ℎ ¬ ℎ ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) ↔ ¬ ∃ ℎ ℎ ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) )
23	21 22	sylib	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑟 ∈ NzRing ) → ¬ ∃ ℎ ℎ ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) )
24		euex	⊢ ( ∃! ℎ ℎ ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) → ∃ ℎ ℎ ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) )
25	23 24	nsyl	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑟 ∈ NzRing ) → ¬ ∃! ℎ ℎ ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) )
26	25	ex	⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑟 ∈ NzRing → ¬ ∃! ℎ ℎ ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) ) )
27	26	reximdva	⊢ ( 𝜑 → ( ∃ 𝑟 ∈ ( Base ‘ 𝐶 ) 𝑟 ∈ NzRing → ∃ 𝑟 ∈ ( Base ‘ 𝐶 ) ¬ ∃! ℎ ℎ ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) ) )
28	5 27	mpd	⊢ ( 𝜑 → ∃ 𝑟 ∈ ( Base ‘ 𝐶 ) ¬ ∃! ℎ ℎ ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) )
29		rexnal	⊢ ( ∃ 𝑟 ∈ ( Base ‘ 𝐶 ) ¬ ∃! ℎ ℎ ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) ↔ ¬ ∀ 𝑟 ∈ ( Base ‘ 𝐶 ) ∃! ℎ ℎ ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) )
30	28 29	sylib	⊢ ( 𝜑 → ¬ ∀ 𝑟 ∈ ( Base ‘ 𝐶 ) ∃! ℎ ℎ ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) )
31		df-nel	⊢ ( 𝑍 ∉ ( InitO ‘ 𝐶 ) ↔ ¬ 𝑍 ∈ ( InitO ‘ 𝐶 ) )
32	2	ringccat	⊢ ( 𝑈 ∈ 𝑉 → 𝐶 ∈ Cat )
33	1 32	syl	⊢ ( 𝜑 → 𝐶 ∈ Cat )
34	6 8 33 12	isinito	⊢ ( 𝜑 → ( 𝑍 ∈ ( InitO ‘ 𝐶 ) ↔ ∀ 𝑟 ∈ ( Base ‘ 𝐶 ) ∃! ℎ ℎ ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) ) )
35	34	notbid	⊢ ( 𝜑 → ( ¬ 𝑍 ∈ ( InitO ‘ 𝐶 ) ↔ ¬ ∀ 𝑟 ∈ ( Base ‘ 𝐶 ) ∃! ℎ ℎ ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) ) )
36	31 35	bitrid	⊢ ( 𝜑 → ( 𝑍 ∉ ( InitO ‘ 𝐶 ) ↔ ¬ ∀ 𝑟 ∈ ( Base ‘ 𝐶 ) ∃! ℎ ℎ ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) ) )
37	30 36	mpbird	⊢ ( 𝜑 → 𝑍 ∉ ( InitO ‘ 𝐶 ) )

Metamath Proof Explorer

Theorem zrninitoringc

Proof