chdmm1i

Description: De Morgan's law for meet in a Hilbert lattice. (Contributed by NM, 21-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ch0le.1	$⊢ A \in C_{ℋ}$
	chjcl.2	$⊢ B \in C_{ℋ}$
Assertion	chdmm1i	$⊢ ⊥ (A \cap B) = ⊥ (A) \lor_{ℋ} ⊥ (B)$

Proof

Step	Hyp	Ref	Expression
1		ch0le.1	$⊢ A \in C_{ℋ}$
2		chjcl.2	$⊢ B \in C_{ℋ}$
3	1	choccli	$⊢ ⊥ (A) \in C_{ℋ}$
4	2	choccli	$⊢ ⊥ (B) \in C_{ℋ}$
5	3 4	chub1i	$⊢ ⊥ (A) \subseteq ⊥ (A) \lor_{ℋ} ⊥ (B)$
6	3 4	chjcli	$⊢ ⊥ (A) \lor_{ℋ} ⊥ (B) \in C_{ℋ}$
7	1 6	chsscon1i	$⊢ ⊥ (A) \subseteq ⊥ (A) \lor_{ℋ} ⊥ (B) \leftrightarrow ⊥ (⊥ (A) \lor_{ℋ} ⊥ (B)) \subseteq A$
8	5 7	mpbi	$⊢ ⊥ (⊥ (A) \lor_{ℋ} ⊥ (B)) \subseteq A$
9	4 3	chub2i	$⊢ ⊥ (B) \subseteq ⊥ (A) \lor_{ℋ} ⊥ (B)$
10	2 6	chsscon1i	$⊢ ⊥ (B) \subseteq ⊥ (A) \lor_{ℋ} ⊥ (B) \leftrightarrow ⊥ (⊥ (A) \lor_{ℋ} ⊥ (B)) \subseteq B$
11	9 10	mpbi	$⊢ ⊥ (⊥ (A) \lor_{ℋ} ⊥ (B)) \subseteq B$
12	8 11	ssini	$⊢ ⊥ (⊥ (A) \lor_{ℋ} ⊥ (B)) \subseteq A \cap B$
13	1 2	chincli	$⊢ A \cap B \in C_{ℋ}$
14	6 13	chsscon1i	$⊢ ⊥ (⊥ (A) \lor_{ℋ} ⊥ (B)) \subseteq A \cap B \leftrightarrow ⊥ (A \cap B) \subseteq ⊥ (A) \lor_{ℋ} ⊥ (B)$
15	12 14	mpbi	$⊢ ⊥ (A \cap B) \subseteq ⊥ (A) \lor_{ℋ} ⊥ (B)$
16		inss1	$⊢ A \cap B \subseteq A$
17	13 1	chsscon3i	$⊢ A \cap B \subseteq A \leftrightarrow ⊥ (A) \subseteq ⊥ (A \cap B)$
18	16 17	mpbi	$⊢ ⊥ (A) \subseteq ⊥ (A \cap B)$
19		inss2	$⊢ A \cap B \subseteq B$
20	13 2	chsscon3i	$⊢ A \cap B \subseteq B \leftrightarrow ⊥ (B) \subseteq ⊥ (A \cap B)$
21	19 20	mpbi	$⊢ ⊥ (B) \subseteq ⊥ (A \cap B)$
22	13	choccli	$⊢ ⊥ (A \cap B) \in C_{ℋ}$
23	3 4 22	chlubii	$⊢ (⊥ (A) \subseteq ⊥ (A \cap B) \land ⊥ (B) \subseteq ⊥ (A \cap B)) \to ⊥ (A) \lor_{ℋ} ⊥ (B) \subseteq ⊥ (A \cap B)$
24	18 21 23	mp2an	$⊢ ⊥ (A) \lor_{ℋ} ⊥ (B) \subseteq ⊥ (A \cap B)$
25	15 24	eqssi	$⊢ ⊥ (A \cap B) = ⊥ (A) \lor_{ℋ} ⊥ (B)$

Metamath Proof Explorer

Theorem chdmm1i

Proof