4atlem12b

Description: Lemma for 4at . Substitute T for P (cont.). (Contributed by NM, 11-Jul-2012)

	Ref	Expression
Hypotheses	4at.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	4at.j	$⊢ \underset{˙}{\lor} = join (K)$
	4at.a	$⊢ A = Atoms (K)$
Assertion	4atlem12b	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land ((P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)$

Proof

Step	Hyp	Ref	Expression
1		4at.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		4at.j	$⊢ \underset{˙}{\lor} = join (K)$
3		4at.a	$⊢ A = Atoms (K)$
4		simp11	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land ((P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to (K \in HL \land P \in A \land Q \in A)$
5		simp121	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land ((P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to R \in A$
6		simp122	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land ((P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to S \in A$
7	5 6	jca	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land ((P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to (R \in A \land S \in A)$
8		simp13	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land ((P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to (U \in A \land V \in A \land W \in A)$
9	4 7 8	3jca	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land ((P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A))$
10		simp2l	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land ((P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))$
11	9 10	jca	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land ((P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)))$
12		simp3lr	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land ((P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))$
13		simp3rl	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land ((P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))$
14		simp3rr	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land ((P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))$
15		simp111	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land ((P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to K \in HL$
16	15	hllatd	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land ((P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to K \in Lat$
17		eqid	$⊢ {Base}_{K} = {Base}_{K}$
18	17 3	atbase	$⊢ R \in A \to R \in {Base}_{K}$
19	5 18	syl	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land ((P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to R \in {Base}_{K}$
20	17 3	atbase	$⊢ S \in A \to S \in {Base}_{K}$
21	6 20	syl	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land ((P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to S \in {Base}_{K}$
22		simp123	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land ((P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to T \in A$
23		simp131	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land ((P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to U \in A$
24	17 2 3	hlatjcl	$⊢ (K \in HL \land T \in A \land U \in A) \to T \underset{˙}{\lor} U \in {Base}_{K}$
25	15 22 23 24	syl3anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land ((P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to T \underset{˙}{\lor} U \in {Base}_{K}$
26		simp132	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land ((P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to V \in A$
27		simp133	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land ((P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to W \in A$
28	17 2 3	hlatjcl	$⊢ (K \in HL \land V \in A \land W \in A) \to V \underset{˙}{\lor} W \in {Base}_{K}$
29	15 26 27 28	syl3anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land ((P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to V \underset{˙}{\lor} W \in {Base}_{K}$
30	17 2	latjcl	$⊢ (K \in Lat \land T \underset{˙}{\lor} U \in {Base}_{K} \land V \underset{˙}{\lor} W \in {Base}_{K}) \to (T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W) \in {Base}_{K}$
31	16 25 29 30	syl3anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land ((P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to (T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W) \in {Base}_{K}$
32	17 1 2	latjle12	$⊢ (K \in Lat \land (R \in {Base}_{K} \land S \in {Base}_{K} \land (T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W) \in {Base}_{K})) \to ((R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \leftrightarrow (R \underset{˙}{\lor} S) \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))$
33	16 19 21 31 32	syl13anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land ((P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to ((R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \leftrightarrow (R \underset{˙}{\lor} S) \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))$
34	13 14 33	mpbi2and	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land ((P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to (R \underset{˙}{\lor} S) \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))$
35		simp113	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land ((P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to Q \in A$
36	17 3	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
37	35 36	syl	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land ((P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to Q \in {Base}_{K}$
38	17 2 3	hlatjcl	$⊢ (K \in HL \land R \in A \land S \in A) \to R \underset{˙}{\lor} S \in {Base}_{K}$
39	15 5 6 38	syl3anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land ((P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to R \underset{˙}{\lor} S \in {Base}_{K}$
40	17 1 2	latjle12	$⊢ (K \in Lat \land (Q \in {Base}_{K} \land R \underset{˙}{\lor} S \in {Base}_{K} \land (T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W) \in {Base}_{K})) \to ((Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land (R \underset{˙}{\lor} S) \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \leftrightarrow (Q \underset{˙}{\lor} (R \underset{˙}{\lor} S)) \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))$
41	16 37 39 31 40	syl13anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land ((P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to ((Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land (R \underset{˙}{\lor} S) \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \leftrightarrow (Q \underset{˙}{\lor} (R \underset{˙}{\lor} S)) \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))$
42	12 34 41	mpbi2and	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land ((P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to (Q \underset{˙}{\lor} (R \underset{˙}{\lor} S)) \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))$
43		simp3ll	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land ((P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))$
44		simp112	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land ((P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to P \in A$
45		simp2r	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land ((P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)$
46	1 2 3	4atlem12a	$⊢ ((K \in HL \land P \in A \land T \in A) \land (U \in A \land V \in A \land W \in A) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \to (P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \leftrightarrow (P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W) = (T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))$
47	15 44 22 8 45 46	syl311anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land ((P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to (P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \leftrightarrow (P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W) = (T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))$
48	43 47	mpbid	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land ((P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to (P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W) = (T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)$
49	42 48	breqtrrd	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land ((P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to (Q \underset{˙}{\lor} (R \underset{˙}{\lor} S)) \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))$
50	1 2 3	4atlem11	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to ((Q \underset{˙}{\lor} (R \underset{˙}{\lor} S)) \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))$
51	11 49 50	sylc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land ((P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)$
52	51 48	eqtrd	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land ((P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)$

Metamath Proof Explorer

Theorem 4atlem12b

Proof