cdleme20

Description: Combine cdleme19f and cdleme20m to eliminate -. R .<_ ( S .\/ T ) condition. (Contributed by NM, 28-Nov-2012)

	Ref	Expression
Hypotheses	cdleme19.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdleme19.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdleme19.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdleme19.a	$⊢ A = Atoms (K)$
	cdleme19.h	$⊢ H = LHyp (K)$
	cdleme19.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
	cdleme19.f	$⊢ F = (S \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W))$
	cdleme19.g	$⊢ G = (T \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} T) \underset{˙}{\land} W))$
	cdleme19.d	$⊢ D = (R \underset{˙}{\lor} S) \underset{˙}{\land} W$
	cdleme19.y	$⊢ Y = (R \underset{˙}{\lor} T) \underset{˙}{\land} W$
	cdleme20.v	$⊢ V = (S \underset{˙}{\lor} T) \underset{˙}{\land} W$
	cdleme20.n	$⊢ N = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (F \underset{˙}{\lor} D)$
	cdleme20.o	$⊢ O = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (G \underset{˙}{\lor} Y)$
Assertion	cdleme20	$⊢ (((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to N = O$

Proof

Step	Hyp	Ref	Expression
1		cdleme19.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdleme19.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdleme19.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdleme19.a	$⊢ A = Atoms (K)$
5		cdleme19.h	$⊢ H = LHyp (K)$
6		cdleme19.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
7		cdleme19.f	$⊢ F = (S \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W))$
8		cdleme19.g	$⊢ G = (T \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} T) \underset{˙}{\land} W))$
9		cdleme19.d	$⊢ D = (R \underset{˙}{\lor} S) \underset{˙}{\land} W$
10		cdleme19.y	$⊢ Y = (R \underset{˙}{\lor} T) \underset{˙}{\land} W$
11		cdleme20.v	$⊢ V = (S \underset{˙}{\lor} T) \underset{˙}{\land} W$
12		cdleme20.n	$⊢ N = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (F \underset{˙}{\lor} D)$
13		cdleme20.o	$⊢ O = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (G \underset{˙}{\lor} Y)$
14		simpl1	$⊢ ((((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land R \underset{˙}{\leq} (S \underset{˙}{\lor} T)) \to ((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))$
15		simpl22	$⊢ ((((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land R \underset{˙}{\leq} (S \underset{˙}{\lor} T)) \to (S \in A \land \neg S \underset{˙}{\leq} W)$
16		simpl23	$⊢ ((((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land R \underset{˙}{\leq} (S \underset{˙}{\lor} T)) \to (T \in A \land \neg T \underset{˙}{\leq} W)$
17		simp21l	$⊢ (((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to R \in A$
18	17	adantr	$⊢ ((((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land R \underset{˙}{\leq} (S \underset{˙}{\lor} T)) \to R \in A$
19		simpl31	$⊢ ((((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land R \underset{˙}{\leq} (S \underset{˙}{\lor} T)) \to (P \neq Q \land S \neq T)$
20		simp321	$⊢ (((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
21	20	adantr	$⊢ ((((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land R \underset{˙}{\leq} (S \underset{˙}{\lor} T)) \to \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
22		simp322	$⊢ (((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
23	22	adantr	$⊢ ((((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land R \underset{˙}{\leq} (S \underset{˙}{\lor} T)) \to \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
24	21 23	jca	$⊢ ((((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land R \underset{˙}{\leq} (S \underset{˙}{\lor} T)) \to (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
25		simp323	$⊢ (((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
26	25	anim1i	$⊢ ((((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land R \underset{˙}{\leq} (S \underset{˙}{\lor} T)) \to (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \underset{˙}{\leq} (S \underset{˙}{\lor} T))$
27	1 2 3 4 5 6 7 8 9 10 12 13	cdleme19f	$⊢ (((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 R \in A) \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)) \land (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \underset{˙}{\leq} (S \underset{˙}{\lor} T)))) \to N = O$
28	14 15 16 18 19 24 26 27	syl133anc	$⊢ ((((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land R \underset{˙}{\leq} (S \underset{˙}{\lor} T)) \to N = O$
29		simpl11	$⊢ ((((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T)) \to (K \in HL \land W \in H)$
30		simpl12	$⊢ ((((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T)) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
31		simpl13	$⊢ ((((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T)) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
32		simpl21	$⊢ ((((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T)) \to (R \in A \land \neg R \underset{˙}{\leq} W)$
33		simpl22	$⊢ ((((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T)) \to (S \in A \land \neg S \underset{˙}{\leq} W)$
34		simpl23	$⊢ ((((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T)) \to (T \in A \land \neg T \underset{˙}{\leq} W)$
35		simpl31	$⊢ ((((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T)) \to (P \neq Q \land S \neq T)$
36		simpl32	$⊢ ((((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T)) \to (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
37		simpr	$⊢ ((((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T)) \to \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T)$
38		simpl33	$⊢ ((((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T)) \to \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T)$
39	37 38	jca	$⊢ ((((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T)) \to (\neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))$
40	1 2 3 4 5 6 7 8 9 10 11 12 13	cdleme20m	$⊢ (((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (\neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T)))) \to N = O$
41	29 30 31 32 33 34 35 36 39 40	syl333anc	$⊢ ((((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T)) \to N = O$
42	28 41	pm2.61dan	$⊢ (((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 ((R \in A \land \neg R \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) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to N = O$

Metamath Proof Explorer

Theorem cdleme20

Proof