Theorem isnzr2

Description: Equivalent characterization of nonzero rings: they have at least two elements. (Contributed by Stefan O'Rear, 24-Feb-2015)

	Ref	Expression
Hypothesis	isnzr2.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
Assertion	isnzr2	⊢ ( 𝑅 ∈ NzRing ↔ ( 𝑅 ∈ Ring ∧ 2o ≼ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		isnzr2.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
3		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
4	2 3	isnzr	⊢ ( 𝑅 ∈ NzRing ↔ ( 𝑅 ∈ Ring ∧ ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) )
5	1 2	ringidcl	⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
6	5	adantr	⊢ ( ( 𝑅 ∈ Ring ∧ ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
7	1 3	ring0cl	⊢ ( 𝑅 ∈ Ring → ( 0g ‘ 𝑅 ) ∈ 𝐵 )
8	7	adantr	⊢ ( ( 𝑅 ∈ Ring ∧ ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) → ( 0g ‘ 𝑅 ) ∈ 𝐵 )
9		simpr	⊢ ( ( 𝑅 ∈ Ring ∧ ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) → ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) )
10		df-ne	⊢ ( 𝑥 ≠ 𝑦 ↔ ¬ 𝑥 = 𝑦 )
11		neeq1	⊢ ( 𝑥 = ( 1r ‘ 𝑅 ) → ( 𝑥 ≠ 𝑦 ↔ ( 1r ‘ 𝑅 ) ≠ 𝑦 ) )
12	10 11	bitr3id	⊢ ( 𝑥 = ( 1r ‘ 𝑅 ) → ( ¬ 𝑥 = 𝑦 ↔ ( 1r ‘ 𝑅 ) ≠ 𝑦 ) )
13		neeq2	⊢ ( 𝑦 = ( 0g ‘ 𝑅 ) → ( ( 1r ‘ 𝑅 ) ≠ 𝑦 ↔ ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) )
14	12 13	rspc2ev	⊢ ( ( ( 1r ‘ 𝑅 ) ∈ 𝐵 ∧ ( 0g ‘ 𝑅 ) ∈ 𝐵 ∧ ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) → ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ¬ 𝑥 = 𝑦 )
15	6 8 9 14	syl3anc	⊢ ( ( 𝑅 ∈ Ring ∧ ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) → ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ¬ 𝑥 = 𝑦 )
16	15	ex	⊢ ( 𝑅 ∈ Ring → ( ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) → ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ¬ 𝑥 = 𝑦 ) )
17	1 2 3	ring1eq0	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) → 𝑥 = 𝑦 ) )
18	17	3expb	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) → 𝑥 = 𝑦 ) )
19	18	necon3bd	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ¬ 𝑥 = 𝑦 → ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) )
20	19	rexlimdvva	⊢ ( 𝑅 ∈ Ring → ( ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ¬ 𝑥 = 𝑦 → ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) )
21	16 20	impbid	⊢ ( 𝑅 ∈ Ring → ( ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ↔ ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ¬ 𝑥 = 𝑦 ) )
22	1	fvexi	⊢ 𝐵 ∈ V
23		1sdom	⊢ ( 𝐵 ∈ V → ( 1o ≺ 𝐵 ↔ ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ¬ 𝑥 = 𝑦 ) )
24	22 23	ax-mp	⊢ ( 1o ≺ 𝐵 ↔ ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ¬ 𝑥 = 𝑦 )
25	21 24	bitr4di	⊢ ( 𝑅 ∈ Ring → ( ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ↔ 1o ≺ 𝐵 ) )
26		1onn	⊢ 1o ∈ ω
27		sucdom	⊢ ( 1o ∈ ω → ( 1o ≺ 𝐵 ↔ suc 1o ≼ 𝐵 ) )
28	26 27	ax-mp	⊢ ( 1o ≺ 𝐵 ↔ suc 1o ≼ 𝐵 )
29		df-2o	⊢ 2o = suc 1o
30	29	breq1i	⊢ ( 2o ≼ 𝐵 ↔ suc 1o ≼ 𝐵 )
31	28 30	bitr4i	⊢ ( 1o ≺ 𝐵 ↔ 2o ≼ 𝐵 )
32	25 31	bitrdi	⊢ ( 𝑅 ∈ Ring → ( ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ↔ 2o ≼ 𝐵 ) )
33	32	pm5.32i	⊢ ( ( 𝑅 ∈ Ring ∧ ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) ↔ ( 𝑅 ∈ Ring ∧ 2o ≼ 𝐵 ) )
34	4 33	bitri	⊢ ( 𝑅 ∈ NzRing ↔ ( 𝑅 ∈ Ring ∧ 2o ≼ 𝐵 ) )