cdleme11dN

Description: Part of proof of Lemma E in Crawley p. 113. Lemma leading to cdleme11 . (Contributed by NM, 13-Jun-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cdleme11.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdleme11.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdleme11.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdleme11.a	$⊢ A = Atoms (K)$
	cdleme11.h	$⊢ H = LHyp (K)$
	cdleme11.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
Assertion	cdleme11dN	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land P \neq Q) \land (S \neq T \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to P \underset{˙}{\lor} S \neq P \underset{˙}{\lor} T$

Proof

Step	Hyp	Ref	Expression
1		cdleme11.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdleme11.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdleme11.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdleme11.a	$⊢ A = Atoms (K)$
5		cdleme11.h	$⊢ H = LHyp (K)$
6		cdleme11.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
7		simp1	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land P \neq Q) \land (S \neq T \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A)$
8		simp2	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land P \neq Q) \land (S \neq T \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land P \neq Q)$
9		simp32	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land P \neq Q) \land (S \neq T \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
10		simp33	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land P \neq Q) \land (S \neq T \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to U \underset{˙}{\leq} (S \underset{˙}{\lor} T)$
11	1 2 3 4 5 6	cdleme11c	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land P \neq Q) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to \neg P \underset{˙}{\leq} (S \underset{˙}{\lor} T)$
12	7 8 9 10 11	syl112anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land P \neq Q) \land (S \neq T \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to \neg P \underset{˙}{\leq} (S \underset{˙}{\lor} T)$
13		simp11l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land P \neq Q) \land (S \neq T \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to K \in HL$
14		simp12l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land P \neq Q) \land (S \neq T \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to P \in A$
15		simp21l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land P \neq Q) \land (S \neq T \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to S \in A$
16	1 2 4	hlatlej2	$⊢ (K \in HL \land P \in A \land S \in A) \to S \underset{˙}{\leq} (P \underset{˙}{\lor} S)$
17	13 14 15 16	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land P \neq Q) \land (S \neq T \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to S \underset{˙}{\leq} (P \underset{˙}{\lor} S)$
18		breq2	$⊢ P \underset{˙}{\lor} S = P \underset{˙}{\lor} T \to (S \underset{˙}{\leq} (P \underset{˙}{\lor} S) \leftrightarrow S \underset{˙}{\leq} (P \underset{˙}{\lor} T))$
19	17 18	syl5ibcom	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land P \neq Q) \land (S \neq T \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to (P \underset{˙}{\lor} S = P \underset{˙}{\lor} T \to S \underset{˙}{\leq} (P \underset{˙}{\lor} T))$
20		simp22	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land P \neq Q) \land (S \neq T \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to T \in A$
21		simp31	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land P \neq Q) \land (S \neq T \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to S \neq T$
22	1 2 4	hlatexch2	$⊢ (K \in HL \land (S \in A \land P \in A \land T \in A) \land S \neq T) \to (S \underset{˙}{\leq} (P \underset{˙}{\lor} T) \to P \underset{˙}{\leq} (S \underset{˙}{\lor} T))$
23	13 15 14 20 21 22	syl131anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land P \neq Q) \land (S \neq T \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to (S \underset{˙}{\leq} (P \underset{˙}{\lor} T) \to P \underset{˙}{\leq} (S \underset{˙}{\lor} T))$
24	19 23	syld	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land P \neq Q) \land (S \neq T \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to (P \underset{˙}{\lor} S = P \underset{˙}{\lor} T \to P \underset{˙}{\leq} (S \underset{˙}{\lor} T))$
25	24	necon3bd	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land P \neq Q) \land (S \neq T \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to (\neg P \underset{˙}{\leq} (S \underset{˙}{\lor} T) \to P \underset{˙}{\lor} S \neq P \underset{˙}{\lor} T)$
26	12 25	mpd	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land T \in A \land P \neq Q) \land (S \neq T \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to P \underset{˙}{\lor} S \neq P \underset{˙}{\lor} T$

Metamath Proof Explorer

Theorem cdleme11dN

Proof