cdleme22cN

Description: Part of proof of Lemma E in Crawley p. 113, 3rd paragraph, 5th line on p. 115. Show that t \/ v =/= p \/ q and s <_ p \/ q implies -. v <_ p \/ q. (Contributed by NM, 3-Dec-2012) (New usage is discouraged.)

	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)$
Assertion	cdleme22cN	$⊢ (((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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \to \neg V \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$

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		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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \to K \in HL$
7	6	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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \to K \in Lat$
8		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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \to P \in A$
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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \to Q \in A$
10		eqid	$⊢ {Base}_{K} = {Base}_{K}$
11	10 2 4	hlatjcl	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
12	6 8 9 11	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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
13		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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \to W \in H$
14	10 5	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
15	13 14	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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \to W \in {Base}_{K}$
16	10 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$
17	7 12 15 16	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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\leq} W$
18		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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \to \neg S \underset{˙}{\leq} W$
19		nbrne2	$⊢ (((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\leq} W \land \neg S \underset{˙}{\leq} W) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} W \neq S$
20	17 18 19	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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} W \neq S$
21		simp32l	$⊢ (((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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \to S \underset{˙}{\leq} (T \underset{˙}{\lor} V)$
22	21	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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \land V \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to S \underset{˙}{\leq} (T \underset{˙}{\lor} V)$
23	6	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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \land V \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to K \in HL$
24	13	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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \land V \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to W \in H$
25		simpl12	$⊢ ((((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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \land V \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
26		simpl13	$⊢ ((((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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \land V \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to Q \in A$
27		simp31l	$⊢ (((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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \to P \neq Q$
28	27	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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \land V \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to P \neq Q$
29		simp23l	$⊢ (((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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \to V \in A$
30	29	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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \land V \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to V \in A$
31		simp23r	$⊢ (((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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \to V \underset{˙}{\leq} W$
32	31	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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \land V \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to V \underset{˙}{\leq} W$
33		simpr	$⊢ ((((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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \land V \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to V \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
34		eqid	$⊢ (P \underset{˙}{\lor} Q) \underset{˙}{\land} W = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
35	1 2 3 4 5 34	cdleme22aa	$⊢ ((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) \land (V \in A \land V \underset{˙}{\leq} W \land V \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to V = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
36	23 24 25 26 28 30 32 33 35	syl233anc	$⊢ ((((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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \land V \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to V = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
37	36	oveq2d	$⊢ ((((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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \land V \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to T \underset{˙}{\lor} V = T \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W)$
38	22 37	breqtrd	$⊢ ((((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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \land V \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to S \underset{˙}{\leq} (T \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W))$
39		simp32r	$⊢ (((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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \to S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
40	39	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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \land V \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
41		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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \to S \in A$
42	10 4	atbase	$⊢ S \in A \to S \in {Base}_{K}$
43	41 42	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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \to S \in {Base}_{K}$
44		simp22	$⊢ (((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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \to T \in A$
45		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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \to \neg P \underset{˙}{\leq} W$
46	1 2 3 4 5	lhpat	$⊢ ((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 (P \underset{˙}{\lor} Q) \underset{˙}{\land} W \in A$
47	6 13 8 45 9 27 46	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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} W \in A$
48	10 2 4	hlatjcl	$⊢ (K \in HL \land T \in A \land (P \underset{˙}{\lor} Q) \underset{˙}{\land} W \in A) \to T \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \in {Base}_{K}$
49	6 44 47 48	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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \to T \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \in {Base}_{K}$
50	10 1 3	latlem12	$⊢ (K \in Lat \land (S \in {Base}_{K} \land T \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \in {Base}_{K} \land P \underset{˙}{\lor} Q \in {Base}_{K})) \to ((S \underset{˙}{\leq} (T \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W)) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \leftrightarrow S \underset{˙}{\leq} ((T \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W)) \underset{˙}{\land} (P \underset{˙}{\lor} Q)))$
51	7 43 49 12 50	syl13anc	$⊢ (((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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \to ((S \underset{˙}{\leq} (T \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W)) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \leftrightarrow S \underset{˙}{\leq} ((T \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W)) \underset{˙}{\land} (P \underset{˙}{\lor} Q)))$
52	51	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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \land V \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to ((S \underset{˙}{\leq} (T \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W)) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \leftrightarrow S \underset{˙}{\leq} ((T \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W)) \underset{˙}{\land} (P \underset{˙}{\lor} Q)))$
53	38 40 52	mpbi2and	$⊢ ((((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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \land V \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to S \underset{˙}{\leq} ((T \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W)) \underset{˙}{\land} (P \underset{˙}{\lor} Q))$
54		simp31r	$⊢ (((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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \to S \neq T$
55	41 44 54	3jca	$⊢ (((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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \to (S \in A \land T \in A \land S \neq T)$
56		simp33	$⊢ (((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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \to T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q$
57	56 21 39	3jca	$⊢ (((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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \to (T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
58	1 2 3 4 5	cdleme22b	$⊢ ((K \in HL \land (S \in A \land T \in A \land S \neq T)) \land (P \in A \land Q \in A \land P \neq Q) \land (V \in A \land (T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
59	6 55 8 9 27 29 57 58	syl232anc	$⊢ (((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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \to \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
60		hlatl	$⊢ K \in HL \to K \in AtLat$
61	6 60	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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \to K \in AtLat$
62		eqid	$⊢ 0. (K) = 0. (K)$
63	10 1 3 62 4	atnle	$⊢ (K \in AtLat \land T \in A \land P \underset{˙}{\lor} Q \in {Base}_{K}) \to (\neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \leftrightarrow T \underset{˙}{\land} (P \underset{˙}{\lor} Q) = 0. (K))$
64	61 44 12 63	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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \to (\neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \leftrightarrow T \underset{˙}{\land} (P \underset{˙}{\lor} Q) = 0. (K))$
65	59 64	mpbid	$⊢ (((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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \to T \underset{˙}{\land} (P \underset{˙}{\lor} Q) = 0. (K)$
66	65	oveq1d	$⊢ (((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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \to (T \underset{˙}{\land} (P \underset{˙}{\lor} Q)) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) = 0. (K) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W)$
67	10 4	atbase	$⊢ T \in A \to T \in {Base}_{K}$
68	44 67	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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \to T \in {Base}_{K}$
69	10 1 3	latmle1	$⊢ (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} (P \underset{˙}{\lor} Q)$
70	7 12 15 69	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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
71	10 1 2 3 4	atmod4i1	$⊢ (K \in HL \land ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W \in A \land T \in {Base}_{K} \land P \underset{˙}{\lor} Q \in {Base}_{K}) \land ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (T \underset{˙}{\land} (P \underset{˙}{\lor} Q)) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) = (T \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W)) \underset{˙}{\land} (P \underset{˙}{\lor} Q)$
72	6 47 68 12 70 71	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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \to (T \underset{˙}{\land} (P \underset{˙}{\lor} Q)) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) = (T \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W)) \underset{˙}{\land} (P \underset{˙}{\lor} Q)$
73		hlol	$⊢ K \in HL \to K \in OL$
74	6 73	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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \to K \in OL$
75	10 3	latmcl	$⊢ (K \in Lat \land P \underset{˙}{\lor} Q \in {Base}_{K} \land W \in {Base}_{K}) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} W \in {Base}_{K}$
76	7 12 15 75	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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} W \in {Base}_{K}$
77	10 2 62	olj02	$⊢ (K \in OL \land (P \underset{˙}{\lor} Q) \underset{˙}{\land} W \in {Base}_{K}) \to 0. (K) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
78	74 76 77	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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \to 0. (K) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
79	66 72 78	3eqtr3d	$⊢ (((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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \to (T \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W)) \underset{˙}{\land} (P \underset{˙}{\lor} Q) = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
80	79	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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \land V \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (T \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W)) \underset{˙}{\land} (P \underset{˙}{\lor} Q) = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
81	53 80	breqtrd	$⊢ ((((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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \land V \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W)$
82	1 4	atcmp	$⊢ (K \in AtLat \land S \in A \land (P \underset{˙}{\lor} Q) \underset{˙}{\land} W \in A) \to (S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \leftrightarrow S = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W)$
83	61 41 47 82	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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \to (S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \leftrightarrow S = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W)$
84	83	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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \land V \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \leftrightarrow S = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W)$
85	81 84	mpbid	$⊢ ((((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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \land V \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to S = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
86	85	eqcomd	$⊢ ((((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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \land V \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} W = S$
87	86	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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \to (V \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} W = S)$
88	87	necon3ad	$⊢ (((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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W \neq S \to \neg V \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
89	20 88	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 (V \in A \land V \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \to \neg V \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$

Metamath Proof Explorer

Theorem cdleme22cN

Proof