isirred2

Description: Expand out the class difference from isirred . (Contributed by Mario Carneiro, 4-Dec-2014)

	Ref	Expression
Hypotheses	isirred2.1	$⊢ B = {Base}_{R}$
	isirred2.2	$⊢ U = Unit (R)$
	isirred2.3	$⊢ I = Irred (R)$
	isirred2.4	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
Assertion	isirred2	$⊢ X \in I \leftrightarrow (X \in B \land \neg X \in U \land \forall x \in B \forall y \in B (x \underset{˙}{\cdot} y = X \to (x \in U \lor y \in U)))$

Proof

Step	Hyp	Ref	Expression
1		isirred2.1	$⊢ B = {Base}_{R}$
2		isirred2.2	$⊢ U = Unit (R)$
3		isirred2.3	$⊢ I = Irred (R)$
4		isirred2.4	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
5		eldif	$⊢ X \in (B ∖ U) \leftrightarrow (X \in B \land \neg X \in U)$
6		eldif	$⊢ x \in (B ∖ U) \leftrightarrow (x \in B \land \neg x \in U)$
7		eldif	$⊢ y \in (B ∖ U) \leftrightarrow (y \in B \land \neg y \in U)$
8	6 7	anbi12i	$⊢ (x \in (B ∖ U) \land y \in (B ∖ U)) \leftrightarrow ((x \in B \land \neg x \in U) \land (y \in B \land \neg y \in U))$
9		an4	$⊢ ((x \in B \land \neg x \in U) \land (y \in B \land \neg y \in U)) \leftrightarrow ((x \in B \land y \in B) \land (\neg x \in U \land \neg y \in U))$
10	8 9	bitri	$⊢ (x \in (B ∖ U) \land y \in (B ∖ U)) \leftrightarrow ((x \in B \land y \in B) \land (\neg x \in U \land \neg y \in U))$
11	10	imbi1i	$⊢ ((x \in (B ∖ U) \land y \in (B ∖ U)) \to x \underset{˙}{\cdot} y \neq X) \leftrightarrow (((x \in B \land y \in B) \land (\neg x \in U \land \neg y \in U)) \to x \underset{˙}{\cdot} y \neq X)$
12		impexp	$⊢ (((x \in B \land y \in B) \land (\neg x \in U \land \neg y \in U)) \to x \underset{˙}{\cdot} y \neq X) \leftrightarrow ((x \in B \land y \in B) \to ((\neg x \in U \land \neg y \in U) \to x \underset{˙}{\cdot} y \neq X))$
13		pm4.56	$⊢ (\neg x \in U \land \neg y \in U) \leftrightarrow \neg (x \in U \lor y \in U)$
14		df-ne	$⊢ x \underset{˙}{\cdot} y \neq X \leftrightarrow \neg x \underset{˙}{\cdot} y = X$
15	13 14	imbi12i	$⊢ ((\neg x \in U \land \neg y \in U) \to x \underset{˙}{\cdot} y \neq X) \leftrightarrow (\neg (x \in U \lor y \in U) \to \neg x \underset{˙}{\cdot} y = X)$
16		con34b	$⊢ (x \underset{˙}{\cdot} y = X \to (x \in U \lor y \in U)) \leftrightarrow (\neg (x \in U \lor y \in U) \to \neg x \underset{˙}{\cdot} y = X)$
17	15 16	bitr4i	$⊢ ((\neg x \in U \land \neg y \in U) \to x \underset{˙}{\cdot} y \neq X) \leftrightarrow (x \underset{˙}{\cdot} y = X \to (x \in U \lor y \in U))$
18	17	imbi2i	$⊢ ((x \in B \land y \in B) \to ((\neg x \in U \land \neg y \in U) \to x \underset{˙}{\cdot} y \neq X)) \leftrightarrow ((x \in B \land y \in B) \to (x \underset{˙}{\cdot} y = X \to (x \in U \lor y \in U)))$
19	12 18	bitri	$⊢ (((x \in B \land y \in B) \land (\neg x \in U \land \neg y \in U)) \to x \underset{˙}{\cdot} y \neq X) \leftrightarrow ((x \in B \land y \in B) \to (x \underset{˙}{\cdot} y = X \to (x \in U \lor y \in U)))$
20	11 19	bitri	$⊢ ((x \in (B ∖ U) \land y \in (B ∖ U)) \to x \underset{˙}{\cdot} y \neq X) \leftrightarrow ((x \in B \land y \in B) \to (x \underset{˙}{\cdot} y = X \to (x \in U \lor y \in U)))$
21	20	2albii	$⊢ \forall x \forall y ((x \in (B ∖ U) \land y \in (B ∖ U)) \to x \underset{˙}{\cdot} y \neq X) \leftrightarrow \forall x \forall y ((x \in B \land y \in B) \to (x \underset{˙}{\cdot} y = X \to (x \in U \lor y \in U)))$
22		r2al	$⊢ \forall x \in (B ∖ U) \forall y \in (B ∖ U) x \underset{˙}{\cdot} y \neq X \leftrightarrow \forall x \forall y ((x \in (B ∖ U) \land y \in (B ∖ U)) \to x \underset{˙}{\cdot} y \neq X)$
23		r2al	$⊢ \forall x \in B \forall y \in B (x \underset{˙}{\cdot} y = X \to (x \in U \lor y \in U)) \leftrightarrow \forall x \forall y ((x \in B \land y \in B) \to (x \underset{˙}{\cdot} y = X \to (x \in U \lor y \in U)))$
24	21 22 23	3bitr4i	$⊢ \forall x \in (B ∖ U) \forall y \in (B ∖ U) x \underset{˙}{\cdot} y \neq X \leftrightarrow \forall x \in B \forall y \in B (x \underset{˙}{\cdot} y = X \to (x \in U \lor y \in U))$
25	5 24	anbi12i	$⊢ (X \in (B ∖ U) \land \forall x \in (B ∖ U) \forall y \in (B ∖ U) x \underset{˙}{\cdot} y \neq X) \leftrightarrow ((X \in B \land \neg X \in U) \land \forall x \in B \forall y \in B (x \underset{˙}{\cdot} y = X \to (x \in U \lor y \in U)))$
26		eqid	$⊢ B ∖ U = B ∖ U$
27	1 2 3 26 4	isirred	$⊢ X \in I \leftrightarrow (X \in (B ∖ U) \land \forall x \in (B ∖ U) \forall y \in (B ∖ U) x \underset{˙}{\cdot} y \neq X)$
28		df-3an	$⊢ (X \in B \land \neg X \in U \land \forall x \in B \forall y \in B (x \underset{˙}{\cdot} y = X \to (x \in U \lor y \in U))) \leftrightarrow ((X \in B \land \neg X \in U) \land \forall x \in B \forall y \in B (x \underset{˙}{\cdot} y = X \to (x \in U \lor y \in U)))$
29	25 27 28	3bitr4i	$⊢ X \in I \leftrightarrow (X \in B \land \neg X \in U \land \forall x \in B \forall y \in B (x \underset{˙}{\cdot} y = X \to (x \in U \lor y \in U)))$

Metamath Proof Explorer

Theorem isirred2

Proof