cdleme21ct

Description: Part of proof of Lemma E in Crawley p. 115. (Contributed by NM, 29-Nov-2012)

	Ref	Expression
Hypotheses	cdleme21.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdleme21.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdleme21.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdleme21.a	$⊢ A = Atoms (K)$
	cdleme21.h	$⊢ H = LHyp (K)$
	cdleme21.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
Assertion	cdleme21ct	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land ((z \in A \land \neg z \underset{˙}{\leq} W) \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to \neg U \underset{˙}{\leq} (T \underset{˙}{\lor} z)$

Proof

Step	Hyp	Ref	Expression
1		cdleme21.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdleme21.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdleme21.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdleme21.a	$⊢ A = Atoms (K)$
5		cdleme21.h	$⊢ H = LHyp (K)$
6		cdleme21.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
7		simp11	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land ((z \in A \land \neg z \underset{˙}{\leq} W) \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to (K \in HL \land W \in H)$
8		simp12	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land ((z \in A \land \neg z \underset{˙}{\leq} W) \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
9		simp13	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land ((z \in A \land \neg z \underset{˙}{\leq} W) \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to Q \in A$
10		simp21l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land ((z \in A \land \neg z \underset{˙}{\leq} W) \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to S \in A$
11		simp231	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land ((z \in A \land \neg z \underset{˙}{\leq} W) \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to P \neq Q$
12		simp232	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land ((z \in A \land \neg z \underset{˙}{\leq} W) \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
13		simp3ll	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land ((z \in A \land \neg z \underset{˙}{\leq} W) \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to z \in A$
14		simp3r	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land ((z \in A \land \neg z \underset{˙}{\leq} W) \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to P \underset{˙}{\lor} z = S \underset{˙}{\lor} z$
15	1 2 3 4 5 6	cdleme21c	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (S \in A \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} z)$
16	7 8 9 10 11 12 13 14 15	syl332anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land ((z \in A \land \neg z \underset{˙}{\leq} W) \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} z)$
17		simp233	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land ((z \in A \land \neg z \underset{˙}{\leq} W) \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to U \underset{˙}{\leq} (S \underset{˙}{\lor} T)$
18		simp11l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land ((z \in A \land \neg z \underset{˙}{\leq} W) \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to K \in HL$
19		hlcvl	$⊢ K \in HL \to K \in CvLat$
20	18 19	syl	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land ((z \in A \land \neg z \underset{˙}{\leq} W) \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to K \in CvLat$
21		simp11r	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land ((z \in A \land \neg z \underset{˙}{\leq} W) \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to W \in H$
22		simp12l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land ((z \in A \land \neg z \underset{˙}{\leq} W) \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to P \in A$
23		simp12r	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land ((z \in A \land \neg z \underset{˙}{\leq} W) \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to \neg P \underset{˙}{\leq} W$
24	1 2 3 4 5 6	cdleme0a	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land P \neq Q)) \to U \in A$
25	18 21 22 23 9 11 24	syl222anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land ((z \in A \land \neg z \underset{˙}{\leq} W) \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to U \in A$
26		simp22l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land ((z \in A \land \neg z \underset{˙}{\leq} W) \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to T \in A$
27	18	hllatd	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land ((z \in A \land \neg z \underset{˙}{\leq} W) \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to K \in Lat$
28		eqid	$⊢ {Base}_{K} = {Base}_{K}$
29	28 2 4	hlatjcl	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
30	18 22 9 29	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land ((z \in A \land \neg z \underset{˙}{\leq} W) \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
31	28 5	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
32	21 31	syl	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land ((z \in A \land \neg z \underset{˙}{\leq} W) \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to W \in {Base}_{K}$
33	28 1 3	latmle2	$⊢ (K \in Lat \land P \underset{˙}{\lor} Q \in {Base}_{K} \land W \in {Base}_{K}) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\leq} W$
34	27 30 32 33	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land ((z \in A \land \neg z \underset{˙}{\leq} W) \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\leq} W$
35	6 34	eqbrtrid	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land ((z \in A \land \neg z \underset{˙}{\leq} W) \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to U \underset{˙}{\leq} W$
36		simp21r	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land ((z \in A \land \neg z \underset{˙}{\leq} W) \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to \neg S \underset{˙}{\leq} W$
37		nbrne2	$⊢ (U \underset{˙}{\leq} W \land \neg S \underset{˙}{\leq} W) \to U \neq S$
38	35 36 37	syl2anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land ((z \in A \land \neg z \underset{˙}{\leq} W) \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to U \neq S$
39		simp22r	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land ((z \in A \land \neg z \underset{˙}{\leq} W) \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to \neg T \underset{˙}{\leq} W$
40		nbrne2	$⊢ (U \underset{˙}{\leq} W \land \neg T \underset{˙}{\leq} W) \to U \neq T$
41	35 39 40	syl2anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land ((z \in A \land \neg z \underset{˙}{\leq} W) \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to U \neq T$
42	1 2 4	cvlatexch3	$⊢ (K \in CvLat \land (U \in A \land S \in A \land T \in A) \land (U \neq S \land U \neq T)) \to (U \underset{˙}{\leq} (S \underset{˙}{\lor} T) \to U \underset{˙}{\lor} S = U \underset{˙}{\lor} T)$
43	20 25 10 26 38 41 42	syl132anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land ((z \in A \land \neg z \underset{˙}{\leq} W) \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to (U \underset{˙}{\leq} (S \underset{˙}{\lor} T) \to U \underset{˙}{\lor} S = U \underset{˙}{\lor} T)$
44	17 43	mpd	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land ((z \in A \land \neg z \underset{˙}{\leq} W) \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to U \underset{˙}{\lor} S = U \underset{˙}{\lor} T$
45	44	adantr	$⊢ ((((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land ((z \in A \land \neg z \underset{˙}{\leq} W) \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \land U \underset{˙}{\leq} (T \underset{˙}{\lor} z)) \to U \underset{˙}{\lor} S = U \underset{˙}{\lor} T$
46		simp3lr	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land ((z \in A \land \neg z \underset{˙}{\leq} W) \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to \neg z \underset{˙}{\leq} W$
47		nbrne2	$⊢ (U \underset{˙}{\leq} W \land \neg z \underset{˙}{\leq} W) \to U \neq z$
48	35 46 47	syl2anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land ((z \in A \land \neg z \underset{˙}{\leq} W) \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to U \neq z$
49	1 2 4	cvlatexch3	$⊢ (K \in CvLat \land (U \in A \land T \in A \land z \in A) \land (U \neq T \land U \neq z)) \to (U \underset{˙}{\leq} (T \underset{˙}{\lor} z) \to U \underset{˙}{\lor} T = U \underset{˙}{\lor} z)$
50	20 25 26 13 41 48 49	syl132anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land ((z \in A \land \neg z \underset{˙}{\leq} W) \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to (U \underset{˙}{\leq} (T \underset{˙}{\lor} z) \to U \underset{˙}{\lor} T = U \underset{˙}{\lor} z)$
51	50	imp	$⊢ ((((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land ((z \in A \land \neg z \underset{˙}{\leq} W) \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \land U \underset{˙}{\leq} (T \underset{˙}{\lor} z)) \to U \underset{˙}{\lor} T = U \underset{˙}{\lor} z$
52	45 51	eqtrd	$⊢ ((((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land ((z \in A \land \neg z \underset{˙}{\leq} W) \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \land U \underset{˙}{\leq} (T \underset{˙}{\lor} z)) \to U \underset{˙}{\lor} S = U \underset{˙}{\lor} z$
53	52	ex	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land ((z \in A \land \neg z \underset{˙}{\leq} W) \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to (U \underset{˙}{\leq} (T \underset{˙}{\lor} z) \to U \underset{˙}{\lor} S = U \underset{˙}{\lor} z)$
54	1 2 4	hlatlej2	$⊢ (K \in HL \land U \in A \land S \in A) \to S \underset{˙}{\leq} (U \underset{˙}{\lor} S)$
55	18 25 10 54	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land ((z \in A \land \neg z \underset{˙}{\leq} W) \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to S \underset{˙}{\leq} (U \underset{˙}{\lor} S)$
56		breq2	$⊢ U \underset{˙}{\lor} S = U \underset{˙}{\lor} z \to (S \underset{˙}{\leq} (U \underset{˙}{\lor} S) \leftrightarrow S \underset{˙}{\leq} (U \underset{˙}{\lor} z))$
57	55 56	syl5ibcom	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land ((z \in A \land \neg z \underset{˙}{\leq} W) \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to (U \underset{˙}{\lor} S = U \underset{˙}{\lor} z \to S \underset{˙}{\leq} (U \underset{˙}{\lor} z))$
58	1 2 4	cdleme21a	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (S \in A \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to S \neq z$
59	18 22 9 10 12 13 14 58	syl322anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land ((z \in A \land \neg z \underset{˙}{\leq} W) \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to S \neq z$
60	1 2 4	cvlatexch2	$⊢ (K \in CvLat \land (S \in A \land U \in A \land z \in A) \land S \neq z) \to (S \underset{˙}{\leq} (U \underset{˙}{\lor} z) \to U \underset{˙}{\leq} (S \underset{˙}{\lor} z))$
61	20 10 25 13 59 60	syl131anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land ((z \in A \land \neg z \underset{˙}{\leq} W) \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to (S \underset{˙}{\leq} (U \underset{˙}{\lor} z) \to U \underset{˙}{\leq} (S \underset{˙}{\lor} z))$
62	53 57 61	3syld	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land ((z \in A \land \neg z \underset{˙}{\leq} W) \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to (U \underset{˙}{\leq} (T \underset{˙}{\lor} z) \to U \underset{˙}{\leq} (S \underset{˙}{\lor} z))$
63	16 62	mtod	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land ((z \in A \land \neg z \underset{˙}{\leq} W) \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to \neg U \underset{˙}{\leq} (T \underset{˙}{\lor} z)$

Metamath Proof Explorer

Theorem cdleme21ct

Proof