3dim2

Description: Construct 2 new layers on top of 2 given atoms. (Contributed by NM, 27-Jul-2012)

	Ref	Expression
Hypotheses	3dim0.j	$⊢ \underset{˙}{\lor} = join (K)$
	3dim0.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	3dim0.a	$⊢ A = Atoms (K)$
Assertion	3dim2	$⊢ (K \in HL \land P \in A \land Q \in A) \to \exists r \in A \exists s \in A (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r))$

Proof

Step	Hyp	Ref	Expression
1		3dim0.j	$⊢ \underset{˙}{\lor} = join (K)$
2		3dim0.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		3dim0.a	$⊢ A = Atoms (K)$
4	1 2 3	3dim1	$⊢ (K \in HL \land Q \in A) \to \exists u \in A \exists v \in A \exists w \in A (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))$
5	4	3adant2	$⊢ (K \in HL \land P \in A \land Q \in A) \to \exists u \in A \exists v \in A \exists w \in A (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))$
6		simpl21	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land P = Q) \to u \in A$
7		simpl22	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land P = Q) \to v \in A$
8		simp31	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \to Q \neq u$
9	8	necomd	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \to u \neq Q$
10	9	adantr	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land P = Q) \to u \neq Q$
11		oveq1	$⊢ P = Q \to P \underset{˙}{\lor} Q = Q \underset{˙}{\lor} Q$
12		simp11	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \to K \in HL$
13		simp13	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \to Q \in A$
14	1 3	hlatjidm	$⊢ (K \in HL \land Q \in A) \to Q \underset{˙}{\lor} Q = Q$
15	12 13 14	syl2anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \to Q \underset{˙}{\lor} Q = Q$
16	11 15	sylan9eqr	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land P = Q) \to P \underset{˙}{\lor} Q = Q$
17	16	breq2d	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land P = Q) \to (u \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \leftrightarrow u \underset{˙}{\leq} Q)$
18	17	notbid	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land P = Q) \to (\neg u \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \leftrightarrow \neg u \underset{˙}{\leq} Q)$
19		hlatl	$⊢ K \in HL \to K \in AtLat$
20	12 19	syl	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \to K \in AtLat$
21		simp21	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \to u \in A$
22	2 3	atncmp	$⊢ (K \in AtLat \land u \in A \land Q \in A) \to (\neg u \underset{˙}{\leq} Q \leftrightarrow u \neq Q)$
23	20 21 13 22	syl3anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \to (\neg u \underset{˙}{\leq} Q \leftrightarrow u \neq Q)$
24	23	adantr	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land P = Q) \to (\neg u \underset{˙}{\leq} Q \leftrightarrow u \neq Q)$
25	18 24	bitrd	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land P = Q) \to (\neg u \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \leftrightarrow u \neq Q)$
26	10 25	mpbird	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land P = Q) \to \neg u \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
27		simpl32	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land P = Q) \to \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u)$
28	16	oveq1d	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land P = Q) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} u = Q \underset{˙}{\lor} u$
29	28	breq2d	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land P = Q) \to (v \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} u) \leftrightarrow v \underset{˙}{\leq} (Q \underset{˙}{\lor} u))$
30	27 29	mtbird	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land P = Q) \to \neg v \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} u)$
31		breq1	$⊢ r = u \to (r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \leftrightarrow u \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
32	31	notbid	$⊢ r = u \to (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \leftrightarrow \neg u \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
33		oveq2	$⊢ r = u \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} r = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} u$
34	33	breq2d	$⊢ r = u \to (s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r) \leftrightarrow s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} u))$
35	34	notbid	$⊢ r = u \to (\neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r) \leftrightarrow \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} u))$
36	32 35	anbi12d	$⊢ r = u \to ((\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r)) \leftrightarrow (\neg u \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} u)))$
37		breq1	$⊢ s = v \to (s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} u) \leftrightarrow v \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} u))$
38	37	notbid	$⊢ s = v \to (\neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} u) \leftrightarrow \neg v \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} u))$
39	38	anbi2d	$⊢ s = v \to ((\neg u \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} u)) \leftrightarrow (\neg u \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg v \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} u)))$
40	36 39	rspc2ev	$⊢ (u \in A \land v \in A \land (\neg u \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg v \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} u))) \to \exists r \in A \exists s \in A (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r))$
41	6 7 26 30 40	syl112anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land P = Q) \to \exists r \in A \exists s \in A (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r))$
42		simp22	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \to v \in A$
43		simp23	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \to w \in A$
44	42 43	jca	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \to (v \in A \land w \in A)$
45	44	ad2antrr	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land P \neq Q) \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} u)) \to (v \in A \land w \in A)$
46		simpll1	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land P \neq Q) \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} u)) \to (K \in HL \land P \in A \land Q \in A)$
47		simp32	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \to \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u)$
48		simp33	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \to \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v)$
49	21 47 48	3jca	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \to (u \in A \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))$
50	49	ad2antrr	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land P \neq Q) \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} u)) \to (u \in A \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))$
51		simplr	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land P \neq Q) \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} u)) \to P \neq Q$
52		simpr	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land P \neq Q) \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} u)) \to P \underset{˙}{\leq} (Q \underset{˙}{\lor} u)$
53	1 2 3	3dimlem2	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (u \in A \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \land (P \neq Q \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} u))) \to (P \neq Q \land \neg v \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg w \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} v))$
54	46 50 51 52 53	syl112anc	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land P \neq Q) \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} u)) \to (P \neq Q \land \neg v \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg w \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} v))$
55		3simpc	$⊢ (P \neq Q \land \neg v \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg w \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} v)) \to (\neg v \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg w \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} v))$
56	54 55	syl	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land P \neq Q) \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} u)) \to (\neg v \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg w \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} v))$
57		breq1	$⊢ r = v \to (r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \leftrightarrow v \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
58	57	notbid	$⊢ r = v \to (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \leftrightarrow \neg v \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
59		oveq2	$⊢ r = v \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} r = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} v$
60	59	breq2d	$⊢ r = v \to (s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r) \leftrightarrow s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} v))$
61	60	notbid	$⊢ r = v \to (\neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r) \leftrightarrow \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} v))$
62	58 61	anbi12d	$⊢ r = v \to ((\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r)) \leftrightarrow (\neg v \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} v)))$
63		breq1	$⊢ s = w \to (s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} v) \leftrightarrow w \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} v))$
64	63	notbid	$⊢ s = w \to (\neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} v) \leftrightarrow \neg w \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} v))$
65	64	anbi2d	$⊢ s = w \to ((\neg v \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} v)) \leftrightarrow (\neg v \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg w \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} v)))$
66	62 65	rspc2ev	$⊢ (v \in A \land w \in A \land (\neg v \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg w \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} v))) \to \exists r \in A \exists s \in A (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r))$
67	66	3expa	$⊢ ((v \in A \land w \in A) \land (\neg v \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg w \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} v))) \to \exists r \in A \exists s \in A (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r))$
68	45 56 67	syl2anc	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land P \neq Q) \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} u)) \to \exists r \in A \exists s \in A (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r))$
69	21 43	jca	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \to (u \in A \land w \in A)$
70	69	ad3antrrr	$⊢ (((((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land P \neq Q) \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} u)) \land P \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to (u \in A \land w \in A)$
71		simp1	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \to (K \in HL \land P \in A \land Q \in A)$
72	21 42	jca	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \to (u \in A \land v \in A)$
73	8 48	jca	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \to (Q \neq u \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))$
74	71 72 73	3jca	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \to ((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A) \land (Q \neq u \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v)))$
75	74	ad3antrrr	$⊢ (((((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land P \neq Q) \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} u)) \land P \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to ((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A) \land (Q \neq u \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v)))$
76		simpllr	$⊢ (((((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land P \neq Q) \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} u)) \land P \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to P \neq Q$
77		simplr	$⊢ (((((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land P \neq Q) \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} u)) \land P \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} u)$
78		simpr	$⊢ (((((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land P \neq Q) \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} u)) \land P \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to P \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v)$
79	1 2 3	3dimlem3	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A) \land (Q \neq u \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land (P \neq Q \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land P \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \to (P \neq Q \land \neg u \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg w \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} u))$
80	75 76 77 78 79	syl13anc	$⊢ (((((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land P \neq Q) \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} u)) \land P \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to (P \neq Q \land \neg u \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg w \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} u))$
81		3simpc	$⊢ (P \neq Q \land \neg u \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg w \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} u)) \to (\neg u \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg w \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} u))$
82	80 81	syl	$⊢ (((((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land P \neq Q) \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} u)) \land P \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to (\neg u \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg w \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} u))$
83		breq1	$⊢ s = w \to (s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} u) \leftrightarrow w \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} u))$
84	83	notbid	$⊢ s = w \to (\neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} u) \leftrightarrow \neg w \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} u))$
85	84	anbi2d	$⊢ s = w \to ((\neg u \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} u)) \leftrightarrow (\neg u \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg w \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} u)))$
86	36 85	rspc2ev	$⊢ (u \in A \land w \in A \land (\neg u \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg w \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} u))) \to \exists r \in A \exists s \in A (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r))$
87	86	3expa	$⊢ ((u \in A \land w \in A) \land (\neg u \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg w \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} u))) \to \exists r \in A \exists s \in A (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r))$
88	70 82 87	syl2anc	$⊢ (((((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land P \neq Q) \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} u)) \land P \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to \exists r \in A \exists s \in A (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r))$
89	72	ad3antrrr	$⊢ (((((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land P \neq Q) \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} u)) \land \neg P \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to (u \in A \land v \in A)$
90	8 47	jca	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \to (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u))$
91	71 72 90	3jca	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \to ((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u)))$
92	91	ad3antrrr	$⊢ (((((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land P \neq Q) \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} u)) \land \neg P \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to ((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u)))$
93		simpllr	$⊢ (((((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land P \neq Q) \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} u)) \land \neg P \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to P \neq Q$
94		simplr	$⊢ (((((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land P \neq Q) \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} u)) \land \neg P \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} u)$
95		simpr	$⊢ (((((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land P \neq Q) \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} u)) \land \neg P \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to \neg P \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v)$
96	1 2 3	3dimlem4	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u))) \land (P \neq Q \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} u)) \land \neg P \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to (P \neq Q \land \neg u \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg v \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} u))$
97	92 93 94 95 96	syl121anc	$⊢ (((((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land P \neq Q) \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} u)) \land \neg P \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to (P \neq Q \land \neg u \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg v \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} u))$
98		3simpc	$⊢ (P \neq Q \land \neg u \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg v \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} u)) \to (\neg u \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg v \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} u))$
99	97 98	syl	$⊢ (((((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land P \neq Q) \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} u)) \land \neg P \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to (\neg u \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg v \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} u))$
100	40	3expa	$⊢ ((u \in A \land v \in A) \land (\neg u \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg v \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} u))) \to \exists r \in A \exists s \in A (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r))$
101	89 99 100	syl2anc	$⊢ (((((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land P \neq Q) \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} u)) \land \neg P \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to \exists r \in A \exists s \in A (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r))$
102	88 101	pm2.61dan	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land P \neq Q) \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} u)) \to \exists r \in A \exists s \in A (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r))$
103	68 102	pm2.61dan	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land P \neq Q) \to \exists r \in A \exists s \in A (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r))$
104	41 103	pm2.61dane	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A \land w \in A) \land (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \to \exists r \in A \exists s \in A (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r))$
105	104	3exp	$⊢ (K \in HL \land P \in A \land Q \in A) \to ((u \in A \land v \in A \land w \in A) \to ((Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to \exists r \in A \exists s \in A (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r))))$
106	105	3expd	$⊢ (K \in HL \land P \in A \land Q \in A) \to (u \in A \to (v \in A \to (w \in A \to ((Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to \exists r \in A \exists s \in A (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r))))))$
107	106	imp32	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A)) \to (w \in A \to ((Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to \exists r \in A \exists s \in A (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r))))$
108	107	rexlimdv	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (u \in A \land v \in A)) \to (\exists w \in A (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to \exists r \in A \exists s \in A (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r)))$
109	108	rexlimdvva	$⊢ (K \in HL \land P \in A \land Q \in A) \to (\exists u \in A \exists v \in A \exists w \in A (Q \neq u \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((Q \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to \exists r \in A \exists s \in A (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r)))$
110	5 109	mpd	$⊢ (K \in HL \land P \in A \land Q \in A) \to \exists r \in A \exists s \in A (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r))$

Metamath Proof Explorer

Theorem 3dim2

Proof