3atlem5

	Ref	Expression
Hypotheses	3at.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	3at.j	$⊢ \underset{˙}{\lor} = join (K)$
	3at.a	$⊢ A = Atoms (K)$
Assertion	3atlem5	$⊢ ((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 (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)) \land ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R = (S \underset{˙}{\lor} T) \underset{˙}{\lor} U$

Proof

Step	Hyp	Ref	Expression
1		3at.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		3at.j	$⊢ \underset{˙}{\lor} = join (K)$
3		3at.a	$⊢ A = Atoms (K)$
4		oveq2	$⊢ U = P \to (S \underset{˙}{\lor} T) \underset{˙}{\lor} U = (S \underset{˙}{\lor} T) \underset{˙}{\lor} P$
5	4	eqcoms	$⊢ P = U \to (S \underset{˙}{\lor} T) \underset{˙}{\lor} U = (S \underset{˙}{\lor} T) \underset{˙}{\lor} P$
6	5	breq2d	$⊢ P = U \to (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U) \leftrightarrow ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} P))$
7	5	eqeq2d	$⊢ P = U \to ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R = (S \underset{˙}{\lor} T) \underset{˙}{\lor} U \leftrightarrow (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R = (S \underset{˙}{\lor} T) \underset{˙}{\lor} P)$
8	6 7	imbi12d	$⊢ P = U \to ((((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R = (S \underset{˙}{\lor} T) \underset{˙}{\lor} U) \leftrightarrow (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} P) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R = (S \underset{˙}{\lor} T) \underset{˙}{\lor} P))$
9		simp1l	$⊢ (((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 (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U))) \land P \neq U \land ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U)) \to (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))$
10		simp1r1	$⊢ (((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 (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U))) \land P \neq U \land ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U)) \to \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
11		simp2	$⊢ (((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 (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U))) \land P \neq U \land ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U)) \to P \neq U$
12		simp1r3	$⊢ (((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 (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U))) \land P \neq U \land ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U)) \to \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)$
13		simp3	$⊢ (((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 (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U))) \land P \neq U \land ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U)) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U)$
14	1 2 3	3atlem3	$⊢ ((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 (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq U \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)) \land ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R = (S \underset{˙}{\lor} T) \underset{˙}{\lor} U$
15	9 10 11 12 13 14	syl131anc	$⊢ (((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 (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U))) \land P \neq U \land ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R = (S \underset{˙}{\lor} T) \underset{˙}{\lor} U$
16	15	3expia	$⊢ (((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 (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U))) \land P \neq U) \to (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R = (S \underset{˙}{\lor} T) \underset{˙}{\lor} U)$
17		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 (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)) \land ((R \underset{˙}{\lor} Q) \underset{˙}{\lor} P) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} P)) \to K \in HL$
18		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 (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)) \land ((R \underset{˙}{\lor} Q) \underset{˙}{\lor} P) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} P)) \to R \in A$
19		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 (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)) \land ((R \underset{˙}{\lor} Q) \underset{˙}{\lor} P) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} P)) \to Q \in A$
20		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 (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)) \land ((R \underset{˙}{\lor} Q) \underset{˙}{\lor} P) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} P)) \to P \in A$
21	18 19 20	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 (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)) \land ((R \underset{˙}{\lor} Q) \underset{˙}{\lor} P) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} P)) \to (R \in A \land Q \in A \land P \in A)$
22		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 (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)) \land ((R \underset{˙}{\lor} Q) \underset{˙}{\lor} P) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} P)) \to S \in A$
23		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 (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)) \land ((R \underset{˙}{\lor} Q) \underset{˙}{\lor} P) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} P)) \to T \in A$
24	22 23	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 (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)) \land ((R \underset{˙}{\lor} Q) \underset{˙}{\lor} P) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} P)) \to (S \in A \land T \in A)$
25		simp21	$⊢ ((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 (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)) \land ((R \underset{˙}{\lor} Q) \underset{˙}{\lor} P) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} P)) \to \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
26		simp22	$⊢ ((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 (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)) \land ((R \underset{˙}{\lor} Q) \underset{˙}{\lor} P) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} P)) \to P \neq Q$
27	1 2 3	hlatexch2	$⊢ (K \in HL \land (P \in A \land R \in A \land Q \in A) \land P \neq Q) \to (P \underset{˙}{\leq} (R \underset{˙}{\lor} Q) \to R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
28	17 20 18 19 26 27	syl131anc	$⊢ ((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 (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)) \land ((R \underset{˙}{\lor} Q) \underset{˙}{\lor} P) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} P)) \to (P \underset{˙}{\leq} (R \underset{˙}{\lor} Q) \to R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
29	25 28	mtod	$⊢ ((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 (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)) \land ((R \underset{˙}{\lor} Q) \underset{˙}{\lor} P) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} P)) \to \neg P \underset{˙}{\leq} (R \underset{˙}{\lor} Q)$
30	17	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 (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)) \land ((R \underset{˙}{\lor} Q) \underset{˙}{\lor} P) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} P)) \to K \in Lat$
31		eqid	$⊢ {Base}_{K} = {Base}_{K}$
32	31 3	atbase	$⊢ R \in A \to R \in {Base}_{K}$
33	18 32	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 (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)) \land ((R \underset{˙}{\lor} Q) \underset{˙}{\lor} P) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} P)) \to R \in {Base}_{K}$
34	31 3	atbase	$⊢ P \in A \to P \in {Base}_{K}$
35	20 34	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 (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)) \land ((R \underset{˙}{\lor} Q) \underset{˙}{\lor} P) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} P)) \to P \in {Base}_{K}$
36	31 3	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
37	19 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 (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)) \land ((R \underset{˙}{\lor} Q) \underset{˙}{\lor} P) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} P)) \to Q \in {Base}_{K}$
38	31 1 2	latnlej1r	$⊢ (K \in Lat \land (R \in {Base}_{K} \land P \in {Base}_{K} \land Q \in {Base}_{K}) \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to R \neq Q$
39	30 33 35 37 25 38	syl131anc	$⊢ ((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 (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)) \land ((R \underset{˙}{\lor} Q) \underset{˙}{\lor} P) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} P)) \to R \neq Q$
40		simp3	$⊢ ((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 (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)) \land ((R \underset{˙}{\lor} Q) \underset{˙}{\lor} P) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} P)) \to ((R \underset{˙}{\lor} Q) \underset{˙}{\lor} P) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} P)$
41	1 2 3	3atlem4	$⊢ ((K \in HL \land (R \in A \land Q \in A \land P \in A) \land (S \in A \land T \in A)) \land (\neg P \underset{˙}{\leq} (R \underset{˙}{\lor} Q) \land R \neq Q) \land ((R \underset{˙}{\lor} Q) \underset{˙}{\lor} P) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} P)) \to (R \underset{˙}{\lor} Q) \underset{˙}{\lor} P = (S \underset{˙}{\lor} T) \underset{˙}{\lor} P$
42	17 21 24 29 39 40 41	syl321anc	$⊢ ((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 (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)) \land ((R \underset{˙}{\lor} Q) \underset{˙}{\lor} P) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} P)) \to (R \underset{˙}{\lor} Q) \underset{˙}{\lor} P = (S \underset{˙}{\lor} T) \underset{˙}{\lor} P$
43	42	3expia	$⊢ ((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 (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U))) \to (((R \underset{˙}{\lor} Q) \underset{˙}{\lor} P) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} P) \to (R \underset{˙}{\lor} Q) \underset{˙}{\lor} P = (S \underset{˙}{\lor} T) \underset{˙}{\lor} P)$
44		simpl1	$⊢ ((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 (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U))) \to K \in HL$
45	44	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 (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U))) \to K \in Lat$
46		simpl21	$⊢ ((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 (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U))) \to P \in A$
47	46 34	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 (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U))) \to P \in {Base}_{K}$
48		simpl22	$⊢ ((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 (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U))) \to Q \in A$
49	48 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 (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U))) \to Q \in {Base}_{K}$
50		simpl23	$⊢ ((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 (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U))) \to R \in A$
51	50 32	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 (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U))) \to R \in {Base}_{K}$
52	31 2	latj31	$⊢ (K \in Lat \land (P \in {Base}_{K} \land Q \in {Base}_{K} \land R \in {Base}_{K})) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R = (R \underset{˙}{\lor} Q) \underset{˙}{\lor} P$
53	45 47 49 51 52	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 (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R = (R \underset{˙}{\lor} Q) \underset{˙}{\lor} P$
54	53	breq1d	$⊢ ((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 (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U))) \to (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} P) \leftrightarrow ((R \underset{˙}{\lor} Q) \underset{˙}{\lor} P) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} P))$
55	53	eqeq1d	$⊢ ((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 (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U))) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R = (S \underset{˙}{\lor} T) \underset{˙}{\lor} P \leftrightarrow (R \underset{˙}{\lor} Q) \underset{˙}{\lor} P = (S \underset{˙}{\lor} T) \underset{˙}{\lor} P)$
56	43 54 55	3imtr4d	$⊢ ((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 (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U))) \to (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} P) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R = (S \underset{˙}{\lor} T) \underset{˙}{\lor} P)$
57	8 16 56	pm2.61ne	$⊢ ((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 (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U))) \to (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R = (S \underset{˙}{\lor} T) \underset{˙}{\lor} U)$
58	57	3impia	$⊢ ((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 (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land P \neq Q \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)) \land ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} U)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R = (S \underset{˙}{\lor} T) \underset{˙}{\lor} U$

Metamath Proof Explorer

Theorem 3atlem5

Proof