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 \in NzRing \leftrightarrow (R \in Ring \land 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 \in NzRing \leftrightarrow (R \in Ring \land 1_{R} \neq 0_{R})$
5	1 2	ringidcl	$⊢ R \in Ring \to 1_{R} \in B$
6	5	adantr	$⊢ (R \in Ring \land 1_{R} \neq 0_{R}) \to 1_{R} \in B$
7	1 3	ring0cl	$⊢ R \in Ring \to 0_{R} \in B$
8	7	adantr	$⊢ (R \in Ring \land 1_{R} \neq 0_{R}) \to 0_{R} \in B$
9		simpr	$⊢ (R \in Ring \land 1_{R} \neq 0_{R}) \to 1_{R} \neq 0_{R}$
10		df-ne	$⊢ x \neq y \leftrightarrow \neg x = y$
11		neeq1	$⊢ x = 1_{R} \to (x \neq y \leftrightarrow 1_{R} \neq y)$
12	10 11	syl5bbr	$⊢ x = 1_{R} \to (\neg x = y \leftrightarrow 1_{R} \neq y)$
13		neeq2	$⊢ y = 0_{R} \to (1_{R} \neq y \leftrightarrow 1_{R} \neq 0_{R})$
14	12 13	rspc2ev	$⊢ (1_{R} \in B \land 0_{R} \in B \land 1_{R} \neq 0_{R}) \to \exists x \in B \exists y \in B \neg x = y$
15	6 8 9 14	syl3anc	$⊢ (R \in Ring \land 1_{R} \neq 0_{R}) \to \exists x \in B \exists y \in B \neg x = y$
16	15	ex	$⊢ R \in Ring \to (1_{R} \neq 0_{R} \to \exists x \in B \exists y \in B \neg x = y)$
17	1 2 3	ring1eq0	$⊢ (R \in Ring \land x \in B \land y \in B) \to (1_{R} = 0_{R} \to x = y)$
18	17	3expb	$⊢ (R \in Ring \land (x \in B \land y \in B)) \to (1_{R} = 0_{R} \to x = y)$
19	18	necon3bd	$⊢ (R \in Ring \land (x \in B \land y \in B)) \to (\neg x = y \to 1_{R} \neq 0_{R})$
20	19	rexlimdvva	$⊢ R \in Ring \to (\exists x \in B \exists y \in B \neg x = y \to 1_{R} \neq 0_{R})$
21	16 20	impbid	$⊢ R \in Ring \to (1_{R} \neq 0_{R} \leftrightarrow \exists x \in B \exists y \in B \neg x = y)$
22	1	fvexi	$⊢ B \in V$
23		1sdom	$⊢ B \in V \to (1_{𝑜} ≺ B \leftrightarrow \exists x \in B \exists y \in B \neg x = y)$
24	22 23	ax-mp	$⊢ 1_{𝑜} ≺ B \leftrightarrow \exists x \in B \exists y \in B \neg x = y$
25	21 24	syl6bbr	$⊢ R \in Ring \to (1_{R} \neq 0_{R} \leftrightarrow 1_{𝑜} ≺ B)$
26		1onn	$⊢ 1_{𝑜} \in ω$
27		sucdom	$⊢ 1_{𝑜} \in ω \to (1_{𝑜} ≺ B \leftrightarrow suc 1_{𝑜} ≼ B)$
28	26 27	ax-mp	$⊢ 1_{𝑜} ≺ B \leftrightarrow suc 1_{𝑜} ≼ B$
29		df-2o	$⊢ 2_{𝑜} = suc 1_{𝑜}$
30	29	breq1i	$⊢ 2_{𝑜} ≼ B \leftrightarrow suc 1_{𝑜} ≼ B$
31	28 30	bitr4i	$⊢ 1_{𝑜} ≺ B \leftrightarrow 2_{𝑜} ≼ B$
32	25 31	syl6bb	$⊢ R \in Ring \to (1_{R} \neq 0_{R} \leftrightarrow 2_{𝑜} ≼ B)$
33	32	pm5.32i	$⊢ (R \in Ring \land 1_{R} \neq 0_{R}) \leftrightarrow (R \in Ring \land 2_{𝑜} ≼ B)$
34	4 33	bitri	$⊢ R \in NzRing \leftrightarrow (R \in Ring \land 2_{𝑜} ≼ B)$

Metamath Proof Explorer

Theorem isnzr2

Proof