atcvati

Description: A nonzero Hilbert lattice element less than the join of two atoms is an atom. (Contributed by NM, 28-Jun-2004) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	atoml.1	$⊢ A \in C_{ℋ}$
	Assertion	atcvati	$⊢ (B \in HAtoms \land C \in HAtoms) \to ((A \neq 0_{ℋ} \land A \subset B \lor_{ℋ} C) \to A \in HAtoms)$

Proof

Step	Hyp	Ref	Expression
1		atoml.1	$⊢ A \in C_{ℋ}$
2	1	atcvatlem	$⊢ ((B \in HAtoms \land C \in HAtoms) \land (A \neq 0_{ℋ} \land A \subset B \lor_{ℋ} C)) \to (\neg B \subseteq A \to A \in HAtoms)$
3		atelch	$⊢ C \in HAtoms \to C \in C_{ℋ}$
4		atelch	$⊢ B \in HAtoms \to B \in C_{ℋ}$
5		chjcom	$⊢ (C \in C_{ℋ} \land B \in C_{ℋ}) \to C \lor_{ℋ} B = B \lor_{ℋ} C$
6	3 4 5	syl2an	$⊢ (C \in HAtoms \land B \in HAtoms) \to C \lor_{ℋ} B = B \lor_{ℋ} C$
7	6	psseq2d	$⊢ (C \in HAtoms \land B \in HAtoms) \to (A \subset C \lor_{ℋ} B \leftrightarrow A \subset B \lor_{ℋ} C)$
8	7	anbi2d	$⊢ (C \in HAtoms \land B \in HAtoms) \to ((A \neq 0_{ℋ} \land A \subset C \lor_{ℋ} B) \leftrightarrow (A \neq 0_{ℋ} \land A \subset B \lor_{ℋ} C))$
9	1	atcvatlem	$⊢ ((C \in HAtoms \land B \in HAtoms) \land (A \neq 0_{ℋ} \land A \subset C \lor_{ℋ} B)) \to (\neg C \subseteq A \to A \in HAtoms)$
10	9	ex	$⊢ (C \in HAtoms \land B \in HAtoms) \to ((A \neq 0_{ℋ} \land A \subset C \lor_{ℋ} B) \to (\neg C \subseteq A \to A \in HAtoms))$
11	8 10	sylbird	$⊢ (C \in HAtoms \land B \in HAtoms) \to ((A \neq 0_{ℋ} \land A \subset B \lor_{ℋ} C) \to (\neg C \subseteq A \to A \in HAtoms))$
12	11	ancoms	$⊢ (B \in HAtoms \land C \in HAtoms) \to ((A \neq 0_{ℋ} \land A \subset B \lor_{ℋ} C) \to (\neg C \subseteq A \to A \in HAtoms))$
13	12	imp	$⊢ ((B \in HAtoms \land C \in HAtoms) \land (A \neq 0_{ℋ} \land A \subset B \lor_{ℋ} C)) \to (\neg C \subseteq A \to A \in HAtoms)$
14		chlub	$⊢ (B \in C_{ℋ} \land C \in C_{ℋ} \land A \in C_{ℋ}) \to ((B \subseteq A \land C \subseteq A) \leftrightarrow B \lor_{ℋ} C \subseteq A)$
15	14	3comr	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \to ((B \subseteq A \land C \subseteq A) \leftrightarrow B \lor_{ℋ} C \subseteq A)$
16		ssnpss	$⊢ B \lor_{ℋ} C \subseteq A \to \neg A \subset B \lor_{ℋ} C$
17	15 16	biimtrdi	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \to ((B \subseteq A \land C \subseteq A) \to \neg A \subset B \lor_{ℋ} C)$
18	17	con2d	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \to (A \subset B \lor_{ℋ} C \to \neg (B \subseteq A \land C \subseteq A))$
19		ianor	$⊢ \neg (B \subseteq A \land C \subseteq A) \leftrightarrow (\neg B \subseteq A \lor \neg C \subseteq A)$
20	18 19	imbitrdi	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \to (A \subset B \lor_{ℋ} C \to (\neg B \subseteq A \lor \neg C \subseteq A))$
21	1 20	mp3an1	$⊢ (B \in C_{ℋ} \land C \in C_{ℋ}) \to (A \subset B \lor_{ℋ} C \to (\neg B \subseteq A \lor \neg C \subseteq A))$
22	4 3 21	syl2an	$⊢ (B \in HAtoms \land C \in HAtoms) \to (A \subset B \lor_{ℋ} C \to (\neg B \subseteq A \lor \neg C \subseteq A))$
23	22	imp	$⊢ ((B \in HAtoms \land C \in HAtoms) \land A \subset B \lor_{ℋ} C) \to (\neg B \subseteq A \lor \neg C \subseteq A)$
24	23	adantrl	$⊢ ((B \in HAtoms \land C \in HAtoms) \land (A \neq 0_{ℋ} \land A \subset B \lor_{ℋ} C)) \to (\neg B \subseteq A \lor \neg C \subseteq A)$
25	2 13 24	mpjaod	$⊢ ((B \in HAtoms \land C \in HAtoms) \land (A \neq 0_{ℋ} \land A \subset B \lor_{ℋ} C)) \to A \in HAtoms$
26	25	ex	$⊢ (B \in HAtoms \land C \in HAtoms) \to ((A \neq 0_{ℋ} \land A \subset B \lor_{ℋ} C) \to A \in HAtoms)$

Metamath Proof Explorer

Theorem atcvati

Proof