4atlem3

Description: Lemma for 4at . Break inequality into 4 cases. (Contributed by NM, 8-Jul-2012)

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

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		simpl11	$⊢ (((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 (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 K \in HL$
5		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 V \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 (K \in HL \land P \in A \land Q \in A)$
6		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 V \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 R \in A$
7		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 V \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 S \in A$
8		simpr	$⊢ (((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 (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 (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))$
9		eqid	$⊢ LVols (K) = LVols (K)$
10	1 2 3 9	lvoli2	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \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 ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\lor} S \in LVols (K)$
11	5 6 7 8 10	syl121anc	$⊢ (((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 (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 ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\lor} S \in LVols (K)$
12		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 V \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 T \in A$
13		simpl3l	$⊢ (((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 (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 U \in A$
14		simpl3r	$⊢ (((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 (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 V \in A$
15	1 2 3 9	lvolnle3at	$⊢ ((K \in HL \land ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\lor} S \in LVols (K)) \land (T \in A \land U \in A \land V \in A)) \to \neg (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\lor} S) \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V)$
16	4 11 12 13 14 15	syl23anc	$⊢ (((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 (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 \neg (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\lor} S) \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V)$
17	4	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 (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 K \in Lat$
18		eqid	$⊢ {Base}_{K} = {Base}_{K}$
19	18 2 3	hlatjcl	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
20	5 19	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 (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 P \underset{˙}{\lor} Q \in {Base}_{K}$
21	18 2 3	hlatjcl	$⊢ (K \in HL \land R \in A \land S \in A) \to R \underset{˙}{\lor} S \in {Base}_{K}$
22	4 6 7 21	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 (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 R \underset{˙}{\lor} S \in {Base}_{K}$
23	18 2 3	hlatjcl	$⊢ (K \in HL \land T \in A \land U \in A) \to T \underset{˙}{\lor} U \in {Base}_{K}$
24	4 12 13 23	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 (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 T \underset{˙}{\lor} U \in {Base}_{K}$
25	18 3	atbase	$⊢ V \in A \to V \in {Base}_{K}$
26	14 25	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 (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 V \in {Base}_{K}$
27	18 2	latjcl	$⊢ (K \in Lat \land T \underset{˙}{\lor} U \in {Base}_{K} \land V \in {Base}_{K}) \to (T \underset{˙}{\lor} U) \underset{˙}{\lor} V \in {Base}_{K}$
28	17 24 26 27	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 (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 (T \underset{˙}{\lor} U) \underset{˙}{\lor} V \in {Base}_{K}$
29	18 1 2	latjle12	$⊢ (K \in Lat \land (P \underset{˙}{\lor} Q \in {Base}_{K} \land R \underset{˙}{\lor} S \in {Base}_{K} \land (T \underset{˙}{\lor} U) \underset{˙}{\lor} V \in {Base}_{K})) \to (((P \underset{˙}{\lor} Q) \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V) \land (R \underset{˙}{\lor} S) \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V)) \leftrightarrow ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S)) \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V))$
30	17 20 22 28 29	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 (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 (((P \underset{˙}{\lor} Q) \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V) \land (R \underset{˙}{\lor} S) \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V)) \leftrightarrow ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S)) \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V))$
31		simpl12	$⊢ (((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 (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 P \in A$
32	18 3	atbase	$⊢ P \in A \to P \in {Base}_{K}$
33	31 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 V \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 P \in {Base}_{K}$
34		simpl13	$⊢ (((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 (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 \in A$
35	18 3	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
36	34 35	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 (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 \in {Base}_{K}$
37	18 1 2	latjle12	$⊢ (K \in Lat \land (P \in {Base}_{K} \land Q \in {Base}_{K} \land (T \underset{˙}{\lor} U) \underset{˙}{\lor} V \in {Base}_{K})) \to ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V)) \leftrightarrow (P \underset{˙}{\lor} Q) \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V))$
38	17 33 36 28 37	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 (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 ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V)) \leftrightarrow (P \underset{˙}{\lor} Q) \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V))$
39	18 3	atbase	$⊢ R \in A \to R \in {Base}_{K}$
40	6 39	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 (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 R \in {Base}_{K}$
41	18 3	atbase	$⊢ S \in A \to S \in {Base}_{K}$
42	7 41	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 (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 S \in {Base}_{K}$
43	18 1 2	latjle12	$⊢ (K \in Lat \land (R \in {Base}_{K} \land S \in {Base}_{K} \land (T \underset{˙}{\lor} U) \underset{˙}{\lor} V \in {Base}_{K})) \to ((R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V)) \leftrightarrow (R \underset{˙}{\lor} S) \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V))$
44	17 40 42 28 43	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 (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 ((R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V)) \leftrightarrow (R \underset{˙}{\lor} S) \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V))$
45	38 44	anbi12d	$⊢ (((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 (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 (((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V)) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V))) \leftrightarrow ((P \underset{˙}{\lor} Q) \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V) \land (R \underset{˙}{\lor} S) \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V)))$
46	18 2	latjass	$⊢ (K \in Lat \land (P \underset{˙}{\lor} Q \in {Base}_{K} \land R \in {Base}_{K} \land S \in {Base}_{K})) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\lor} S = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S)$
47	17 20 40 42 46	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 (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 ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\lor} S = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S)$
48	47	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 V \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 ((((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\lor} S) \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V) \leftrightarrow ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S)) \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V))$
49	30 45 48	3bitr4d	$⊢ (((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 (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 (((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V)) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V))) \leftrightarrow (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\lor} S) \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V))$
50	16 49	mtbird	$⊢ (((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 (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 \neg ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V)) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V)))$
51		ianor	$⊢ \neg ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V)) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V))) \leftrightarrow (\neg (P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V)) \lor \neg (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V)))$
52		ianor	$⊢ \neg (P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V)) \leftrightarrow (\neg P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V) \lor \neg Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V))$
53		ianor	$⊢ \neg (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V)) \leftrightarrow (\neg R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V) \lor \neg S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V))$
54	52 53	orbi12i	$⊢ (\neg (P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V)) \lor \neg (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V))) \leftrightarrow ((\neg P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V) \lor \neg Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V)) \lor (\neg R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V) \lor \neg S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V)))$
55	51 54	bitri	$⊢ \neg ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V)) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V))) \leftrightarrow ((\neg P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V) \lor \neg Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V)) \lor (\neg R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V) \lor \neg S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V)))$
56	50 55	sylib	$⊢ (((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 (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 ((\neg P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V) \lor \neg Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V)) \lor (\neg R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V) \lor \neg S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V)))$

Metamath Proof Explorer

Theorem 4atlem3

Proof