osumcori

Description: Corollary of osumi . (Contributed by NM, 5-Nov-2000) (New usage is discouraged.)

	Ref	Expression
Hypotheses	osum.1	$⊢ A \in C_{ℋ}$
	osum.2	$⊢ B \in C_{ℋ}$
Assertion	osumcori	$⊢ (A \cap B) +_{ℋ} (A \cap ⊥ (B)) = (A \cap B) \lor_{ℋ} (A \cap ⊥ (B))$

Step	Hyp	Ref	Expression
1		osum.1	$⊢ A \in C_{ℋ}$
2		osum.2	$⊢ B \in C_{ℋ}$
3		inss2	$⊢ A \cap B \subseteq B$
4	1	choccli	$⊢ ⊥ (A) \in C_{ℋ}$
5	2 4	chub2i	$⊢ B \subseteq ⊥ (A) \lor_{ℋ} B$
6	3 5	sstri	$⊢ A \cap B \subseteq ⊥ (A) \lor_{ℋ} B$
7	1 2	chdmm3i	$⊢ ⊥ (A \cap ⊥ (B)) = ⊥ (A) \lor_{ℋ} B$
8	6 7	sseqtrri	$⊢ A \cap B \subseteq ⊥ (A \cap ⊥ (B))$
9	1 2	chincli	$⊢ A \cap B \in C_{ℋ}$
10	2	choccli	$⊢ ⊥ (B) \in C_{ℋ}$
11	1 10	chincli	$⊢ A \cap ⊥ (B) \in C_{ℋ}$
12	9 11	osumi	$⊢ A \cap B \subseteq ⊥ (A \cap ⊥ (B)) \to (A \cap B) +_{ℋ} (A \cap ⊥ (B)) = (A \cap B) \lor_{ℋ} (A \cap ⊥ (B))$
13	8 12	ax-mp	$⊢ (A \cap B) +_{ℋ} (A \cap ⊥ (B)) = (A \cap B) \lor_{ℋ} (A \cap ⊥ (B))$

Metamath Proof Explorer