cdleme11c

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

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

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		simp3l	$⊢ (((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 S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
8		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 (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to K \in HL$
9		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 (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to P \in A$
10		simp11	$⊢ (((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 (K \in HL \land W \in H)$
11		simp12	$⊢ (((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 (P \in A \land \neg P \underset{˙}{\leq} W)$
12		simp13	$⊢ (((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 Q \in A$
13		simp23	$⊢ (((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 P \neq Q$
14	1 2 3 4 5 6	lhpat2	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land P \neq Q)) \to U \in A$
15	10 11 12 13 14	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 (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to U \in A$
16	1 2 4	hlatlej1	$⊢ (K \in HL \land P \in A \land U \in A) \to P \underset{˙}{\leq} (P \underset{˙}{\lor} U)$
17	8 9 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 (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to P \underset{˙}{\leq} (P \underset{˙}{\lor} U)$
18	17	adantr	$⊢ ((((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))) \land P \underset{˙}{\leq} (S \underset{˙}{\lor} T)) \to P \underset{˙}{\leq} (P \underset{˙}{\lor} U)$
19	12 13	jca	$⊢ (((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 (Q \in A \land P \neq Q)$
20		simp21	$⊢ (((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 (S \in A \land \neg S \underset{˙}{\leq} W)$
21		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 (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to T \in A$
22		simp3r	$⊢ (((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 U \underset{˙}{\leq} (S \underset{˙}{\lor} T)$
23	21 22	jca	$⊢ (((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 (T \in A \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))$
24	1 2 3 4 5 6	cdleme11a	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land P \neq Q)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T)))) \to S \underset{˙}{\lor} U = S \underset{˙}{\lor} T$
25	10 11 19 20 23 24	syl122anc	$⊢ (((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 S \underset{˙}{\lor} U = S \underset{˙}{\lor} T$
26	25	breq2d	$⊢ (((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 (P \underset{˙}{\leq} (S \underset{˙}{\lor} U) \leftrightarrow P \underset{˙}{\leq} (S \underset{˙}{\lor} T))$
27		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 (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to S \in A$
28	1 2 3 4 5 6	cdleme0b	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \to U \neq P$
29	10 11 12 28	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 (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to U \neq P$
30	29	necomd	$⊢ (((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 P \neq U$
31	1 2 4	hlatexch2	$⊢ (K \in HL \land (P \in A \land S \in A \land U \in A) \land P \neq U) \to (P \underset{˙}{\leq} (S \underset{˙}{\lor} U) \to S \underset{˙}{\leq} (P \underset{˙}{\lor} U))$
32	8 9 27 15 30 31	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 (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to (P \underset{˙}{\leq} (S \underset{˙}{\lor} U) \to S \underset{˙}{\leq} (P \underset{˙}{\lor} U))$
33	26 32	sylbird	$⊢ (((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 (P \underset{˙}{\leq} (S \underset{˙}{\lor} T) \to S \underset{˙}{\leq} (P \underset{˙}{\lor} U))$
34	33	imp	$⊢ ((((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))) \land P \underset{˙}{\leq} (S \underset{˙}{\lor} T)) \to S \underset{˙}{\leq} (P \underset{˙}{\lor} U)$
35	1 2 4	hlatlej2	$⊢ (K \in HL \land P \in A \land Q \in A) \to Q \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
36	8 9 12 35	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 (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to Q \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
37	1 2 3 4 5 6	cdleme0cp	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A)) \to P \underset{˙}{\lor} U = P \underset{˙}{\lor} Q$
38	10 11 12 37	syl12anc	$⊢ (((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 P \underset{˙}{\lor} U = P \underset{˙}{\lor} Q$
39	36 38	breqtrrd	$⊢ (((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)$
40	39	adantr	$⊢ ((((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))) \land P \underset{˙}{\leq} (S \underset{˙}{\lor} T)) \to Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)$
41	8	hllatd	$⊢ (((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 K \in Lat$
42		eqid	$⊢ {Base}_{K} = {Base}_{K}$
43	42 4	atbase	$⊢ S \in A \to S \in {Base}_{K}$
44	27 43	syl	$⊢ (((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 S \in {Base}_{K}$
45	42 4	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
46	12 45	syl	$⊢ (((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 Q \in {Base}_{K}$
47	42 2 4	hlatjcl	$⊢ (K \in HL \land P \in A \land U \in A) \to P \underset{˙}{\lor} U \in {Base}_{K}$
48	8 9 15 47	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 (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to P \underset{˙}{\lor} U \in {Base}_{K}$
49	42 1 2	latjle12	$⊢ (K \in Lat \land (S \in {Base}_{K} \land Q \in {Base}_{K} \land P \underset{˙}{\lor} U \in {Base}_{K})) \to ((S \underset{˙}{\leq} (P \underset{˙}{\lor} U) \land Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)) \leftrightarrow (S \underset{˙}{\lor} Q) \underset{˙}{\leq} (P \underset{˙}{\lor} U))$
50	41 44 46 48 49	syl13anc	$⊢ (((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 ((S \underset{˙}{\leq} (P \underset{˙}{\lor} U) \land Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)) \leftrightarrow (S \underset{˙}{\lor} Q) \underset{˙}{\leq} (P \underset{˙}{\lor} U))$
51	50	adantr	$⊢ ((((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))) \land P \underset{˙}{\leq} (S \underset{˙}{\lor} T)) \to ((S \underset{˙}{\leq} (P \underset{˙}{\lor} U) \land Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)) \leftrightarrow (S \underset{˙}{\lor} Q) \underset{˙}{\leq} (P \underset{˙}{\lor} U))$
52	34 40 51	mpbi2and	$⊢ ((((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))) \land P \underset{˙}{\leq} (S \underset{˙}{\lor} T)) \to (S \underset{˙}{\lor} Q) \underset{˙}{\leq} (P \underset{˙}{\lor} U)$
53	42 4	atbase	$⊢ P \in A \to P \in {Base}_{K}$
54	9 53	syl	$⊢ (((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 P \in {Base}_{K}$
55	42 1 2	latnlej1r	$⊢ (K \in Lat \land (S \in {Base}_{K} \land P \in {Base}_{K} \land Q \in {Base}_{K}) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to S \neq Q$
56	41 44 54 46 7 55	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 (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to S \neq Q$
57	1 2 4	ps-1	$⊢ (K \in HL \land (S \in A \land Q \in A \land S \neq Q) \land (P \in A \land U \in A)) \to ((S \underset{˙}{\lor} Q) \underset{˙}{\leq} (P \underset{˙}{\lor} U) \leftrightarrow S \underset{˙}{\lor} Q = P \underset{˙}{\lor} U)$
58	8 27 12 56 9 15 57	syl132anc	$⊢ (((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 ((S \underset{˙}{\lor} Q) \underset{˙}{\leq} (P \underset{˙}{\lor} U) \leftrightarrow S \underset{˙}{\lor} Q = P \underset{˙}{\lor} U)$
59	58	adantr	$⊢ ((((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))) \land P \underset{˙}{\leq} (S \underset{˙}{\lor} T)) \to ((S \underset{˙}{\lor} Q) \underset{˙}{\leq} (P \underset{˙}{\lor} U) \leftrightarrow S \underset{˙}{\lor} Q = P \underset{˙}{\lor} U)$
60	52 59	mpbid	$⊢ ((((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))) \land P \underset{˙}{\leq} (S \underset{˙}{\lor} T)) \to S \underset{˙}{\lor} Q = P \underset{˙}{\lor} U$
61	18 60	breqtrrd	$⊢ ((((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))) \land P \underset{˙}{\leq} (S \underset{˙}{\lor} T)) \to P \underset{˙}{\leq} (S \underset{˙}{\lor} Q)$
62	61	ex	$⊢ (((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 (P \underset{˙}{\leq} (S \underset{˙}{\lor} T) \to P \underset{˙}{\leq} (S \underset{˙}{\lor} Q))$
63	1 2 4	hlatexch2	$⊢ (K \in HL \land (P \in A \land S \in A \land Q \in A) \land P \neq Q) \to (P \underset{˙}{\leq} (S \underset{˙}{\lor} Q) \to S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
64	8 9 27 12 13 63	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 (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to (P \underset{˙}{\leq} (S \underset{˙}{\lor} Q) \to S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
65	62 64	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 (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to (P \underset{˙}{\leq} (S \underset{˙}{\lor} T) \to S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
66	7 65	mtod	$⊢ (((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)$

Metamath Proof Explorer

Theorem cdleme11c

Proof