Metamath Proof Explorer

Theorem pexmidlem5N

Description: Lemma for pexmidN . (Contributed by NM, 2-Feb-2012) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		pexmidlem.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		pexmidlem.j	$⊢ \underset{˙}{\lor} = join (K)$
3		pexmidlem.a	$⊢ A = Atoms (K)$
4		pexmidlem.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
5		pexmidlem.o	$⊢ \underset{˙}{⊥} = ⊥_{𝑃} (K)$
6		pexmidlem.m	$⊢ M = X \underset{˙}{+} \{p\}$
7		n0	$⊢ \underset{˙}{⊥} (X) \cap M \neq \emptyset \leftrightarrow \exists q q \in (\underset{˙}{⊥} (X) \cap M)$
8	1 2 3 4 5 6	pexmidlem4N	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (X \neq \emptyset \land q \in (\underset{˙}{⊥} (X) \cap M))) \to p \in (X \underset{˙}{+} \underset{˙}{⊥} (X))$
9	8	expr	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land X \neq \emptyset) \to (q \in (\underset{˙}{⊥} (X) \cap M) \to p \in (X \underset{˙}{+} \underset{˙}{⊥} (X)))$
10	9	exlimdv	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land X \neq \emptyset) \to (\exists q q \in (\underset{˙}{⊥} (X) \cap M) \to p \in (X \underset{˙}{+} \underset{˙}{⊥} (X)))$
11	7 10	syl5bi	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land X \neq \emptyset) \to (\underset{˙}{⊥} (X) \cap M \neq \emptyset \to p \in (X \underset{˙}{+} \underset{˙}{⊥} (X)))$
12	11	necon1bd	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land X \neq \emptyset) \to (\neg p \in (X \underset{˙}{+} \underset{˙}{⊥} (X)) \to \underset{˙}{⊥} (X) \cap M = \emptyset)$
13	12	impr	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (X \neq \emptyset \land \neg p \in (X \underset{˙}{+} \underset{˙}{⊥} (X)))) \to \underset{˙}{⊥} (X) \cap M = \emptyset$