Metamath Proof Explorer


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 B = Base R
Assertion isnzr2 R NzRing R Ring 2 𝑜 B

Proof

Step Hyp Ref Expression
1 isnzr2.b B = Base R
2 eqid 1 R = 1 R
3 eqid 0 R = 0 R
4 2 3 isnzr R NzRing R Ring 1 R 0 R
5 1 2 ringidcl R Ring 1 R B
6 5 adantr R Ring 1 R 0 R 1 R B
7 1 3 ring0cl R Ring 0 R B
8 7 adantr R Ring 1 R 0 R 0 R B
9 simpr R Ring 1 R 0 R 1 R 0 R
10 df-ne x y ¬ x = y
11 neeq1 x = 1 R x y 1 R y
12 10 11 bitr3id x = 1 R ¬ x = y 1 R y
13 neeq2 y = 0 R 1 R y 1 R 0 R
14 12 13 rspc2ev 1 R B 0 R B 1 R 0 R x B y B ¬ x = y
15 6 8 9 14 syl3anc R Ring 1 R 0 R x B y B ¬ x = y
16 15 ex R Ring 1 R 0 R x B y B ¬ x = y
17 1 2 3 ring1eq0 R Ring x B y B 1 R = 0 R x = y
18 17 3expb R Ring x B y B 1 R = 0 R x = y
19 18 necon3bd R Ring x B y B ¬ x = y 1 R 0 R
20 19 rexlimdvva R Ring x B y B ¬ x = y 1 R 0 R
21 16 20 impbid R Ring 1 R 0 R x B y B ¬ x = y
22 1 fvexi B V
23 1sdom B V 1 𝑜 B x B y B ¬ x = y
24 22 23 ax-mp 1 𝑜 B x B y B ¬ x = y
25 21 24 bitr4di R Ring 1 R 0 R 1 𝑜 B
26 1onn 1 𝑜 ω
27 sucdom 1 𝑜 ω 1 𝑜 B suc 1 𝑜 B
28 26 27 ax-mp 1 𝑜 B suc 1 𝑜 B
29 df-2o 2 𝑜 = suc 1 𝑜
30 29 breq1i 2 𝑜 B suc 1 𝑜 B
31 28 30 bitr4i 1 𝑜 B 2 𝑜 B
32 25 31 bitrdi R Ring 1 R 0 R 2 𝑜 B
33 32 pm5.32i R Ring 1 R 0 R R Ring 2 𝑜 B
34 4 33 bitri R NzRing R Ring 2 𝑜 B