cdlemblem

	Ref	Expression
Hypotheses	cdlemb.b	$⊢ B = {Base}_{K}$
	cdlemb.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlemb.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdlemb.u	$⊢ \underset{˙}{1} = 1. (K)$
	cdlemb.c	$⊢ C = ⋖_{K}$
	cdlemb.a	$⊢ A = Atoms (K)$
	cdlemblem.s	$⊢ \underset{˙}{<} = <_{K}$
	cdlemblem.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdlemblem.v	$⊢ V = (P \underset{˙}{\lor} Q) \underset{˙}{\land} X$
Assertion	cdlemblem	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq V \land u \underset{˙}{<} X)) \land (r \in A \land (r \neq P \land r \neq u \land r \underset{˙}{\leq} (P \underset{˙}{\lor} u)))) \to (\neg r \underset{˙}{\leq} X \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$

Proof

Step	Hyp	Ref	Expression
1		cdlemb.b	$⊢ B = {Base}_{K}$
2		cdlemb.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cdlemb.j	$⊢ \underset{˙}{\lor} = join (K)$
4		cdlemb.u	$⊢ \underset{˙}{1} = 1. (K)$
5		cdlemb.c	$⊢ C = ⋖_{K}$
6		cdlemb.a	$⊢ A = Atoms (K)$
7		cdlemblem.s	$⊢ \underset{˙}{<} = <_{K}$
8		cdlemblem.m	$⊢ \underset{˙}{\land} = meet (K)$
9		cdlemblem.v	$⊢ V = (P \underset{˙}{\lor} Q) \underset{˙}{\land} X$
10		simp132	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq V \land u \underset{˙}{<} X)) \land (r \in A \land (r \neq P \land r \neq u \land r \underset{˙}{\leq} (P \underset{˙}{\lor} u)))) \to \neg P \underset{˙}{\leq} X$
11		simp111	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq V \land u \underset{˙}{<} X)) \land (r \in A \land (r \neq P \land r \neq u \land r \underset{˙}{\leq} (P \underset{˙}{\lor} u)))) \to K \in HL$
12		simp2l	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq V \land u \underset{˙}{<} X)) \land (r \in A \land (r \neq P \land r \neq u \land r \underset{˙}{\leq} (P \underset{˙}{\lor} u)))) \to u \in A$
13		simp12l	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq V \land u \underset{˙}{<} X)) \land (r \in A \land (r \neq P \land r \neq u \land r \underset{˙}{\leq} (P \underset{˙}{\lor} u)))) \to X \in B$
14	11 12 13	3jca	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq V \land u \underset{˙}{<} X)) \land (r \in A \land (r \neq P \land r \neq u \land r \underset{˙}{\leq} (P \underset{˙}{\lor} u)))) \to (K \in HL \land u \in A \land X \in B)$
15		simp2rr	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq V \land u \underset{˙}{<} X)) \land (r \in A \land (r \neq P \land r \neq u \land r \underset{˙}{\leq} (P \underset{˙}{\lor} u)))) \to u \underset{˙}{<} X$
16	2 7	pltle	$⊢ (K \in HL \land u \in A \land X \in B) \to (u \underset{˙}{<} X \to u \underset{˙}{\leq} X)$
17	14 15 16	sylc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq V \land u \underset{˙}{<} X)) \land (r \in A \land (r \neq P \land r \neq u \land r \underset{˙}{\leq} (P \underset{˙}{\lor} u)))) \to u \underset{˙}{\leq} X$
18	11	hllatd	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq V \land u \underset{˙}{<} X)) \land (r \in A \land (r \neq P \land r \neq u \land r \underset{˙}{\leq} (P \underset{˙}{\lor} u)))) \to K \in Lat$
19		simp3l	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq V \land u \underset{˙}{<} X)) \land (r \in A \land (r \neq P \land r \neq u \land r \underset{˙}{\leq} (P \underset{˙}{\lor} u)))) \to r \in A$
20	1 6	atbase	$⊢ r \in A \to r \in B$
21	19 20	syl	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq V \land u \underset{˙}{<} X)) \land (r \in A \land (r \neq P \land r \neq u \land r \underset{˙}{\leq} (P \underset{˙}{\lor} u)))) \to r \in B$
22	1 6	atbase	$⊢ u \in A \to u \in B$
23	12 22	syl	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq V \land u \underset{˙}{<} X)) \land (r \in A \land (r \neq P \land r \neq u \land r \underset{˙}{\leq} (P \underset{˙}{\lor} u)))) \to u \in B$
24	1 2 3	latjle12	$⊢ (K \in Lat \land (r \in B \land u \in B \land X \in B)) \to ((r \underset{˙}{\leq} X \land u \underset{˙}{\leq} X) \leftrightarrow (r \underset{˙}{\lor} u) \underset{˙}{\leq} X)$
25	18 21 23 13 24	syl13anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq V \land u \underset{˙}{<} X)) \land (r \in A \land (r \neq P \land r \neq u \land r \underset{˙}{\leq} (P \underset{˙}{\lor} u)))) \to ((r \underset{˙}{\leq} X \land u \underset{˙}{\leq} X) \leftrightarrow (r \underset{˙}{\lor} u) \underset{˙}{\leq} X)$
26	25	biimpd	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq V \land u \underset{˙}{<} X)) \land (r \in A \land (r \neq P \land r \neq u \land r \underset{˙}{\leq} (P \underset{˙}{\lor} u)))) \to ((r \underset{˙}{\leq} X \land u \underset{˙}{\leq} X) \to (r \underset{˙}{\lor} u) \underset{˙}{\leq} X)$
27	17 26	mpan2d	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq V \land u \underset{˙}{<} X)) \land (r \in A \land (r \neq P \land r \neq u \land r \underset{˙}{\leq} (P \underset{˙}{\lor} u)))) \to (r \underset{˙}{\leq} X \to (r \underset{˙}{\lor} u) \underset{˙}{\leq} X)$
28		simp112	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq V \land u \underset{˙}{<} X)) \land (r \in A \land (r \neq P \land r \neq u \land r \underset{˙}{\leq} (P \underset{˙}{\lor} u)))) \to P \in A$
29	19 28 12	3jca	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq V \land u \underset{˙}{<} X)) \land (r \in A \land (r \neq P \land r \neq u \land r \underset{˙}{\leq} (P \underset{˙}{\lor} u)))) \to (r \in A \land P \in A \land u \in A)$
30		simp3r2	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq V \land u \underset{˙}{<} X)) \land (r \in A \land (r \neq P \land r \neq u \land r \underset{˙}{\leq} (P \underset{˙}{\lor} u)))) \to r \neq u$
31	11 29 30	3jca	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq V \land u \underset{˙}{<} X)) \land (r \in A \land (r \neq P \land r \neq u \land r \underset{˙}{\leq} (P \underset{˙}{\lor} u)))) \to (K \in HL \land (r \in A \land P \in A \land u \in A) \land r \neq u)$
32		simp3r3	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq V \land u \underset{˙}{<} X)) \land (r \in A \land (r \neq P \land r \neq u \land r \underset{˙}{\leq} (P \underset{˙}{\lor} u)))) \to r \underset{˙}{\leq} (P \underset{˙}{\lor} u)$
33	2 3 6	hlatexch2	$⊢ (K \in HL \land (r \in A \land P \in A \land u \in A) \land r \neq u) \to (r \underset{˙}{\leq} (P \underset{˙}{\lor} u) \to P \underset{˙}{\leq} (r \underset{˙}{\lor} u))$
34	31 32 33	sylc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq V \land u \underset{˙}{<} X)) \land (r \in A \land (r \neq P \land r \neq u \land r \underset{˙}{\leq} (P \underset{˙}{\lor} u)))) \to P \underset{˙}{\leq} (r \underset{˙}{\lor} u)$
35	1 6	atbase	$⊢ P \in A \to P \in B$
36	28 35	syl	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq V \land u \underset{˙}{<} X)) \land (r \in A \land (r \neq P \land r \neq u \land r \underset{˙}{\leq} (P \underset{˙}{\lor} u)))) \to P \in B$
37	1 3	latjcl	$⊢ (K \in Lat \land r \in B \land u \in B) \to r \underset{˙}{\lor} u \in B$
38	18 21 23 37	syl3anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq V \land u \underset{˙}{<} X)) \land (r \in A \land (r \neq P \land r \neq u \land r \underset{˙}{\leq} (P \underset{˙}{\lor} u)))) \to r \underset{˙}{\lor} u \in B$
39	1 2	lattr	$⊢ (K \in Lat \land (P \in B \land r \underset{˙}{\lor} u \in B \land X \in B)) \to ((P \underset{˙}{\leq} (r \underset{˙}{\lor} u) \land (r \underset{˙}{\lor} u) \underset{˙}{\leq} X) \to P \underset{˙}{\leq} X)$
40	18 36 38 13 39	syl13anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq V \land u \underset{˙}{<} X)) \land (r \in A \land (r \neq P \land r \neq u \land r \underset{˙}{\leq} (P \underset{˙}{\lor} u)))) \to ((P \underset{˙}{\leq} (r \underset{˙}{\lor} u) \land (r \underset{˙}{\lor} u) \underset{˙}{\leq} X) \to P \underset{˙}{\leq} X)$
41	34 40	mpand	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq V \land u \underset{˙}{<} X)) \land (r \in A \land (r \neq P \land r \neq u \land r \underset{˙}{\leq} (P \underset{˙}{\lor} u)))) \to ((r \underset{˙}{\lor} u) \underset{˙}{\leq} X \to P \underset{˙}{\leq} X)$
42	27 41	syld	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq V \land u \underset{˙}{<} X)) \land (r \in A \land (r \neq P \land r \neq u \land r \underset{˙}{\leq} (P \underset{˙}{\lor} u)))) \to (r \underset{˙}{\leq} X \to P \underset{˙}{\leq} X)$
43	10 42	mtod	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq V \land u \underset{˙}{<} X)) \land (r \in A \land (r \neq P \land r \neq u \land r \underset{˙}{\leq} (P \underset{˙}{\lor} u)))) \to \neg r \underset{˙}{\leq} X$
44		simp2rl	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq V \land u \underset{˙}{<} X)) \land (r \in A \land (r \neq P \land r \neq u \land r \underset{˙}{\leq} (P \underset{˙}{\lor} u)))) \to u \neq V$
45		simp113	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq V \land u \underset{˙}{<} X)) \land (r \in A \land (r \neq P \land r \neq u \land r \underset{˙}{\leq} (P \underset{˙}{\lor} u)))) \to Q \in A$
46		simp3r1	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq V \land u \underset{˙}{<} X)) \land (r \in A \land (r \neq P \land r \neq u \land r \underset{˙}{\leq} (P \underset{˙}{\lor} u)))) \to r \neq P$
47	2 3 6	hlatexchb1	$⊢ (K \in HL \land (r \in A \land Q \in A \land P \in A) \land r \neq P) \to (r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \leftrightarrow P \underset{˙}{\lor} r = P \underset{˙}{\lor} Q)$
48	11 19 45 28 46 47	syl131anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq V \land u \underset{˙}{<} X)) \land (r \in A \land (r \neq P \land r \neq u \land r \underset{˙}{\leq} (P \underset{˙}{\lor} u)))) \to (r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \leftrightarrow P \underset{˙}{\lor} r = P \underset{˙}{\lor} Q)$
49	19 12 28	3jca	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq V \land u \underset{˙}{<} X)) \land (r \in A \land (r \neq P \land r \neq u \land r \underset{˙}{\leq} (P \underset{˙}{\lor} u)))) \to (r \in A \land u \in A \land P \in A)$
50	11 49 46	3jca	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq V \land u \underset{˙}{<} X)) \land (r \in A \land (r \neq P \land r \neq u \land r \underset{˙}{\leq} (P \underset{˙}{\lor} u)))) \to (K \in HL \land (r \in A \land u \in A \land P \in A) \land r \neq P)$
51	2 3 6	hlatexch1	$⊢ (K \in HL \land (r \in A \land u \in A \land P \in A) \land r \neq P) \to (r \underset{˙}{\leq} (P \underset{˙}{\lor} u) \to u \underset{˙}{\leq} (P \underset{˙}{\lor} r))$
52	50 32 51	sylc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq V \land u \underset{˙}{<} X)) \land (r \in A \land (r \neq P \land r \neq u \land r \underset{˙}{\leq} (P \underset{˙}{\lor} u)))) \to u \underset{˙}{\leq} (P \underset{˙}{\lor} r)$
53		breq2	$⊢ P \underset{˙}{\lor} r = P \underset{˙}{\lor} Q \to (u \underset{˙}{\leq} (P \underset{˙}{\lor} r) \leftrightarrow u \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
54	52 53	syl5ibcom	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq V \land u \underset{˙}{<} X)) \land (r \in A \land (r \neq P \land r \neq u \land r \underset{˙}{\leq} (P \underset{˙}{\lor} u)))) \to (P \underset{˙}{\lor} r = P \underset{˙}{\lor} Q \to u \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
55	48 54	sylbid	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq V \land u \underset{˙}{<} X)) \land (r \in A \land (r \neq P \land r \neq u \land r \underset{˙}{\leq} (P \underset{˙}{\lor} u)))) \to (r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \to u \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
56	55 17	jctird	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq V \land u \underset{˙}{<} X)) \land (r \in A \land (r \neq P \land r \neq u \land r \underset{˙}{\leq} (P \underset{˙}{\lor} u)))) \to (r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \to (u \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land u \underset{˙}{\leq} X))$
57	1 6	atbase	$⊢ Q \in A \to Q \in B$
58	45 57	syl	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq V \land u \underset{˙}{<} X)) \land (r \in A \land (r \neq P \land r \neq u \land r \underset{˙}{\leq} (P \underset{˙}{\lor} u)))) \to Q \in B$
59	1 3	latjcl	$⊢ (K \in Lat \land P \in B \land Q \in B) \to P \underset{˙}{\lor} Q \in B$
60	18 36 58 59	syl3anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq V \land u \underset{˙}{<} X)) \land (r \in A \land (r \neq P \land r \neq u \land r \underset{˙}{\leq} (P \underset{˙}{\lor} u)))) \to P \underset{˙}{\lor} Q \in B$
61	1 2 8	latlem12	$⊢ (K \in Lat \land (u \in B \land P \underset{˙}{\lor} Q \in B \land X \in B)) \to ((u \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land u \underset{˙}{\leq} X) \leftrightarrow u \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} X))$
62	18 23 60 13 61	syl13anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq V \land u \underset{˙}{<} X)) \land (r \in A \land (r \neq P \land r \neq u \land r \underset{˙}{\leq} (P \underset{˙}{\lor} u)))) \to ((u \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land u \underset{˙}{\leq} X) \leftrightarrow u \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} X))$
63	9	breq2i	$⊢ u \underset{˙}{\leq} V \leftrightarrow u \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} X)$
64	62 63	bitr4di	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq V \land u \underset{˙}{<} X)) \land (r \in A \land (r \neq P \land r \neq u \land r \underset{˙}{\leq} (P \underset{˙}{\lor} u)))) \to ((u \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land u \underset{˙}{\leq} X) \leftrightarrow u \underset{˙}{\leq} V)$
65	56 64	sylibd	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq V \land u \underset{˙}{<} X)) \land (r \in A \land (r \neq P \land r \neq u \land r \underset{˙}{\leq} (P \underset{˙}{\lor} u)))) \to (r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \to u \underset{˙}{\leq} V)$
66		hlatl	$⊢ K \in HL \to K \in AtLat$
67	11 66	syl	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq V \land u \underset{˙}{<} X)) \land (r \in A \land (r \neq P \land r \neq u \land r \underset{˙}{\leq} (P \underset{˙}{\lor} u)))) \to K \in AtLat$
68		simp12r	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq V \land u \underset{˙}{<} X)) \land (r \in A \land (r \neq P \land r \neq u \land r \underset{˙}{\leq} (P \underset{˙}{\lor} u)))) \to P \neq Q$
69		simp131	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq V \land u \underset{˙}{<} X)) \land (r \in A \land (r \neq P \land r \neq u \land r \underset{˙}{\leq} (P \underset{˙}{\lor} u)))) \to X C \underset{˙}{1}$
70	1 2 3 8 4 5 6	1cvrat	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \neq Q \land X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} X \in A$
71	11 28 45 13 68 69 10 70	syl133anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq V \land u \underset{˙}{<} X)) \land (r \in A \land (r \neq P \land r \neq u \land r \underset{˙}{\leq} (P \underset{˙}{\lor} u)))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} X \in A$
72	9 71	eqeltrid	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq V \land u \underset{˙}{<} X)) \land (r \in A \land (r \neq P \land r \neq u \land r \underset{˙}{\leq} (P \underset{˙}{\lor} u)))) \to V \in A$
73	2 6	atcmp	$⊢ (K \in AtLat \land u \in A \land V \in A) \to (u \underset{˙}{\leq} V \leftrightarrow u = V)$
74	67 12 72 73	syl3anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq V \land u \underset{˙}{<} X)) \land (r \in A \land (r \neq P \land r \neq u \land r \underset{˙}{\leq} (P \underset{˙}{\lor} u)))) \to (u \underset{˙}{\leq} V \leftrightarrow u = V)$
75	65 74	sylibd	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq V \land u \underset{˙}{<} X)) \land (r \in A \land (r \neq P \land r \neq u \land r \underset{˙}{\leq} (P \underset{˙}{\lor} u)))) \to (r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \to u = V)$
76	75	necon3ad	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq V \land u \underset{˙}{<} X)) \land (r \in A \land (r \neq P \land r \neq u \land r \underset{˙}{\leq} (P \underset{˙}{\lor} u)))) \to (u \neq V \to \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
77	44 76	mpd	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq V \land u \underset{˙}{<} X)) \land (r \in A \land (r \neq P \land r \neq u \land r \underset{˙}{\leq} (P \underset{˙}{\lor} u)))) \to \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
78	43 77	jca	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq V \land u \underset{˙}{<} X)) \land (r \in A \land (r \neq P \land r \neq u \land r \underset{˙}{\leq} (P \underset{˙}{\lor} u)))) \to (\neg r \underset{˙}{\leq} X \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$

Metamath Proof Explorer

Theorem cdlemblem

Proof