cdleme19b

Description: Part of proof of Lemma E in Crawley p. 113, 5th paragraph on p. 114, 1st line. D , F , G represent s_2, f(s), f(t). In their notation, we prove that if r <_ s \/ t, then s_2 <_ f(s) \/ f(t). (Contributed by NM, 13-Nov-2012)

	Ref	Expression
Hypotheses	cdleme19.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdleme19.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdleme19.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdleme19.a	$⊢ A = Atoms (K)$
	cdleme19.h	$⊢ H = LHyp (K)$
	cdleme19.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
	cdleme19.f	$⊢ F = (S \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W))$
	cdleme19.g	$⊢ G = (T \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} T) \underset{˙}{\land} W))$
	cdleme19.d	$⊢ D = (R \underset{˙}{\lor} S) \underset{˙}{\land} W$
	cdleme19.y	$⊢ Y = (R \underset{˙}{\lor} T) \underset{˙}{\land} W$
Assertion	cdleme19b	$⊢ (((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 ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land R \in A) \land ((P \neq Q \land S \neq T) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \underset{˙}{\leq} (S \underset{˙}{\lor} T)))) \to D \underset{˙}{\leq} (F \underset{˙}{\lor} G)$

Proof

Step	Hyp	Ref	Expression
1		cdleme19.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdleme19.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdleme19.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdleme19.a	$⊢ A = Atoms (K)$
5		cdleme19.h	$⊢ H = LHyp (K)$
6		cdleme19.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
7		cdleme19.f	$⊢ F = (S \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W))$
8		cdleme19.g	$⊢ G = (T \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} T) \underset{˙}{\land} W))$
9		cdleme19.d	$⊢ D = (R \underset{˙}{\lor} S) \underset{˙}{\land} W$
10		cdleme19.y	$⊢ Y = (R \underset{˙}{\lor} T) \underset{˙}{\land} W$
11		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 ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land R \in A) \land ((P \neq Q \land S \neq T) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \underset{˙}{\leq} (S \underset{˙}{\lor} T)))) \to K \in HL$
12		simp23	$⊢ (((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 ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land R \in A) \land ((P \neq Q \land S \neq T) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \underset{˙}{\leq} (S \underset{˙}{\lor} T)))) \to R \in A$
13		simp21l	$⊢ (((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 ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land R \in A) \land ((P \neq Q \land S \neq T) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \underset{˙}{\leq} (S \underset{˙}{\lor} T)))) \to S \in A$
14		simp22l	$⊢ (((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 ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land R \in A) \land ((P \neq Q \land S \neq T) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \underset{˙}{\leq} (S \underset{˙}{\lor} T)))) \to T \in A$
15		simp33l	$⊢ (((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 ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land R \in A) \land ((P \neq Q \land S \neq T) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \underset{˙}{\leq} (S \underset{˙}{\lor} T)))) \to R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
16		simp32l	$⊢ (((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 ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land R \in A) \land ((P \neq Q \land S \neq T) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \underset{˙}{\leq} (S \underset{˙}{\lor} T)))) \to \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
17		simp33r	$⊢ (((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 ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land R \in A) \land ((P \neq Q \land S \neq T) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \underset{˙}{\leq} (S \underset{˙}{\lor} T)))) \to R \underset{˙}{\leq} (S \underset{˙}{\lor} T)$
18	1 2 3 4 5 6 7 8 9 10	cdleme19a	$⊢ (K \in HL \land (R \in A \land S \in A \land T \in A) \land (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to D = (S \underset{˙}{\lor} T) \underset{˙}{\land} W$
19	11 12 13 14 15 16 17 18	syl133anc	$⊢ (((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 ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land R \in A) \land ((P \neq Q \land S \neq T) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \underset{˙}{\leq} (S \underset{˙}{\lor} T)))) \to D = (S \underset{˙}{\lor} T) \underset{˙}{\land} W$
20		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 ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land R \in A) \land ((P \neq Q \land S \neq T) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \underset{˙}{\leq} (S \underset{˙}{\lor} T)))) \to (K \in HL \land W \in H)$
21		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 ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land R \in A) \land ((P \neq Q \land S \neq T) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \underset{˙}{\leq} (S \underset{˙}{\lor} T)))) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
22		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 ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land R \in A) \land ((P \neq Q \land S \neq T) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \underset{˙}{\leq} (S \underset{˙}{\lor} T)))) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
23		simp21	$⊢ (((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 ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land R \in A) \land ((P \neq Q \land S \neq T) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \underset{˙}{\leq} (S \underset{˙}{\lor} T)))) \to (S \in A \land \neg S \underset{˙}{\leq} W)$
24		simp22	$⊢ (((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 ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land R \in A) \land ((P \neq Q \land S \neq T) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \underset{˙}{\leq} (S \underset{˙}{\lor} T)))) \to (T \in A \land \neg T \underset{˙}{\leq} W)$
25		simp31	$⊢ (((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 ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land R \in A) \land ((P \neq Q \land S \neq T) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \underset{˙}{\leq} (S \underset{˙}{\lor} T)))) \to (P \neq Q \land S \neq T)$
26		simp32r	$⊢ (((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 ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land R \in A) \land ((P \neq Q \land S \neq T) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \underset{˙}{\leq} (S \underset{˙}{\lor} T)))) \to \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
27	1 2 3 4 5 6 7 8	cdleme16	$⊢ (((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 ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (S \underset{˙}{\lor} T) \underset{˙}{\land} W = (F \underset{˙}{\lor} G) \underset{˙}{\land} W$
28	20 21 22 23 24 25 16 26 27	syl332anc	$⊢ (((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 ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land R \in A) \land ((P \neq Q \land S \neq T) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \underset{˙}{\leq} (S \underset{˙}{\lor} T)))) \to (S \underset{˙}{\lor} T) \underset{˙}{\land} W = (F \underset{˙}{\lor} G) \underset{˙}{\land} W$
29	19 28	eqtrd	$⊢ (((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 ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land R \in A) \land ((P \neq Q \land S \neq T) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \underset{˙}{\leq} (S \underset{˙}{\lor} T)))) \to D = (F \underset{˙}{\lor} G) \underset{˙}{\land} W$
30	11	hllatd	$⊢ (((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 ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land R \in A) \land ((P \neq Q \land S \neq T) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \underset{˙}{\leq} (S \underset{˙}{\lor} T)))) \to K \in Lat$
31		simp11r	$⊢ (((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 ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land R \in A) \land ((P \neq Q \land S \neq T) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \underset{˙}{\leq} (S \underset{˙}{\lor} T)))) \to W \in H$
32		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 ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land R \in A) \land ((P \neq Q \land S \neq T) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \underset{˙}{\leq} (S \underset{˙}{\lor} T)))) \to P \in A$
33		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 ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land R \in A) \land ((P \neq Q \land S \neq T) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \underset{˙}{\leq} (S \underset{˙}{\lor} T)))) \to Q \in A$
34		eqid	$⊢ {Base}_{K} = {Base}_{K}$
35	1 2 3 4 5 6 7 34	cdleme1b	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land S \in A)) \to F \in {Base}_{K}$
36	11 31 32 33 13 35	syl23anc	$⊢ (((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 ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land R \in A) \land ((P \neq Q \land S \neq T) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \underset{˙}{\leq} (S \underset{˙}{\lor} T)))) \to F \in {Base}_{K}$
37	1 2 3 4 5 6 8 34	cdleme1b	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land T \in A)) \to G \in {Base}_{K}$
38	11 31 32 33 14 37	syl23anc	$⊢ (((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 ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land R \in A) \land ((P \neq Q \land S \neq T) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \underset{˙}{\leq} (S \underset{˙}{\lor} T)))) \to G \in {Base}_{K}$
39	34 2	latjcl	$⊢ (K \in Lat \land F \in {Base}_{K} \land G \in {Base}_{K}) \to F \underset{˙}{\lor} G \in {Base}_{K}$
40	30 36 38 39	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 ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land R \in A) \land ((P \neq Q \land S \neq T) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \underset{˙}{\leq} (S \underset{˙}{\lor} T)))) \to F \underset{˙}{\lor} G \in {Base}_{K}$
41	34 5	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
42	31 41	syl	$⊢ (((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 ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land R \in A) \land ((P \neq Q \land S \neq T) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \underset{˙}{\leq} (S \underset{˙}{\lor} T)))) \to W \in {Base}_{K}$
43	34 1 3	latmle1	$⊢ (K \in Lat \land F \underset{˙}{\lor} G \in {Base}_{K} \land W \in {Base}_{K}) \to ((F \underset{˙}{\lor} G) \underset{˙}{\land} W) \underset{˙}{\leq} (F \underset{˙}{\lor} G)$
44	30 40 42 43	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 ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land R \in A) \land ((P \neq Q \land S \neq T) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \underset{˙}{\leq} (S \underset{˙}{\lor} T)))) \to ((F \underset{˙}{\lor} G) \underset{˙}{\land} W) \underset{˙}{\leq} (F \underset{˙}{\lor} G)$
45	29 44	eqbrtrd	$⊢ (((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 ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land R \in A) \land ((P \neq Q \land S \neq T) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \underset{˙}{\leq} (S \underset{˙}{\lor} T)))) \to D \underset{˙}{\leq} (F \underset{˙}{\lor} G)$

Metamath Proof Explorer

Theorem cdleme19b

Proof