intnatN

Description: If the intersection with a non-majorizing element is an atom, the intersecting element is not an atom. (Contributed by NM, 26-Jun-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	intnat.b	$⊢ B = {Base}_{K}$
	intnat.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	intnat.m	$⊢ \underset{˙}{\land} = meet (K)$
	intnat.a	$⊢ A = Atoms (K)$
Assertion	intnatN	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (\neg Y \underset{˙}{\leq} X \land X \underset{˙}{\land} Y \in A)) \to \neg Y \in A$

Proof

Step	Hyp	Ref	Expression
1		intnat.b	$⊢ B = {Base}_{K}$
2		intnat.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		intnat.m	$⊢ \underset{˙}{\land} = meet (K)$
4		intnat.a	$⊢ A = Atoms (K)$
5		hlatl	$⊢ K \in HL \to K \in AtLat$
6	5	3ad2ant1	$⊢ (K \in HL \land X \in B \land Y \in B) \to K \in AtLat$
7	6	ad2antrr	$⊢ (((K \in HL \land X \in B \land Y \in B) \land \neg Y \underset{˙}{\leq} X) \land X \underset{˙}{\land} Y \in A) \to K \in AtLat$
8		eqid	$⊢ 0. (K) = 0. (K)$
9	8 4	atn0	$⊢ (K \in AtLat \land X \underset{˙}{\land} Y \in A) \to X \underset{˙}{\land} Y \neq 0. (K)$
10	7 9	sylancom	$⊢ (((K \in HL \land X \in B \land Y \in B) \land \neg Y \underset{˙}{\leq} X) \land X \underset{˙}{\land} Y \in A) \to X \underset{˙}{\land} Y \neq 0. (K)$
11	10	ex	$⊢ ((K \in HL \land X \in B \land Y \in B) \land \neg Y \underset{˙}{\leq} X) \to (X \underset{˙}{\land} Y \in A \to X \underset{˙}{\land} Y \neq 0. (K))$
12		simpll1	$⊢ (((K \in HL \land X \in B \land Y \in B) \land \neg Y \underset{˙}{\leq} X) \land Y \in A) \to K \in HL$
13	12	hllatd	$⊢ (((K \in HL \land X \in B \land Y \in B) \land \neg Y \underset{˙}{\leq} X) \land Y \in A) \to K \in Lat$
14		simpll2	$⊢ (((K \in HL \land X \in B \land Y \in B) \land \neg Y \underset{˙}{\leq} X) \land Y \in A) \to X \in B$
15		simpll3	$⊢ (((K \in HL \land X \in B \land Y \in B) \land \neg Y \underset{˙}{\leq} X) \land Y \in A) \to Y \in B$
16	1 3	latmcom	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \underset{˙}{\land} Y = Y \underset{˙}{\land} X$
17	13 14 15 16	syl3anc	$⊢ (((K \in HL \land X \in B \land Y \in B) \land \neg Y \underset{˙}{\leq} X) \land Y \in A) \to X \underset{˙}{\land} Y = Y \underset{˙}{\land} X$
18		simplr	$⊢ (((K \in HL \land X \in B \land Y \in B) \land \neg Y \underset{˙}{\leq} X) \land Y \in A) \to \neg Y \underset{˙}{\leq} X$
19	12 5	syl	$⊢ (((K \in HL \land X \in B \land Y \in B) \land \neg Y \underset{˙}{\leq} X) \land Y \in A) \to K \in AtLat$
20		simpr	$⊢ (((K \in HL \land X \in B \land Y \in B) \land \neg Y \underset{˙}{\leq} X) \land Y \in A) \to Y \in A$
21	1 2 3 8 4	atnle	$⊢ (K \in AtLat \land Y \in A \land X \in B) \to (\neg Y \underset{˙}{\leq} X \leftrightarrow Y \underset{˙}{\land} X = 0. (K))$
22	19 20 14 21	syl3anc	$⊢ (((K \in HL \land X \in B \land Y \in B) \land \neg Y \underset{˙}{\leq} X) \land Y \in A) \to (\neg Y \underset{˙}{\leq} X \leftrightarrow Y \underset{˙}{\land} X = 0. (K))$
23	18 22	mpbid	$⊢ (((K \in HL \land X \in B \land Y \in B) \land \neg Y \underset{˙}{\leq} X) \land Y \in A) \to Y \underset{˙}{\land} X = 0. (K)$
24	17 23	eqtrd	$⊢ (((K \in HL \land X \in B \land Y \in B) \land \neg Y \underset{˙}{\leq} X) \land Y \in A) \to X \underset{˙}{\land} Y = 0. (K)$
25	24	ex	$⊢ ((K \in HL \land X \in B \land Y \in B) \land \neg Y \underset{˙}{\leq} X) \to (Y \in A \to X \underset{˙}{\land} Y = 0. (K))$
26	25	necon3ad	$⊢ ((K \in HL \land X \in B \land Y \in B) \land \neg Y \underset{˙}{\leq} X) \to (X \underset{˙}{\land} Y \neq 0. (K) \to \neg Y \in A)$
27	11 26	syld	$⊢ ((K \in HL \land X \in B \land Y \in B) \land \neg Y \underset{˙}{\leq} X) \to (X \underset{˙}{\land} Y \in A \to \neg Y \in A)$
28	27	impr	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (\neg Y \underset{˙}{\leq} X \land X \underset{˙}{\land} Y \in A)) \to \neg Y \in A$

Metamath Proof Explorer

Theorem intnatN

Proof