Metamath Proof Explorer

Theorem pexmidlem1N

Description: Lemma for pexmidN . Holland's proof implicitly requires q =/= r , which we prove here. (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	pexmidlem1N	$⊢ ((K \in HL \land X \subseteq A) \land (r \in X \land q \in \underset{˙}{⊥} (X))) \to q \neq r$

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		n0i	$⊢ r \in (X \cap \underset{˙}{⊥} (X)) \to \neg X \cap \underset{˙}{⊥} (X) = \emptyset$
8	3 5	pnonsingN	$⊢ (K \in HL \land X \subseteq A) \to X \cap \underset{˙}{⊥} (X) = \emptyset$
9	8	adantr	$⊢ ((K \in HL \land X \subseteq A) \land (r \in X \land q \in \underset{˙}{⊥} (X))) \to X \cap \underset{˙}{⊥} (X) = \emptyset$
10	7 9	nsyl3	$⊢ ((K \in HL \land X \subseteq A) \land (r \in X \land q \in \underset{˙}{⊥} (X))) \to \neg r \in (X \cap \underset{˙}{⊥} (X))$
11		simprr	$⊢ ((K \in HL \land X \subseteq A) \land (r \in X \land q \in \underset{˙}{⊥} (X))) \to q \in \underset{˙}{⊥} (X)$
12		eleq1w	$⊢ q = r \to (q \in \underset{˙}{⊥} (X) \leftrightarrow r \in \underset{˙}{⊥} (X))$
13	11 12	syl5ibcom	$⊢ ((K \in HL \land X \subseteq A) \land (r \in X \land q \in \underset{˙}{⊥} (X))) \to (q = r \to r \in \underset{˙}{⊥} (X))$
14		simprl	$⊢ ((K \in HL \land X \subseteq A) \land (r \in X \land q \in \underset{˙}{⊥} (X))) \to r \in X$
15	13 14	jctild	$⊢ ((K \in HL \land X \subseteq A) \land (r \in X \land q \in \underset{˙}{⊥} (X))) \to (q = r \to (r \in X \land r \in \underset{˙}{⊥} (X)))$
16		elin	$⊢ r \in (X \cap \underset{˙}{⊥} (X)) \leftrightarrow (r \in X \land r \in \underset{˙}{⊥} (X))$
17	15 16	imbitrrdi	$⊢ ((K \in HL \land X \subseteq A) \land (r \in X \land q \in \underset{˙}{⊥} (X))) \to (q = r \to r \in (X \cap \underset{˙}{⊥} (X)))$
18	17	necon3bd	$⊢ ((K \in HL \land X \subseteq A) \land (r \in X \land q \in \underset{˙}{⊥} (X))) \to (\neg r \in (X \cap \underset{˙}{⊥} (X)) \to q \neq r)$
19	10 18	mpd	$⊢ ((K \in HL \land X \subseteq A) \land (r \in X \land q \in \underset{˙}{⊥} (X))) \to q \neq r$