pexmidlem4N

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	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))$

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		simpl1	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (X \neq \emptyset \land q \in (\underset{˙}{⊥} (X) \cap M))) \to K \in HL$
8	7	hllatd	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (X \neq \emptyset \land q \in (\underset{˙}{⊥} (X) \cap M))) \to K \in Lat$
9		simpl2	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (X \neq \emptyset \land q \in (\underset{˙}{⊥} (X) \cap M))) \to X \subseteq A$
10		simpl3	$⊢ ((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 A$
11		simprl	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (X \neq \emptyset \land q \in (\underset{˙}{⊥} (X) \cap M))) \to X \neq \emptyset$
12		inss2	$⊢ \underset{˙}{⊥} (X) \cap M \subseteq M$
13	12	sseli	$⊢ q \in (\underset{˙}{⊥} (X) \cap M) \to q \in M$
14	13 6	eleqtrdi	$⊢ q \in (\underset{˙}{⊥} (X) \cap M) \to q \in (X \underset{˙}{+} \{p\})$
15	14	ad2antll	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (X \neq \emptyset \land q \in (\underset{˙}{⊥} (X) \cap M))) \to q \in (X \underset{˙}{+} \{p\})$
16	1 2 3 4	elpaddatiN	$⊢ ((K \in Lat \land X \subseteq A \land p \in A) \land (X \neq \emptyset \land q \in (X \underset{˙}{+} \{p\}))) \to \exists r \in X q \underset{˙}{\leq} (r \underset{˙}{\lor} p)$
17	8 9 10 11 15 16	syl32anc	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (X \neq \emptyset \land q \in (\underset{˙}{⊥} (X) \cap M))) \to \exists r \in X q \underset{˙}{\leq} (r \underset{˙}{\lor} p)$
18		simp1	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (X \neq \emptyset \land q \in (\underset{˙}{⊥} (X) \cap M)) \land (r \in X \land q \underset{˙}{\leq} (r \underset{˙}{\lor} p))) \to (K \in HL \land X \subseteq A \land p \in A)$
19		simp3l	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (X \neq \emptyset \land q \in (\underset{˙}{⊥} (X) \cap M)) \land (r \in X \land q \underset{˙}{\leq} (r \underset{˙}{\lor} p))) \to r \in X$
20		inss1	$⊢ \underset{˙}{⊥} (X) \cap M \subseteq \underset{˙}{⊥} (X)$
21		simp2r	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (X \neq \emptyset \land q \in (\underset{˙}{⊥} (X) \cap M)) \land (r \in X \land q \underset{˙}{\leq} (r \underset{˙}{\lor} p))) \to q \in (\underset{˙}{⊥} (X) \cap M)$
22	20 21	sseldi	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (X \neq \emptyset \land q \in (\underset{˙}{⊥} (X) \cap M)) \land (r \in X \land q \underset{˙}{\leq} (r \underset{˙}{\lor} p))) \to q \in \underset{˙}{⊥} (X)$
23		simp3r	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (X \neq \emptyset \land q \in (\underset{˙}{⊥} (X) \cap M)) \land (r \in X \land q \underset{˙}{\leq} (r \underset{˙}{\lor} p))) \to q \underset{˙}{\leq} (r \underset{˙}{\lor} p)$
24	1 2 3 4 5 6	pexmidlem3N	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (r \in X \land q \in \underset{˙}{⊥} (X)) \land q \underset{˙}{\leq} (r \underset{˙}{\lor} p)) \to p \in (X \underset{˙}{+} \underset{˙}{⊥} (X))$
25	18 19 22 23 24	syl121anc	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (X \neq \emptyset \land q \in (\underset{˙}{⊥} (X) \cap M)) \land (r \in X \land q \underset{˙}{\leq} (r \underset{˙}{\lor} p))) \to p \in (X \underset{˙}{+} \underset{˙}{⊥} (X))$
26	25	3expia	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (X \neq \emptyset \land q \in (\underset{˙}{⊥} (X) \cap M))) \to ((r \in X \land q \underset{˙}{\leq} (r \underset{˙}{\lor} p)) \to p \in (X \underset{˙}{+} \underset{˙}{⊥} (X)))$
27	26	expd	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (X \neq \emptyset \land q \in (\underset{˙}{⊥} (X) \cap M))) \to (r \in X \to (q \underset{˙}{\leq} (r \underset{˙}{\lor} p) \to p \in (X \underset{˙}{+} \underset{˙}{⊥} (X))))$
28	27	rexlimdv	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (X \neq \emptyset \land q \in (\underset{˙}{⊥} (X) \cap M))) \to (\exists r \in X q \underset{˙}{\leq} (r \underset{˙}{\lor} p) \to p \in (X \underset{˙}{+} \underset{˙}{⊥} (X)))$
29	17 28	mpd	$⊢ ((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))$

Metamath Proof Explorer

Theorem pexmidlem4N

Proof