cdleme43bN

Description: Lemma for Lemma E in Crawley p. 113. g(s) is an atom not under w. (Contributed by NM, 20-Mar-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cdleme43.b	$⊢ B = {Base}_{K}$
	cdleme43.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdleme43.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdleme43.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdleme43.a	$⊢ A = Atoms (K)$
	cdleme43.h	$⊢ H = LHyp (K)$
	cdleme43.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
	cdleme43.x	$⊢ X = (Q \underset{˙}{\lor} P) \underset{˙}{\land} W$
	cdleme43.c	$⊢ C = (S \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W))$
	cdleme43.f	$⊢ Z = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (C \underset{˙}{\lor} ((R \underset{˙}{\lor} S) \underset{˙}{\land} W))$
	cdleme43.d	$⊢ D = (S \underset{˙}{\lor} X) \underset{˙}{\land} (P \underset{˙}{\lor} ((Q \underset{˙}{\lor} S) \underset{˙}{\land} W))$
	cdleme43.g	$⊢ G = (Q \underset{˙}{\lor} P) \underset{˙}{\land} (D \underset{˙}{\lor} ((Z \underset{˙}{\lor} S) \underset{˙}{\land} W))$
	cdleme43.e	$⊢ E = (D \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} D) \underset{˙}{\land} W))$
	cdleme43.v	$⊢ V = (Z \underset{˙}{\lor} S) \underset{˙}{\land} W$
	cdleme43.y	$⊢ Y = (R \underset{˙}{\lor} D) \underset{˙}{\land} W$
Assertion	cdleme43bN	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (D \in A \land \neg D \underset{˙}{\leq} W)$

Proof

Step	Hyp	Ref	Expression
1		cdleme43.b	$⊢ B = {Base}_{K}$
2		cdleme43.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cdleme43.j	$⊢ \underset{˙}{\lor} = join (K)$
4		cdleme43.m	$⊢ \underset{˙}{\land} = meet (K)$
5		cdleme43.a	$⊢ A = Atoms (K)$
6		cdleme43.h	$⊢ H = LHyp (K)$
7		cdleme43.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
8		cdleme43.x	$⊢ X = (Q \underset{˙}{\lor} P) \underset{˙}{\land} W$
9		cdleme43.c	$⊢ C = (S \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W))$
10		cdleme43.f	$⊢ Z = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (C \underset{˙}{\lor} ((R \underset{˙}{\lor} S) \underset{˙}{\land} W))$
11		cdleme43.d	$⊢ D = (S \underset{˙}{\lor} X) \underset{˙}{\land} (P \underset{˙}{\lor} ((Q \underset{˙}{\lor} S) \underset{˙}{\land} W))$
12		cdleme43.g	$⊢ G = (Q \underset{˙}{\lor} P) \underset{˙}{\land} (D \underset{˙}{\lor} ((Z \underset{˙}{\lor} S) \underset{˙}{\land} W))$
13		cdleme43.e	$⊢ E = (D \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} D) \underset{˙}{\land} W))$
14		cdleme43.v	$⊢ V = (Z \underset{˙}{\lor} S) \underset{˙}{\land} W$
15		cdleme43.y	$⊢ Y = (R \underset{˙}{\lor} D) \underset{˙}{\land} W$
16		simp11	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (K \in HL \land W \in H)$
17		simp13	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
18		simp12	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
19		simp2r	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (S \in A \land \neg S \underset{˙}{\leq} W)$
20		simp2l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to P \neq Q$
21	20	necomd	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to Q \neq P$
22		simp3	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
23		simp11l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to K \in HL$
24		simp12l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to P \in A$
25		simp13l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to Q \in A$
26	3 5	hlatjcom	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} Q = Q \underset{˙}{\lor} P$
27	23 24 25 26	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to P \underset{˙}{\lor} Q = Q \underset{˙}{\lor} P$
28	27	breq2d	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \leftrightarrow S \underset{˙}{\leq} (Q \underset{˙}{\lor} P))$
29	22 28	mtbid	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} P)$
30	2 3 4 5 6 8 11	cdleme3fa	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (Q \neq P \land \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} P))) \to D \in A$
31	16 17 18 19 21 29 30	syl132anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to D \in A$
32	2 3 4 5 6 8 11	cdleme3	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (Q \neq P \land \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} P))) \to \neg D \underset{˙}{\leq} W$
33	16 17 18 19 21 29 32	syl132anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to \neg D \underset{˙}{\leq} W$
34	31 33	jca	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (D \in A \land \neg D \underset{˙}{\leq} W)$

Metamath Proof Explorer

Theorem cdleme43bN

Proof