cdleme22g

Description: Part of proof of Lemma E in Crawley p. 113, 3rd paragraph, 6th and 7th lines on p. 115. F , G represent f(s), f(t) respectively. If s <_ t \/ v and -. s <_ p \/ q, then f(s) <_ f(t) \/ v. (Contributed by NM, 6-Dec-2012)

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

Proof

Step	Hyp	Ref	Expression
1		cdleme22.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdleme22.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdleme22.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdleme22.a	$⊢ A = Atoms (K)$
5		cdleme22.h	$⊢ H = LHyp (K)$
6		cdleme22g.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
7		cdleme22g.f	$⊢ F = (S \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W))$
8		cdleme22g.g	$⊢ G = (T \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} T) \underset{˙}{\land} W))$
9		simp11l	$⊢ (((K \in HL \land W \in H) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (\neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q)) \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 (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V)) \land (V \in A \land V \underset{˙}{\leq} W))) \to K \in HL$
10	9	hllatd	$⊢ (((K \in HL \land W \in H) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (\neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q)) \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 (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V)) \land (V \in A \land V \underset{˙}{\leq} W))) \to K \in Lat$
11		simp11	$⊢ (((K \in HL \land W \in H) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (\neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q)) \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 (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V)) \land (V \in A \land V \underset{˙}{\leq} W))) \to (K \in HL \land W \in H)$
12		simp2l	$⊢ (((K \in HL \land W \in H) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (\neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q)) \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 (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V)) \land (V \in A \land V \underset{˙}{\leq} W))) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
13		simp2r	$⊢ (((K \in HL \land W \in H) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (\neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q)) \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 (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V)) \land (V \in A \land V \underset{˙}{\leq} W))) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
14		simp31	$⊢ (((K \in HL \land W \in H) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (\neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q)) \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 (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V)) \land (V \in A \land V \underset{˙}{\leq} W))) \to (S \in A \land \neg S \underset{˙}{\leq} W)$
15		simp133	$⊢ (((K \in HL \land W \in H) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (\neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q)) \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 (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V)) \land (V \in A \land V \underset{˙}{\leq} W))) \to P \neq Q$
16		simp132	$⊢ (((K \in HL \land W \in H) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (\neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q)) \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 (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V)) \land (V \in A \land V \underset{˙}{\leq} W))) \to \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
17	1 2 3 4 5 6 7	cdleme3fa	$⊢ ((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 (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to F \in A$
18	11 12 13 14 15 16 17	syl132anc	$⊢ (((K \in HL \land W \in H) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (\neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q)) \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 (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V)) \land (V \in A \land V \underset{˙}{\leq} W))) \to F \in A$
19		simp12	$⊢ (((K \in HL \land W \in H) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (\neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q)) \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 (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V)) \land (V \in A \land V \underset{˙}{\leq} W))) \to (T \in A \land \neg T \underset{˙}{\leq} W)$
20		simp131	$⊢ (((K \in HL \land W \in H) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (\neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q)) \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 (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V)) \land (V \in A \land V \underset{˙}{\leq} W))) \to \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
21	1 2 3 4 5 6 8	cdleme3fa	$⊢ ((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 (T \in A \land \neg T \underset{˙}{\leq} W)) \land (P \neq Q \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to G \in A$
22	11 12 13 19 15 20 21	syl132anc	$⊢ (((K \in HL \land W \in H) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (\neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q)) \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 (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V)) \land (V \in A \land V \underset{˙}{\leq} W))) \to G \in A$
23		eqid	$⊢ {Base}_{K} = {Base}_{K}$
24	23 2 4	hlatjcl	$⊢ (K \in HL \land F \in A \land G \in A) \to F \underset{˙}{\lor} G \in {Base}_{K}$
25	9 18 22 24	syl3anc	$⊢ (((K \in HL \land W \in H) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (\neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q)) \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 (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V)) \land (V \in A \land V \underset{˙}{\leq} W))) \to F \underset{˙}{\lor} G \in {Base}_{K}$
26		simp11r	$⊢ (((K \in HL \land W \in H) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (\neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q)) \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 (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V)) \land (V \in A \land V \underset{˙}{\leq} W))) \to W \in H$
27	23 5	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
28	26 27	syl	$⊢ (((K \in HL \land W \in H) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (\neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q)) \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 (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V)) \land (V \in A \land V \underset{˙}{\leq} W))) \to W \in {Base}_{K}$
29	23 1 3	latmle1	$⊢ (K \in Lat \land F \underset{˙}{\lor} G \in {Base}_{K} \land W \in {Base}_{K}) \to ((F \underset{˙}{\lor} G) \underset{˙}{\land} W) \underset{˙}{\leq} (F \underset{˙}{\lor} G)$
30	10 25 28 29	syl3anc	$⊢ (((K \in HL \land W \in H) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (\neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q)) \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 (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V)) \land (V \in A \land V \underset{˙}{\leq} W))) \to ((F \underset{˙}{\lor} G) \underset{˙}{\land} W) \underset{˙}{\leq} (F \underset{˙}{\lor} G)$
31		simp33	$⊢ (((K \in HL \land W \in H) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (\neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q)) \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 (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V)) \land (V \in A \land V \underset{˙}{\leq} W))) \to (V \in A \land V \underset{˙}{\leq} W)$
32		simp32	$⊢ (((K \in HL \land W \in H) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (\neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q)) \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 (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V)) \land (V \in A \land V \underset{˙}{\leq} W))) \to (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))$
33	1 2 3 4 5	cdleme22d	$⊢ ((K \in HL \land W \in H) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to V = (S \underset{˙}{\lor} T) \underset{˙}{\land} W$
34	11 14 19 31 32 33	syl131anc	$⊢ (((K \in HL \land W \in H) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (\neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q)) \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 (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V)) \land (V \in A \land V \underset{˙}{\leq} W))) \to V = (S \underset{˙}{\lor} T) \underset{˙}{\land} W$
35		simp32l	$⊢ (((K \in HL \land W \in H) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (\neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q)) \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 (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V)) \land (V \in A \land V \underset{˙}{\leq} W))) \to S \neq T$
36	15 35	jca	$⊢ (((K \in HL \land W \in H) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (\neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q)) \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 (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V)) \land (V \in A \land V \underset{˙}{\leq} W))) \to (P \neq Q \land S \neq T)$
37	1 2 3 4 5 6 7 8	cdleme16	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (S \underset{˙}{\lor} T) \underset{˙}{\land} W = (F \underset{˙}{\lor} G) \underset{˙}{\land} W$
38	11 12 13 14 19 36 16 20 37	syl332anc	$⊢ (((K \in HL \land W \in H) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (\neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q)) \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 (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V)) \land (V \in A \land V \underset{˙}{\leq} W))) \to (S \underset{˙}{\lor} T) \underset{˙}{\land} W = (F \underset{˙}{\lor} G) \underset{˙}{\land} W$
39	34 38	eqtr2d	$⊢ (((K \in HL \land W \in H) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (\neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q)) \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 (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V)) \land (V \in A \land V \underset{˙}{\leq} W))) \to (F \underset{˙}{\lor} G) \underset{˙}{\land} W = V$
40	2 4	hlatjcom	$⊢ (K \in HL \land F \in A \land G \in A) \to F \underset{˙}{\lor} G = G \underset{˙}{\lor} F$
41	9 18 22 40	syl3anc	$⊢ (((K \in HL \land W \in H) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (\neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q)) \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 (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V)) \land (V \in A \land V \underset{˙}{\leq} W))) \to F \underset{˙}{\lor} G = G \underset{˙}{\lor} F$
42	30 39 41	3brtr3d	$⊢ (((K \in HL \land W \in H) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (\neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q)) \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 (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V)) \land (V \in A \land V \underset{˙}{\leq} W))) \to V \underset{˙}{\leq} (G \underset{˙}{\lor} F)$
43		hlcvl	$⊢ K \in HL \to K \in CvLat$
44	9 43	syl	$⊢ (((K \in HL \land W \in H) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (\neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q)) \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 (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V)) \land (V \in A \land V \underset{˙}{\leq} W))) \to K \in CvLat$
45		simp33l	$⊢ (((K \in HL \land W \in H) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (\neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q)) \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 (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V)) \land (V \in A \land V \underset{˙}{\leq} W))) \to V \in A$
46		simp33r	$⊢ (((K \in HL \land W \in H) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (\neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q)) \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 (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V)) \land (V \in A \land V \underset{˙}{\leq} W))) \to V \underset{˙}{\leq} W$
47	1 2 3 4 5 6 8	cdleme3	$⊢ ((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 (T \in A \land \neg T \underset{˙}{\leq} W)) \land (P \neq Q \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to \neg G \underset{˙}{\leq} W$
48	11 12 13 19 15 20 47	syl132anc	$⊢ (((K \in HL \land W \in H) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (\neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q)) \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 (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V)) \land (V \in A \land V \underset{˙}{\leq} W))) \to \neg G \underset{˙}{\leq} W$
49		nbrne2	$⊢ (V \underset{˙}{\leq} W \land \neg G \underset{˙}{\leq} W) \to V \neq G$
50	46 48 49	syl2anc	$⊢ (((K \in HL \land W \in H) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (\neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q)) \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 (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V)) \land (V \in A \land V \underset{˙}{\leq} W))) \to V \neq G$
51	1 2 4	cvlatexch1	$⊢ (K \in CvLat \land (V \in A \land F \in A \land G \in A) \land V \neq G) \to (V \underset{˙}{\leq} (G \underset{˙}{\lor} F) \to F \underset{˙}{\leq} (G \underset{˙}{\lor} V))$
52	44 45 18 22 50 51	syl131anc	$⊢ (((K \in HL \land W \in H) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (\neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q)) \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 (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V)) \land (V \in A \land V \underset{˙}{\leq} W))) \to (V \underset{˙}{\leq} (G \underset{˙}{\lor} F) \to F \underset{˙}{\leq} (G \underset{˙}{\lor} V))$
53	42 52	mpd	$⊢ (((K \in HL \land W \in H) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (\neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q)) \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 (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V)) \land (V \in A \land V \underset{˙}{\leq} W))) \to F \underset{˙}{\leq} (G \underset{˙}{\lor} V)$

Metamath Proof Explorer

Theorem cdleme22g

Proof