cmcmlem

Description: Commutation is symmetric. Theorem 3.4 of Beran p. 45. (Contributed by NM, 3-Nov-2000) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pjoml2.1	$⊢ A \in C_{ℋ}$
	pjoml2.2	$⊢ B \in C_{ℋ}$
Assertion	cmcmlem	$⊢ A 𝐶_{ℋ} B \to B 𝐶_{ℋ} A$

Proof

Step	Hyp	Ref	Expression
1		pjoml2.1	$⊢ A \in C_{ℋ}$
2		pjoml2.2	$⊢ B \in C_{ℋ}$
3	1	choccli	$⊢ ⊥ (A) \in C_{ℋ}$
4	2 3	chub2i	$⊢ B \subseteq ⊥ (A) \lor_{ℋ} B$
5		sseqin2	$⊢ B \subseteq ⊥ (A) \lor_{ℋ} B \leftrightarrow (⊥ (A) \lor_{ℋ} B) \cap B = B$
6	4 5	mpbi	$⊢ (⊥ (A) \lor_{ℋ} B) \cap B = B$
7	6	ineq2i	$⊢ (⊥ (A) \lor_{ℋ} ⊥ (B)) \cap ((⊥ (A) \lor_{ℋ} B) \cap B) = (⊥ (A) \lor_{ℋ} ⊥ (B)) \cap B$
8		inass	$⊢ ((⊥ (A) \lor_{ℋ} ⊥ (B)) \cap (⊥ (A) \lor_{ℋ} B)) \cap B = (⊥ (A) \lor_{ℋ} ⊥ (B)) \cap ((⊥ (A) \lor_{ℋ} B) \cap B)$
9	1 2	chdmm1i	$⊢ ⊥ (A \cap B) = ⊥ (A) \lor_{ℋ} ⊥ (B)$
10	9	ineq1i	$⊢ ⊥ (A \cap B) \cap B = (⊥ (A) \lor_{ℋ} ⊥ (B)) \cap B$
11	7 8 10	3eqtr4ri	$⊢ ⊥ (A \cap B) \cap B = ((⊥ (A) \lor_{ℋ} ⊥ (B)) \cap (⊥ (A) \lor_{ℋ} B)) \cap B$
12	1 2	chdmj4i	$⊢ ⊥ (⊥ (A) \lor_{ℋ} ⊥ (B)) = A \cap B$
13	1 2	chdmj2i	$⊢ ⊥ (⊥ (A) \lor_{ℋ} B) = A \cap ⊥ (B)$
14	12 13	oveq12i	$⊢ ⊥ (⊥ (A) \lor_{ℋ} ⊥ (B)) \lor_{ℋ} ⊥ (⊥ (A) \lor_{ℋ} B) = (A \cap B) \lor_{ℋ} (A \cap ⊥ (B))$
15	14	eqeq2i	$⊢ A = ⊥ (⊥ (A) \lor_{ℋ} ⊥ (B)) \lor_{ℋ} ⊥ (⊥ (A) \lor_{ℋ} B) \leftrightarrow A = (A \cap B) \lor_{ℋ} (A \cap ⊥ (B))$
16	15	biimpri	$⊢ A = (A \cap B) \lor_{ℋ} (A \cap ⊥ (B)) \to A = ⊥ (⊥ (A) \lor_{ℋ} ⊥ (B)) \lor_{ℋ} ⊥ (⊥ (A) \lor_{ℋ} B)$
17	16	fveq2d	$⊢ A = (A \cap B) \lor_{ℋ} (A \cap ⊥ (B)) \to ⊥ (A) = ⊥ (⊥ (⊥ (A) \lor_{ℋ} ⊥ (B)) \lor_{ℋ} ⊥ (⊥ (A) \lor_{ℋ} B))$
18	2	choccli	$⊢ ⊥ (B) \in C_{ℋ}$
19	3 18	chjcli	$⊢ ⊥ (A) \lor_{ℋ} ⊥ (B) \in C_{ℋ}$
20	3 2	chjcli	$⊢ ⊥ (A) \lor_{ℋ} B \in C_{ℋ}$
21	19 20	chdmj4i	$⊢ ⊥ (⊥ (⊥ (A) \lor_{ℋ} ⊥ (B)) \lor_{ℋ} ⊥ (⊥ (A) \lor_{ℋ} B)) = (⊥ (A) \lor_{ℋ} ⊥ (B)) \cap (⊥ (A) \lor_{ℋ} B)$
22	17 21	eqtr2di	$⊢ A = (A \cap B) \lor_{ℋ} (A \cap ⊥ (B)) \to (⊥ (A) \lor_{ℋ} ⊥ (B)) \cap (⊥ (A) \lor_{ℋ} B) = ⊥ (A)$
23	22	ineq1d	$⊢ A = (A \cap B) \lor_{ℋ} (A \cap ⊥ (B)) \to ((⊥ (A) \lor_{ℋ} ⊥ (B)) \cap (⊥ (A) \lor_{ℋ} B)) \cap B = ⊥ (A) \cap B$
24	11 23	syl5eq	$⊢ A = (A \cap B) \lor_{ℋ} (A \cap ⊥ (B)) \to ⊥ (A \cap B) \cap B = ⊥ (A) \cap B$
25	24	oveq2d	$⊢ A = (A \cap B) \lor_{ℋ} (A \cap ⊥ (B)) \to (A \cap B) \lor_{ℋ} (⊥ (A \cap B) \cap B) = (A \cap B) \lor_{ℋ} (⊥ (A) \cap B)$
26		inss2	$⊢ A \cap B \subseteq B$
27	1 2	chincli	$⊢ A \cap B \in C_{ℋ}$
28	27 2	pjoml2i	$⊢ A \cap B \subseteq B \to (A \cap B) \lor_{ℋ} (⊥ (A \cap B) \cap B) = B$
29	26 28	ax-mp	$⊢ (A \cap B) \lor_{ℋ} (⊥ (A \cap B) \cap B) = B$
30		incom	$⊢ A \cap B = B \cap A$
31		incom	$⊢ ⊥ (A) \cap B = B \cap ⊥ (A)$
32	30 31	oveq12i	$⊢ (A \cap B) \lor_{ℋ} (⊥ (A) \cap B) = (B \cap A) \lor_{ℋ} (B \cap ⊥ (A))$
33	25 29 32	3eqtr3g	$⊢ A = (A \cap B) \lor_{ℋ} (A \cap ⊥ (B)) \to B = (B \cap A) \lor_{ℋ} (B \cap ⊥ (A))$
34	1 2	cmbri	$⊢ A 𝐶_{ℋ} B \leftrightarrow A = (A \cap B) \lor_{ℋ} (A \cap ⊥ (B))$
35	2 1	cmbri	$⊢ B 𝐶_{ℋ} A \leftrightarrow B = (B \cap A) \lor_{ℋ} (B \cap ⊥ (A))$
36	33 34 35	3imtr4i	$⊢ A 𝐶_{ℋ} B \to B 𝐶_{ℋ} A$

Metamath Proof Explorer

Theorem cmcmlem

Proof