cdlema1N

Description: A condition for required for proof of Lemma A in Crawley p. 112. (Contributed by NM, 29-Apr-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cdlema1.b	$⊢ B = {Base}_{K}$
	cdlema1.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlema1.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdlema1.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdlema1.a	$⊢ A = Atoms (K)$
	cdlema1.n	$⊢ N = Lines (K)$
	cdlema1.f	$⊢ F = pmap (K)$
Assertion	cdlema1N	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{\leq} Y) \land (F (Y) \in N \land X \underset{˙}{\land} Y \in A \land \neg Q \underset{˙}{\leq} X))) \to X \underset{˙}{\lor} R = X \underset{˙}{\lor} Y$

Proof

Step	Hyp	Ref	Expression
1		cdlema1.b	$⊢ B = {Base}_{K}$
2		cdlema1.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cdlema1.j	$⊢ \underset{˙}{\lor} = join (K)$
4		cdlema1.m	$⊢ \underset{˙}{\land} = meet (K)$
5		cdlema1.a	$⊢ A = Atoms (K)$
6		cdlema1.n	$⊢ N = Lines (K)$
7		cdlema1.f	$⊢ F = pmap (K)$
8		simp11	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{\leq} Y) \land (F (Y) \in N \land X \underset{˙}{\land} Y \in A \land \neg Q \underset{˙}{\leq} X))) \to K \in HL$
9	8	hllatd	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{\leq} Y) \land (F (Y) \in N \land X \underset{˙}{\land} Y \in A \land \neg Q \underset{˙}{\leq} X))) \to K \in Lat$
10		simp12	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{\leq} Y) \land (F (Y) \in N \land X \underset{˙}{\land} Y \in A \land \neg Q \underset{˙}{\leq} X))) \to X \in B$
11		simp23	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{\leq} Y) \land (F (Y) \in N \land X \underset{˙}{\land} Y \in A \land \neg Q \underset{˙}{\leq} X))) \to R \in A$
12	1 5	atbase	$⊢ R \in A \to R \in B$
13	11 12	syl	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{\leq} Y) \land (F (Y) \in N \land X \underset{˙}{\land} Y \in A \land \neg Q \underset{˙}{\leq} X))) \to R \in B$
14	1 3	latjcl	$⊢ (K \in Lat \land X \in B \land R \in B) \to X \underset{˙}{\lor} R \in B$
15	9 10 13 14	syl3anc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{\leq} Y) \land (F (Y) \in N \land X \underset{˙}{\land} Y \in A \land \neg Q \underset{˙}{\leq} X))) \to X \underset{˙}{\lor} R \in B$
16		simp13	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{\leq} Y) \land (F (Y) \in N \land X \underset{˙}{\land} Y \in A \land \neg Q \underset{˙}{\leq} X))) \to Y \in B$
17	1 3	latjcl	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \underset{˙}{\lor} Y \in B$
18	9 10 16 17	syl3anc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{\leq} Y) \land (F (Y) \in N \land X \underset{˙}{\land} Y \in A \land \neg Q \underset{˙}{\leq} X))) \to X \underset{˙}{\lor} Y \in B$
19	1 2 3	latlej1	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \underset{˙}{\leq} (X \underset{˙}{\lor} Y)$
20	9 10 16 19	syl3anc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{\leq} Y) \land (F (Y) \in N \land X \underset{˙}{\land} Y \in A \land \neg Q \underset{˙}{\leq} X))) \to X \underset{˙}{\leq} (X \underset{˙}{\lor} Y)$
21		simp21	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{\leq} Y) \land (F (Y) \in N \land X \underset{˙}{\land} Y \in A \land \neg Q \underset{˙}{\leq} X))) \to P \in A$
22	1 5	atbase	$⊢ P \in A \to P \in B$
23	21 22	syl	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{\leq} Y) \land (F (Y) \in N \land X \underset{˙}{\land} Y \in A \land \neg Q \underset{˙}{\leq} X))) \to P \in B$
24		simp22	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{\leq} Y) \land (F (Y) \in N \land X \underset{˙}{\land} Y \in A \land \neg Q \underset{˙}{\leq} X))) \to Q \in A$
25	1 5	atbase	$⊢ Q \in A \to Q \in B$
26	24 25	syl	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{\leq} Y) \land (F (Y) \in N \land X \underset{˙}{\land} Y \in A \land \neg Q \underset{˙}{\leq} X))) \to Q \in B$
27	1 3	latjcl	$⊢ (K \in Lat \land P \in B \land Q \in B) \to P \underset{˙}{\lor} Q \in B$
28	9 23 26 27	syl3anc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{\leq} Y) \land (F (Y) \in N \land X \underset{˙}{\land} Y \in A \land \neg Q \underset{˙}{\leq} X))) \to P \underset{˙}{\lor} Q \in B$
29		simp31r	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{\leq} Y) \land (F (Y) \in N \land X \underset{˙}{\land} Y \in A \land \neg Q \underset{˙}{\leq} X))) \to R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
30		simp32l	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{\leq} Y) \land (F (Y) \in N \land X \underset{˙}{\land} Y \in A \land \neg Q \underset{˙}{\leq} X))) \to P \underset{˙}{\leq} X$
31		simp32r	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{\leq} Y) \land (F (Y) \in N \land X \underset{˙}{\land} Y \in A \land \neg Q \underset{˙}{\leq} X))) \to Q \underset{˙}{\leq} Y$
32	1 2 3	latjlej12	$⊢ (K \in Lat \land (P \in B \land X \in B) \land (Q \in B \land Y \in B)) \to ((P \underset{˙}{\leq} X \land Q \underset{˙}{\leq} Y) \to (P \underset{˙}{\lor} Q) \underset{˙}{\leq} (X \underset{˙}{\lor} Y))$
33	9 23 10 26 16 32	syl122anc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{\leq} Y) \land (F (Y) \in N \land X \underset{˙}{\land} Y \in A \land \neg Q \underset{˙}{\leq} X))) \to ((P \underset{˙}{\leq} X \land Q \underset{˙}{\leq} Y) \to (P \underset{˙}{\lor} Q) \underset{˙}{\leq} (X \underset{˙}{\lor} Y))$
34	30 31 33	mp2and	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{\leq} Y) \land (F (Y) \in N \land X \underset{˙}{\land} Y \in A \land \neg Q \underset{˙}{\leq} X))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\leq} (X \underset{˙}{\lor} Y)$
35	1 2 9 13 28 18 29 34	lattrd	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{\leq} Y) \land (F (Y) \in N \land X \underset{˙}{\land} Y \in A \land \neg Q \underset{˙}{\leq} X))) \to R \underset{˙}{\leq} (X \underset{˙}{\lor} Y)$
36	1 2 3	latjle12	$⊢ (K \in Lat \land (X \in B \land R \in B \land X \underset{˙}{\lor} Y \in B)) \to ((X \underset{˙}{\leq} (X \underset{˙}{\lor} Y) \land R \underset{˙}{\leq} (X \underset{˙}{\lor} Y)) \leftrightarrow (X \underset{˙}{\lor} R) \underset{˙}{\leq} (X \underset{˙}{\lor} Y))$
37	9 10 13 18 36	syl13anc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{\leq} Y) \land (F (Y) \in N \land X \underset{˙}{\land} Y \in A \land \neg Q \underset{˙}{\leq} X))) \to ((X \underset{˙}{\leq} (X \underset{˙}{\lor} Y) \land R \underset{˙}{\leq} (X \underset{˙}{\lor} Y)) \leftrightarrow (X \underset{˙}{\lor} R) \underset{˙}{\leq} (X \underset{˙}{\lor} Y))$
38	20 35 37	mpbi2and	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{\leq} Y) \land (F (Y) \in N \land X \underset{˙}{\land} Y \in A \land \neg Q \underset{˙}{\leq} X))) \to (X \underset{˙}{\lor} R) \underset{˙}{\leq} (X \underset{˙}{\lor} Y)$
39	1 2 3	latlej1	$⊢ (K \in Lat \land X \in B \land R \in B) \to X \underset{˙}{\leq} (X \underset{˙}{\lor} R)$
40	9 10 13 39	syl3anc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{\leq} Y) \land (F (Y) \in N \land X \underset{˙}{\land} Y \in A \land \neg Q \underset{˙}{\leq} X))) \to X \underset{˙}{\leq} (X \underset{˙}{\lor} R)$
41		simp331	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{\leq} Y) \land (F (Y) \in N \land X \underset{˙}{\land} Y \in A \land \neg Q \underset{˙}{\leq} X))) \to F (Y) \in N$
42		simp332	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{\leq} Y) \land (F (Y) \in N \land X \underset{˙}{\land} Y \in A \land \neg Q \underset{˙}{\leq} X))) \to X \underset{˙}{\land} Y \in A$
43		simp333	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{\leq} Y) \land (F (Y) \in N \land X \underset{˙}{\land} Y \in A \land \neg Q \underset{˙}{\leq} X))) \to \neg Q \underset{˙}{\leq} X$
44	1 2 4	latmle1	$⊢ (K \in Lat \land X \in B \land Y \in B) \to (X \underset{˙}{\land} Y) \underset{˙}{\leq} X$
45	9 10 16 44	syl3anc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{\leq} Y) \land (F (Y) \in N \land X \underset{˙}{\land} Y \in A \land \neg Q \underset{˙}{\leq} X))) \to (X \underset{˙}{\land} Y) \underset{˙}{\leq} X$
46		breq1	$⊢ Q = X \underset{˙}{\land} Y \to (Q \underset{˙}{\leq} X \leftrightarrow (X \underset{˙}{\land} Y) \underset{˙}{\leq} X)$
47	45 46	syl5ibrcom	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{\leq} Y) \land (F (Y) \in N \land X \underset{˙}{\land} Y \in A \land \neg Q \underset{˙}{\leq} X))) \to (Q = X \underset{˙}{\land} Y \to Q \underset{˙}{\leq} X)$
48	47	necon3bd	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{\leq} Y) \land (F (Y) \in N \land X \underset{˙}{\land} Y \in A \land \neg Q \underset{˙}{\leq} X))) \to (\neg Q \underset{˙}{\leq} X \to Q \neq X \underset{˙}{\land} Y)$
49	43 48	mpd	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{\leq} Y) \land (F (Y) \in N \land X \underset{˙}{\land} Y \in A \land \neg Q \underset{˙}{\leq} X))) \to Q \neq X \underset{˙}{\land} Y$
50	1 2 4	latmle2	$⊢ (K \in Lat \land X \in B \land Y \in B) \to (X \underset{˙}{\land} Y) \underset{˙}{\leq} Y$
51	9 10 16 50	syl3anc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{\leq} Y) \land (F (Y) \in N \land X \underset{˙}{\land} Y \in A \land \neg Q \underset{˙}{\leq} X))) \to (X \underset{˙}{\land} Y) \underset{˙}{\leq} Y$
52	1 2 3 5 6 7	lneq2at	$⊢ ((K \in HL \land Y \in B \land F (Y) \in N) \land (Q \in A \land X \underset{˙}{\land} Y \in A \land Q \neq X \underset{˙}{\land} Y) \land (Q \underset{˙}{\leq} Y \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} Y)) \to Y = Q \underset{˙}{\lor} (X \underset{˙}{\land} Y)$
53	8 16 41 24 42 49 31 51 52	syl332anc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{\leq} Y) \land (F (Y) \in N \land X \underset{˙}{\land} Y \in A \land \neg Q \underset{˙}{\leq} X))) \to Y = Q \underset{˙}{\lor} (X \underset{˙}{\land} Y)$
54	1 3	latjcl	$⊢ (K \in Lat \land P \in B \land R \in B) \to P \underset{˙}{\lor} R \in B$
55	9 23 13 54	syl3anc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{\leq} Y) \land (F (Y) \in N \land X \underset{˙}{\land} Y \in A \land \neg Q \underset{˙}{\leq} X))) \to P \underset{˙}{\lor} R \in B$
56	11 24 21	3jca	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{\leq} Y) \land (F (Y) \in N \land X \underset{˙}{\land} Y \in A \land \neg Q \underset{˙}{\leq} X))) \to (R \in A \land Q \in A \land P \in A)$
57		simp31l	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{\leq} Y) \land (F (Y) \in N \land X \underset{˙}{\land} Y \in A \land \neg Q \underset{˙}{\leq} X))) \to R \neq P$
58	8 56 57	3jca	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{\leq} Y) \land (F (Y) \in N \land X \underset{˙}{\land} Y \in A \land \neg Q \underset{˙}{\leq} X))) \to (K \in HL \land (R \in A \land Q \in A \land P \in A) \land R \neq P)$
59	2 3 5	hlatexch1	$⊢ (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) \to Q \underset{˙}{\leq} (P \underset{˙}{\lor} R))$
60	58 29 59	sylc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{\leq} Y) \land (F (Y) \in N \land X \underset{˙}{\land} Y \in A \land \neg Q \underset{˙}{\leq} X))) \to Q \underset{˙}{\leq} (P \underset{˙}{\lor} R)$
61	23 10 13	3jca	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{\leq} Y) \land (F (Y) \in N \land X \underset{˙}{\land} Y \in A \land \neg Q \underset{˙}{\leq} X))) \to (P \in B \land X \in B \land R \in B)$
62	9 61	jca	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{\leq} Y) \land (F (Y) \in N \land X \underset{˙}{\land} Y \in A \land \neg Q \underset{˙}{\leq} X))) \to (K \in Lat \land (P \in B \land X \in B \land R \in B))$
63	1 2 3	latjlej1	$⊢ (K \in Lat \land (P \in B \land X \in B \land R \in B)) \to (P \underset{˙}{\leq} X \to (P \underset{˙}{\lor} R) \underset{˙}{\leq} (X \underset{˙}{\lor} R))$
64	62 30 63	sylc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{\leq} Y) \land (F (Y) \in N \land X \underset{˙}{\land} Y \in A \land \neg Q \underset{˙}{\leq} X))) \to (P \underset{˙}{\lor} R) \underset{˙}{\leq} (X \underset{˙}{\lor} R)$
65	1 2 9 26 55 15 60 64	lattrd	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{\leq} Y) \land (F (Y) \in N \land X \underset{˙}{\land} Y \in A \land \neg Q \underset{˙}{\leq} X))) \to Q \underset{˙}{\leq} (X \underset{˙}{\lor} R)$
66	1 2 3 4	latmlej11	$⊢ (K \in Lat \land (X \in B \land Y \in B \land R \in B)) \to (X \underset{˙}{\land} Y) \underset{˙}{\leq} (X \underset{˙}{\lor} R)$
67	9 10 16 13 66	syl13anc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{\leq} Y) \land (F (Y) \in N \land X \underset{˙}{\land} Y \in A \land \neg Q \underset{˙}{\leq} X))) \to (X \underset{˙}{\land} Y) \underset{˙}{\leq} (X \underset{˙}{\lor} R)$
68	1 4	latmcl	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \underset{˙}{\land} Y \in B$
69	9 10 16 68	syl3anc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{\leq} Y) \land (F (Y) \in N \land X \underset{˙}{\land} Y \in A \land \neg Q \underset{˙}{\leq} X))) \to X \underset{˙}{\land} Y \in B$
70	1 2 3	latjle12	$⊢ (K \in Lat \land (Q \in B \land X \underset{˙}{\land} Y \in B \land X \underset{˙}{\lor} R \in B)) \to ((Q \underset{˙}{\leq} (X \underset{˙}{\lor} R) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} (X \underset{˙}{\lor} R)) \leftrightarrow (Q \underset{˙}{\lor} (X \underset{˙}{\land} Y)) \underset{˙}{\leq} (X \underset{˙}{\lor} R))$
71	9 26 69 15 70	syl13anc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{\leq} Y) \land (F (Y) \in N \land X \underset{˙}{\land} Y \in A \land \neg Q \underset{˙}{\leq} X))) \to ((Q \underset{˙}{\leq} (X \underset{˙}{\lor} R) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} (X \underset{˙}{\lor} R)) \leftrightarrow (Q \underset{˙}{\lor} (X \underset{˙}{\land} Y)) \underset{˙}{\leq} (X \underset{˙}{\lor} R))$
72	65 67 71	mpbi2and	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{\leq} Y) \land (F (Y) \in N \land X \underset{˙}{\land} Y \in A \land \neg Q \underset{˙}{\leq} X))) \to (Q \underset{˙}{\lor} (X \underset{˙}{\land} Y)) \underset{˙}{\leq} (X \underset{˙}{\lor} R)$
73	53 72	eqbrtrd	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{\leq} Y) \land (F (Y) \in N \land X \underset{˙}{\land} Y \in A \land \neg Q \underset{˙}{\leq} X))) \to Y \underset{˙}{\leq} (X \underset{˙}{\lor} R)$
74	1 2 3	latjle12	$⊢ (K \in Lat \land (X \in B \land Y \in B \land X \underset{˙}{\lor} R \in B)) \to ((X \underset{˙}{\leq} (X \underset{˙}{\lor} R) \land Y \underset{˙}{\leq} (X \underset{˙}{\lor} R)) \leftrightarrow (X \underset{˙}{\lor} Y) \underset{˙}{\leq} (X \underset{˙}{\lor} R))$
75	9 10 16 15 74	syl13anc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{\leq} Y) \land (F (Y) \in N \land X \underset{˙}{\land} Y \in A \land \neg Q \underset{˙}{\leq} X))) \to ((X \underset{˙}{\leq} (X \underset{˙}{\lor} R) \land Y \underset{˙}{\leq} (X \underset{˙}{\lor} R)) \leftrightarrow (X \underset{˙}{\lor} Y) \underset{˙}{\leq} (X \underset{˙}{\lor} R))$
76	40 73 75	mpbi2and	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{\leq} Y) \land (F (Y) \in N \land X \underset{˙}{\land} Y \in A \land \neg Q \underset{˙}{\leq} X))) \to (X \underset{˙}{\lor} Y) \underset{˙}{\leq} (X \underset{˙}{\lor} R)$
77	1 2 9 15 18 38 76	latasymd	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A \land R \in A) \land ((R \neq P \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (P \underset{˙}{\leq} X \land Q \underset{˙}{\leq} Y) \land (F (Y) \in N \land X \underset{˙}{\land} Y \in A \land \neg Q \underset{˙}{\leq} X))) \to X \underset{˙}{\lor} R = X \underset{˙}{\lor} Y$

Metamath Proof Explorer

Theorem cdlema1N

Proof