Metamath Proof Explorer

Theorem pexmidlem2N

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	pexmidlem2N	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (r \in X \land q \in \underset{˙}{⊥} (X) \land p \underset{˙}{\leq} (r \underset{˙}{\lor} q))) \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 (r \in X \land q \in \underset{˙}{⊥} (X) \land p \underset{˙}{\leq} (r \underset{˙}{\lor} q))) \to K \in HL$
8	7	hllatd	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (r \in X \land q \in \underset{˙}{⊥} (X) \land p \underset{˙}{\leq} (r \underset{˙}{\lor} q))) \to K \in Lat$
9		simpl2	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (r \in X \land q \in \underset{˙}{⊥} (X) \land p \underset{˙}{\leq} (r \underset{˙}{\lor} q))) \to X \subseteq A$
10	3 5	polssatN	$⊢ (K \in HL \land X \subseteq A) \to \underset{˙}{⊥} (X) \subseteq A$
11	7 9 10	syl2anc	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (r \in X \land q \in \underset{˙}{⊥} (X) \land p \underset{˙}{\leq} (r \underset{˙}{\lor} q))) \to \underset{˙}{⊥} (X) \subseteq A$
12		simpr1	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (r \in X \land q \in \underset{˙}{⊥} (X) \land p \underset{˙}{\leq} (r \underset{˙}{\lor} q))) \to r \in X$
13		simpr2	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (r \in X \land q \in \underset{˙}{⊥} (X) \land p \underset{˙}{\leq} (r \underset{˙}{\lor} q))) \to q \in \underset{˙}{⊥} (X)$
14		simpl3	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (r \in X \land q \in \underset{˙}{⊥} (X) \land p \underset{˙}{\leq} (r \underset{˙}{\lor} q))) \to p \in A$
15		simpr3	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (r \in X \land q \in \underset{˙}{⊥} (X) \land p \underset{˙}{\leq} (r \underset{˙}{\lor} q))) \to p \underset{˙}{\leq} (r \underset{˙}{\lor} q)$
16	1 2 3 4	elpaddri	$⊢ ((K \in Lat \land X \subseteq A \land \underset{˙}{⊥} (X) \subseteq A) \land (r \in X \land q \in \underset{˙}{⊥} (X)) \land (p \in A \land p \underset{˙}{\leq} (r \underset{˙}{\lor} q))) \to p \in (X \underset{˙}{+} \underset{˙}{⊥} (X))$
17	8 9 11 12 13 14 15 16	syl322anc	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (r \in X \land q \in \underset{˙}{⊥} (X) \land p \underset{˙}{\leq} (r \underset{˙}{\lor} q))) \to p \in (X \underset{˙}{+} \underset{˙}{⊥} (X))$