Metamath Proof Explorer

Theorem osumcllem8N

Description: Lemma for osumclN . (Contributed by NM, 24-Mar-2012) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	osumcllem.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
		osumcllem.j	$⊢ \underset{˙}{\lor} = join (K)$
		osumcllem.a	$⊢ A = Atoms (K)$
		osumcllem.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
		osumcllem.o	$⊢ \underset{˙}{⊥} = ⊥_{𝑃} (K)$
		osumcllem.c	$⊢ C = PSubCl (K)$
		osumcllem.m	$⊢ M = X \underset{˙}{+} \{p\}$
		osumcllem.u	$⊢ U = \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y))$
	Assertion	osumcllem8N	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in A) \land \neg p \in (X \underset{˙}{+} Y)) \to Y \cap M = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		osumcllem.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		osumcllem.j	$⊢ \underset{˙}{\lor} = join (K)$
3		osumcllem.a	$⊢ A = Atoms (K)$
4		osumcllem.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
5		osumcllem.o	$⊢ \underset{˙}{⊥} = ⊥_{𝑃} (K)$
6		osumcllem.c	$⊢ C = PSubCl (K)$
7		osumcllem.m	$⊢ M = X \underset{˙}{+} \{p\}$
8		osumcllem.u	$⊢ U = \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y))$
9		n0	$⊢ Y \cap M \neq \emptyset \leftrightarrow \exists q q \in (Y \cap M)$
10	1 2 3 4 5 6 7 8	osumcllem7N	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in A) \land q \in (Y \cap M)) \to p \in (X \underset{˙}{+} Y)$
11	10	3expia	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in A)) \to (q \in (Y \cap M) \to p \in (X \underset{˙}{+} Y))$
12	11	exlimdv	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in A)) \to (\exists q q \in (Y \cap M) \to p \in (X \underset{˙}{+} Y))$
13	9 12	biimtrid	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in A)) \to (Y \cap M \neq \emptyset \to p \in (X \underset{˙}{+} Y))$
14	13	necon1bd	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in A)) \to (\neg p \in (X \underset{˙}{+} Y) \to Y \cap M = \emptyset)$
15	14	3impia	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in A) \land \neg p \in (X \underset{˙}{+} Y)) \to Y \cap M = \emptyset$