cdleme20j

Description: Part of proof of Lemma E in Crawley p. 113, last paragraph on p. 114. D , F , Y , G represent s_2, f(s), t_2, f(t). We show s_2 =/= t_2. (Contributed by NM, 18-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$
	cdleme20.v	$⊢ V = (S \underset{˙}{\lor} T) \underset{˙}{\land} W$
Assertion	cdleme20j	$⊢ (((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to D \neq Y$

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		cdleme20.v	$⊢ V = (S \underset{˙}{\lor} T) \underset{˙}{\land} W$
12		simp33	$⊢ (((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to \neg R \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 \neg Q \underset{˙}{\leq} W)) \land ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to K \in HL$
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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to S \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 \neg Q \underset{˙}{\leq} W)) \land ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to R \in A$
16		eqid	$⊢ {Base}_{K} = {Base}_{K}$
17	16 2 4	hlatjcl	$⊢ (K \in HL \land R \in A \land S \in A) \to R \underset{˙}{\lor} S \in {Base}_{K}$
18	13 15 14 17	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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to R \underset{˙}{\lor} S \in {Base}_{K}$
19		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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to W \in H$
20	16 5	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
21	19 20	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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to W \in {Base}_{K}$
22	1 2 4	hlatlej2	$⊢ (K \in HL \land R \in A \land S \in A) \to S \underset{˙}{\leq} (R \underset{˙}{\lor} S)$
23	13 15 14 22	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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to S \underset{˙}{\leq} (R \underset{˙}{\lor} S)$
24	16 1 2 3 4	atmod2i1	$⊢ (K \in HL \land (S \in A \land R \underset{˙}{\lor} S \in {Base}_{K} \land W \in {Base}_{K}) \land S \underset{˙}{\leq} (R \underset{˙}{\lor} S)) \to ((R \underset{˙}{\lor} S) \underset{˙}{\land} W) \underset{˙}{\lor} S = (R \underset{˙}{\lor} S) \underset{˙}{\land} (W \underset{˙}{\lor} S)$
25	13 14 18 21 23 24	syl131anc	$⊢ (((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to ((R \underset{˙}{\lor} S) \underset{˙}{\land} W) \underset{˙}{\lor} S = (R \underset{˙}{\lor} S) \underset{˙}{\land} (W \underset{˙}{\lor} S)$
26		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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to (S \in A \land \neg S \underset{˙}{\leq} W)$
27		eqid	$⊢ 1. (K) = 1. (K)$
28	1 2 27 4 5	lhpjat1	$⊢ ((K \in HL \land W \in H) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \to W \underset{˙}{\lor} S = 1. (K)$
29	13 19 26 28	syl21anc	$⊢ (((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to W \underset{˙}{\lor} S = 1. (K)$
30	29	oveq2d	$⊢ (((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to (R \underset{˙}{\lor} S) \underset{˙}{\land} (W \underset{˙}{\lor} S) = (R \underset{˙}{\lor} S) \underset{˙}{\land} 1. (K)$
31		hlol	$⊢ K \in HL \to K \in OL$
32	13 31	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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to K \in OL$
33	16 3 27	olm11	$⊢ (K \in OL \land R \underset{˙}{\lor} S \in {Base}_{K}) \to (R \underset{˙}{\lor} S) \underset{˙}{\land} 1. (K) = R \underset{˙}{\lor} S$
34	32 18 33	syl2anc	$⊢ (((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to (R \underset{˙}{\lor} S) \underset{˙}{\land} 1. (K) = R \underset{˙}{\lor} S$
35	25 30 34	3eqtrd	$⊢ (((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to ((R \underset{˙}{\lor} S) \underset{˙}{\land} W) \underset{˙}{\lor} S = R \underset{˙}{\lor} S$
36	35	adantr	$⊢ ((((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land D = Y) \to ((R \underset{˙}{\lor} S) \underset{˙}{\land} W) \underset{˙}{\lor} S = R \underset{˙}{\lor} S$
37		simp1	$⊢ (((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \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 \land \neg Q \underset{˙}{\leq} W))$
38		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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to (T \in A \land \neg T \underset{˙}{\leq} W)$
39		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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to (R \in A \land \neg R \underset{˙}{\leq} W)$
40		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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to (P \neq Q \land S \neq T)$
41		simp321	$⊢ (((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
42		simp322	$⊢ (((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
43	41 42	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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
44		simp323	$⊢ (((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
45	1 2 3 4 5 6 7 8 9 10 11	cdleme20d	$⊢ (((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 \neg R \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)) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (F \underset{˙}{\lor} G) \underset{˙}{\land} (D \underset{˙}{\lor} Y) = V$
46	37 26 38 39 40 43 44 45	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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to (F \underset{˙}{\lor} G) \underset{˙}{\land} (D \underset{˙}{\lor} Y) = V$
47	13	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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to K \in Lat$
48		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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to P \in A$
49		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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to Q \in A$
50	1 2 3 4 5 6 7 16	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}$
51	13 19 48 49 14 50	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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to F \in {Base}_{K}$
52		simp23l	$⊢ (((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to T \in A$
53	1 2 3 4 5 6 8 16	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}$
54	13 19 48 49 52 53	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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to G \in {Base}_{K}$
55	16 2	latjcl	$⊢ (K \in Lat \land F \in {Base}_{K} \land G \in {Base}_{K}) \to F \underset{˙}{\lor} G \in {Base}_{K}$
56	47 51 54 55	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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to F \underset{˙}{\lor} G \in {Base}_{K}$
57		simp22r	$⊢ (((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to \neg S \underset{˙}{\leq} W$
58	1 2 3 4 5 9	cdlemeda	$⊢ ((K \in HL \land W \in H) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (R \in A \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to D \in A$
59	13 19 14 57 15 44 41 58	syl223anc	$⊢ (((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to D \in A$
60		simp23r	$⊢ (((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to \neg T \underset{˙}{\leq} W$
61	1 2 3 4 5 10	cdlemeda	$⊢ ((K \in HL \land W \in H) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (R \in A \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to Y \in A$
62	13 19 52 60 15 44 42 61	syl223anc	$⊢ (((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to Y \in A$
63	16 2 4	hlatjcl	$⊢ (K \in HL \land D \in A \land Y \in A) \to D \underset{˙}{\lor} Y \in {Base}_{K}$
64	13 59 62 63	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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to D \underset{˙}{\lor} Y \in {Base}_{K}$
65	16 1 3	latmle2	$⊢ (K \in Lat \land F \underset{˙}{\lor} G \in {Base}_{K} \land D \underset{˙}{\lor} Y \in {Base}_{K}) \to ((F \underset{˙}{\lor} G) \underset{˙}{\land} (D \underset{˙}{\lor} Y)) \underset{˙}{\leq} (D \underset{˙}{\lor} Y)$
66	47 56 64 65	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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to ((F \underset{˙}{\lor} G) \underset{˙}{\land} (D \underset{˙}{\lor} Y)) \underset{˙}{\leq} (D \underset{˙}{\lor} Y)$
67	46 66	eqbrtrrd	$⊢ (((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to V \underset{˙}{\leq} (D \underset{˙}{\lor} Y)$
68	67	adantr	$⊢ ((((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land D = Y) \to V \underset{˙}{\leq} (D \underset{˙}{\lor} Y)$
69	2 4	hlatjidm	$⊢ (K \in HL \land D \in A) \to D \underset{˙}{\lor} D = D$
70	13 59 69	syl2anc	$⊢ (((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to D \underset{˙}{\lor} D = D$
71		oveq2	$⊢ D = Y \to D \underset{˙}{\lor} D = D \underset{˙}{\lor} Y$
72	70 71	sylan9req	$⊢ ((((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land D = Y) \to D = D \underset{˙}{\lor} Y$
73	68 72	breqtrrd	$⊢ ((((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land D = Y) \to V \underset{˙}{\leq} D$
74		hlatl	$⊢ K \in HL \to K \in AtLat$
75	13 74	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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to K \in AtLat$
76		simp31r	$⊢ (((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to S \neq T$
77	1 2 3 4 5 11	lhpat2	$⊢ ((K \in HL \land W \in H) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land S \neq T)) \to V \in A$
78	13 19 14 57 52 76 77	syl222anc	$⊢ (((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to V \in A$
79	1 4	atcmp	$⊢ (K \in AtLat \land V \in A \land D \in A) \to (V \underset{˙}{\leq} D \leftrightarrow V = D)$
80	75 78 59 79	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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to (V \underset{˙}{\leq} D \leftrightarrow V = D)$
81	80	adantr	$⊢ ((((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land D = Y) \to (V \underset{˙}{\leq} D \leftrightarrow V = D)$
82	73 81	mpbid	$⊢ ((((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land D = Y) \to V = D$
83	82 11	eqtr3di	$⊢ ((((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land D = Y) \to D = (S \underset{˙}{\lor} T) \underset{˙}{\land} W$
84	9 83	eqtr3id	$⊢ ((((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land D = Y) \to (R \underset{˙}{\lor} S) \underset{˙}{\land} W = (S \underset{˙}{\lor} T) \underset{˙}{\land} W$
85	16 2 4	hlatjcl	$⊢ (K \in HL \land S \in A \land T \in A) \to S \underset{˙}{\lor} T \in {Base}_{K}$
86	13 14 52 85	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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to S \underset{˙}{\lor} T \in {Base}_{K}$
87	16 1 3	latmle1	$⊢ (K \in Lat \land S \underset{˙}{\lor} T \in {Base}_{K} \land W \in {Base}_{K}) \to ((S \underset{˙}{\lor} T) \underset{˙}{\land} W) \underset{˙}{\leq} (S \underset{˙}{\lor} T)$
88	47 86 21 87	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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to ((S \underset{˙}{\lor} T) \underset{˙}{\land} W) \underset{˙}{\leq} (S \underset{˙}{\lor} T)$
89	88	adantr	$⊢ ((((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land D = Y) \to ((S \underset{˙}{\lor} T) \underset{˙}{\land} W) \underset{˙}{\leq} (S \underset{˙}{\lor} T)$
90	84 89	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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land D = Y) \to ((R \underset{˙}{\lor} S) \underset{˙}{\land} W) \underset{˙}{\leq} (S \underset{˙}{\lor} T)$
91	1 2 4	hlatlej1	$⊢ (K \in HL \land S \in A \land T \in A) \to S \underset{˙}{\leq} (S \underset{˙}{\lor} T)$
92	13 14 52 91	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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to S \underset{˙}{\leq} (S \underset{˙}{\lor} T)$
93	92	adantr	$⊢ ((((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land D = Y) \to S \underset{˙}{\leq} (S \underset{˙}{\lor} T)$
94	16 3	latmcl	$⊢ (K \in Lat \land R \underset{˙}{\lor} S \in {Base}_{K} \land W \in {Base}_{K}) \to (R \underset{˙}{\lor} S) \underset{˙}{\land} W \in {Base}_{K}$
95	47 18 21 94	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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to (R \underset{˙}{\lor} S) \underset{˙}{\land} W \in {Base}_{K}$
96	16 4	atbase	$⊢ S \in A \to S \in {Base}_{K}$
97	14 96	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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to S \in {Base}_{K}$
98	16 1 2	latjle12	$⊢ (K \in Lat \land ((R \underset{˙}{\lor} S) \underset{˙}{\land} W \in {Base}_{K} \land S \in {Base}_{K} \land S \underset{˙}{\lor} T \in {Base}_{K})) \to ((((R \underset{˙}{\lor} S) \underset{˙}{\land} W) \underset{˙}{\leq} (S \underset{˙}{\lor} T) \land S \underset{˙}{\leq} (S \underset{˙}{\lor} T)) \leftrightarrow (((R \underset{˙}{\lor} S) \underset{˙}{\land} W) \underset{˙}{\lor} S) \underset{˙}{\leq} (S \underset{˙}{\lor} T))$
99	47 95 97 86 98	syl13anc	$⊢ (((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to ((((R \underset{˙}{\lor} S) \underset{˙}{\land} W) \underset{˙}{\leq} (S \underset{˙}{\lor} T) \land S \underset{˙}{\leq} (S \underset{˙}{\lor} T)) \leftrightarrow (((R \underset{˙}{\lor} S) \underset{˙}{\land} W) \underset{˙}{\lor} S) \underset{˙}{\leq} (S \underset{˙}{\lor} T))$
100	99	adantr	$⊢ ((((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land D = Y) \to ((((R \underset{˙}{\lor} S) \underset{˙}{\land} W) \underset{˙}{\leq} (S \underset{˙}{\lor} T) \land S \underset{˙}{\leq} (S \underset{˙}{\lor} T)) \leftrightarrow (((R \underset{˙}{\lor} S) \underset{˙}{\land} W) \underset{˙}{\lor} S) \underset{˙}{\leq} (S \underset{˙}{\lor} T))$
101	90 93 100	mpbi2and	$⊢ ((((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land D = Y) \to (((R \underset{˙}{\lor} S) \underset{˙}{\land} W) \underset{˙}{\lor} S) \underset{˙}{\leq} (S \underset{˙}{\lor} T)$
102	36 101	eqbrtrrd	$⊢ ((((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land D = Y) \to (R \underset{˙}{\lor} S) \underset{˙}{\leq} (S \underset{˙}{\lor} T)$
103	16 4	atbase	$⊢ R \in A \to R \in {Base}_{K}$
104	15 103	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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to R \in {Base}_{K}$
105	16 1 2	latjle12	$⊢ (K \in Lat \land (R \in {Base}_{K} \land S \in {Base}_{K} \land S \underset{˙}{\lor} T \in {Base}_{K})) \to ((R \underset{˙}{\leq} (S \underset{˙}{\lor} T) \land S \underset{˙}{\leq} (S \underset{˙}{\lor} T)) \leftrightarrow (R \underset{˙}{\lor} S) \underset{˙}{\leq} (S \underset{˙}{\lor} T))$
106	47 104 97 86 105	syl13anc	$⊢ (((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to ((R \underset{˙}{\leq} (S \underset{˙}{\lor} T) \land S \underset{˙}{\leq} (S \underset{˙}{\lor} T)) \leftrightarrow (R \underset{˙}{\lor} S) \underset{˙}{\leq} (S \underset{˙}{\lor} T))$
107	106	adantr	$⊢ ((((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land D = Y) \to ((R \underset{˙}{\leq} (S \underset{˙}{\lor} T) \land S \underset{˙}{\leq} (S \underset{˙}{\lor} T)) \leftrightarrow (R \underset{˙}{\lor} S) \underset{˙}{\leq} (S \underset{˙}{\lor} T))$
108	102 107	mpbird	$⊢ ((((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land D = Y) \to (R \underset{˙}{\leq} (S \underset{˙}{\lor} T) \land S \underset{˙}{\leq} (S \underset{˙}{\lor} T))$
109	108	simpld	$⊢ ((((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land D = Y) \to R \underset{˙}{\leq} (S \underset{˙}{\lor} T)$
110	109	ex	$⊢ (((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to (D = Y \to R \underset{˙}{\leq} (S \underset{˙}{\lor} T))$
111	110	necon3bd	$⊢ (((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to (\neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T) \to D \neq Y)$
112	12 111	mpd	$⊢ (((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to D \neq Y$

Metamath Proof Explorer

Theorem cdleme20j

Proof