3dim1

Description: Construct a 3-dimensional volume (height-4 element) on top of a given atom P . (Contributed by NM, 25-Jul-2012)

	Ref	Expression
Hypotheses	3dim0.j	$⊢ \underset{˙}{\lor} = join (K)$
	3dim0.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	3dim0.a	$⊢ A = Atoms (K)$
Assertion	3dim1	$⊢ (K \in HL \land P \in A) \to \exists q \in A \exists r \in A \exists s \in A (P \neq q \land \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	3dim0	$⊢ K \in HL \to \exists t \in A \exists u \in A \exists v \in A \exists w \in A (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v))$
5	4	adantr	$⊢ (K \in HL \land P \in A) \to \exists t \in A \exists u \in A \exists v \in A \exists w \in A (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v))$
6		simpl2	$⊢ (((K \in HL \land P \in A \land t \in A) \land (u \in A \land v \in A \land w \in A) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land P = t) \to (u \in A \land v \in A \land w \in A)$
7	1 2 3	3dimlem1	$⊢ ((t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \land P = t) \to (P \neq u \land \neg v \underset{˙}{\leq} (P \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((P \underset{˙}{\lor} u) \underset{˙}{\lor} v))$
8	7	3ad2antl3	$⊢ (((K \in HL \land P \in A \land t \in A) \land (u \in A \land v \in A \land w \in A) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land P = t) \to (P \neq u \land \neg v \underset{˙}{\leq} (P \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((P \underset{˙}{\lor} u) \underset{˙}{\lor} v))$
9	1 2 3	3dim1lem5	$⊢ ((u \in A \land v \in A \land w \in A) \land (P \neq u \land \neg v \underset{˙}{\leq} (P \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((P \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \to \exists q \in A \exists r \in A \exists s \in A (P \neq q \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} q) \underset{˙}{\lor} r))$
10	6 8 9	syl2anc	$⊢ (((K \in HL \land P \in A \land t \in A) \land (u \in A \land v \in A \land w \in A) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land P = t) \to \exists q \in A \exists r \in A \exists s \in A (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		simp13	$⊢ ((K \in HL \land P \in A \land t \in A) \land (u \in A \land v \in A \land w \in A) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \to t \in A$
12		simp22	$⊢ ((K \in HL \land P \in A \land t \in A) \land (u \in A \land v \in A \land w \in A) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \to v \in A$
13		simp23	$⊢ ((K \in HL \land P \in A \land t \in A) \land (u \in A \land v \in A \land w \in A) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \to w \in A$
14	11 12 13	3jca	$⊢ ((K \in HL \land P \in A \land t \in A) \land (u \in A \land v \in A \land w \in A) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \to (t \in A \land v \in A \land w \in A)$
15	14	ad2antrr	$⊢ ((((K \in HL \land P \in A \land t \in A) \land (u \in A \land v \in A \land w \in A) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land P \neq t) \land P \underset{˙}{\leq} (t \underset{˙}{\lor} u)) \to (t \in A \land v \in A \land w \in A)$
16		simpll1	$⊢ ((((K \in HL \land P \in A \land t \in A) \land (u \in A \land v \in A \land w \in A) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land P \neq t) \land P \underset{˙}{\leq} (t \underset{˙}{\lor} u)) \to (K \in HL \land P \in A \land t \in A)$
17		simp21	$⊢ ((K \in HL \land P \in A \land t \in A) \land (u \in A \land v \in A \land w \in A) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \to u \in A$
18		simp32	$⊢ ((K \in HL \land P \in A \land t \in A) \land (u \in A \land v \in A \land w \in A) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \to \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u)$
19		simp33	$⊢ ((K \in HL \land P \in A \land t \in A) \land (u \in A \land v \in A \land w \in A) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \to \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v)$
20	17 18 19	3jca	$⊢ ((K \in HL \land P \in A \land t \in A) \land (u \in A \land v \in A \land w \in A) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \to (u \in A \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v))$
21	20	ad2antrr	$⊢ ((((K \in HL \land P \in A \land t \in A) \land (u \in A \land v \in A \land w \in A) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land P \neq t) \land P \underset{˙}{\leq} (t \underset{˙}{\lor} u)) \to (u \in A \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v))$
22		simplr	$⊢ ((((K \in HL \land P \in A \land t \in A) \land (u \in A \land v \in A \land w \in A) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land P \neq t) \land P \underset{˙}{\leq} (t \underset{˙}{\lor} u)) \to P \neq t$
23		simpr	$⊢ ((((K \in HL \land P \in A \land t \in A) \land (u \in A \land v \in A \land w \in A) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land P \neq t) \land P \underset{˙}{\leq} (t \underset{˙}{\lor} u)) \to P \underset{˙}{\leq} (t \underset{˙}{\lor} u)$
24	1 2 3	3dimlem2	$⊢ ((K \in HL \land P \in A \land t \in A) \land (u \in A \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \land (P \neq t \land P \underset{˙}{\leq} (t \underset{˙}{\lor} u))) \to (P \neq t \land \neg v \underset{˙}{\leq} (P \underset{˙}{\lor} t) \land \neg w \underset{˙}{\leq} ((P \underset{˙}{\lor} t) \underset{˙}{\lor} v))$
25	16 21 22 23 24	syl112anc	$⊢ ((((K \in HL \land P \in A \land t \in A) \land (u \in A \land v \in A \land w \in A) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land P \neq t) \land P \underset{˙}{\leq} (t \underset{˙}{\lor} u)) \to (P \neq t \land \neg v \underset{˙}{\leq} (P \underset{˙}{\lor} t) \land \neg w \underset{˙}{\leq} ((P \underset{˙}{\lor} t) \underset{˙}{\lor} v))$
26	1 2 3	3dim1lem5	$⊢ ((t \in A \land v \in A \land w \in A) \land (P \neq t \land \neg v \underset{˙}{\leq} (P \underset{˙}{\lor} t) \land \neg w \underset{˙}{\leq} ((P \underset{˙}{\lor} t) \underset{˙}{\lor} v))) \to \exists q \in A \exists r \in A \exists s \in A (P \neq q \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} q) \underset{˙}{\lor} r))$
27	15 25 26	syl2anc	$⊢ ((((K \in HL \land P \in A \land t \in A) \land (u \in A \land v \in A \land w \in A) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land P \neq t) \land P \underset{˙}{\leq} (t \underset{˙}{\lor} u)) \to \exists q \in A \exists r \in A \exists s \in A (P \neq q \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} q) \underset{˙}{\lor} r))$
28	11 17 13	3jca	$⊢ ((K \in HL \land P \in A \land t \in A) \land (u \in A \land v \in A \land w \in A) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \to (t \in A \land u \in A \land w \in A)$
29	28	ad2antrr	$⊢ ((((K \in HL \land P \in A \land t \in A) \land (u \in A \land v \in A \land w \in A) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land (P \neq t \land \neg P \underset{˙}{\leq} (t \underset{˙}{\lor} u))) \land P \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to (t \in A \land u \in A \land w \in A)$
30		simp1	$⊢ ((K \in HL \land P \in A \land t \in A) \land (u \in A \land v \in A \land w \in A) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \to (K \in HL \land P \in A \land t \in A)$
31	17 12	jca	$⊢ ((K \in HL \land P \in A \land t \in A) \land (u \in A \land v \in A \land w \in A) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \to (u \in A \land v \in A)$
32		simp31	$⊢ ((K \in HL \land P \in A \land t \in A) \land (u \in A \land v \in A \land w \in A) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \to t \neq u$
33	32 19	jca	$⊢ ((K \in HL \land P \in A \land t \in A) \land (u \in A \land v \in A \land w \in A) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \to (t \neq u \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v))$
34	30 31 33	3jca	$⊢ ((K \in HL \land P \in A \land t \in A) \land (u \in A \land v \in A \land w \in A) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \to ((K \in HL \land P \in A \land t \in A) \land (u \in A \land v \in A) \land (t \neq u \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v)))$
35	34	ad2antrr	$⊢ ((((K \in HL \land P \in A \land t \in A) \land (u \in A \land v \in A \land w \in A) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land (P \neq t \land \neg P \underset{˙}{\leq} (t \underset{˙}{\lor} u))) \land P \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to ((K \in HL \land P \in A \land t \in A) \land (u \in A \land v \in A) \land (t \neq u \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v)))$
36		simplrl	$⊢ ((((K \in HL \land P \in A \land t \in A) \land (u \in A \land v \in A \land w \in A) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land (P \neq t \land \neg P \underset{˙}{\leq} (t \underset{˙}{\lor} u))) \land P \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to P \neq t$
37		simplrr	$⊢ ((((K \in HL \land P \in A \land t \in A) \land (u \in A \land v \in A \land w \in A) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land (P \neq t \land \neg P \underset{˙}{\leq} (t \underset{˙}{\lor} u))) \land P \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to \neg P \underset{˙}{\leq} (t \underset{˙}{\lor} u)$
38		simpr	$⊢ ((((K \in HL \land P \in A \land t \in A) \land (u \in A \land v \in A \land w \in A) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land (P \neq t \land \neg P \underset{˙}{\leq} (t \underset{˙}{\lor} u))) \land P \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to P \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v)$
39	1 2 3	3dimlem3	$⊢ (((K \in HL \land P \in A \land t \in A) \land (u \in A \land v \in A) \land (t \neq u \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land (P \neq t \land \neg P \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land P \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \to (P \neq t \land \neg u \underset{˙}{\leq} (P \underset{˙}{\lor} t) \land \neg w \underset{˙}{\leq} ((P \underset{˙}{\lor} t) \underset{˙}{\lor} u))$
40	35 36 37 38 39	syl13anc	$⊢ ((((K \in HL \land P \in A \land t \in A) \land (u \in A \land v \in A \land w \in A) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land (P \neq t \land \neg P \underset{˙}{\leq} (t \underset{˙}{\lor} u))) \land P \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to (P \neq t \land \neg u \underset{˙}{\leq} (P \underset{˙}{\lor} t) \land \neg w \underset{˙}{\leq} ((P \underset{˙}{\lor} t) \underset{˙}{\lor} u))$
41	1 2 3	3dim1lem5	$⊢ ((t \in A \land u \in A \land w \in A) \land (P \neq t \land \neg u \underset{˙}{\leq} (P \underset{˙}{\lor} t) \land \neg w \underset{˙}{\leq} ((P \underset{˙}{\lor} t) \underset{˙}{\lor} u))) \to \exists q \in A \exists r \in A \exists s \in A (P \neq q \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} q) \underset{˙}{\lor} r))$
42	29 40 41	syl2anc	$⊢ ((((K \in HL \land P \in A \land t \in A) \land (u \in A \land v \in A \land w \in A) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land (P \neq t \land \neg P \underset{˙}{\leq} (t \underset{˙}{\lor} u))) \land P \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to \exists q \in A \exists r \in A \exists s \in A (P \neq q \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} q) \underset{˙}{\lor} r))$
43	11 17 12	3jca	$⊢ ((K \in HL \land P \in A \land t \in A) \land (u \in A \land v \in A \land w \in A) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \to (t \in A \land u \in A \land v \in A)$
44	43	ad2antrr	$⊢ ((((K \in HL \land P \in A \land t \in A) \land (u \in A \land v \in A \land w \in A) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land (P \neq t \land \neg P \underset{˙}{\leq} (t \underset{˙}{\lor} u))) \land \neg P \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to (t \in A \land u \in A \land v \in A)$
45		simpl1	$⊢ (((K \in HL \land P \in A \land t \in A) \land (u \in A \land v \in A \land w \in A) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land (P \neq t \land \neg P \underset{˙}{\leq} (t \underset{˙}{\lor} u))) \to (K \in HL \land P \in A \land t \in A)$
46		simpl21	$⊢ (((K \in HL \land P \in A \land t \in A) \land (u \in A \land v \in A \land w \in A) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land (P \neq t \land \neg P \underset{˙}{\leq} (t \underset{˙}{\lor} u))) \to u \in A$
47		simpl22	$⊢ (((K \in HL \land P \in A \land t \in A) \land (u \in A \land v \in A \land w \in A) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land (P \neq t \land \neg P \underset{˙}{\leq} (t \underset{˙}{\lor} u))) \to v \in A$
48	46 47	jca	$⊢ (((K \in HL \land P \in A \land t \in A) \land (u \in A \land v \in A \land w \in A) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land (P \neq t \land \neg P \underset{˙}{\leq} (t \underset{˙}{\lor} u))) \to (u \in A \land v \in A)$
49		simpl31	$⊢ (((K \in HL \land P \in A \land t \in A) \land (u \in A \land v \in A \land w \in A) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land (P \neq t \land \neg P \underset{˙}{\leq} (t \underset{˙}{\lor} u))) \to t \neq u$
50		simpl32	$⊢ (((K \in HL \land P \in A \land t \in A) \land (u \in A \land v \in A \land w \in A) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land (P \neq t \land \neg P \underset{˙}{\leq} (t \underset{˙}{\lor} u))) \to \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u)$
51	49 50	jca	$⊢ (((K \in HL \land P \in A \land t \in A) \land (u \in A \land v \in A \land w \in A) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land (P \neq t \land \neg P \underset{˙}{\leq} (t \underset{˙}{\lor} u))) \to (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u))$
52	45 48 51	3jca	$⊢ (((K \in HL \land P \in A \land t \in A) \land (u \in A \land v \in A \land w \in A) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land (P \neq t \land \neg P \underset{˙}{\leq} (t \underset{˙}{\lor} u))) \to ((K \in HL \land P \in A \land t \in A) \land (u \in A \land v \in A) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u)))$
53	52	adantr	$⊢ ((((K \in HL \land P \in A \land t \in A) \land (u \in A \land v \in A \land w \in A) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land (P \neq t \land \neg P \underset{˙}{\leq} (t \underset{˙}{\lor} u))) \land \neg P \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to ((K \in HL \land P \in A \land t \in A) \land (u \in A \land v \in A) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u)))$
54		simplr	$⊢ ((((K \in HL \land P \in A \land t \in A) \land (u \in A \land v \in A \land w \in A) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land (P \neq t \land \neg P \underset{˙}{\leq} (t \underset{˙}{\lor} u))) \land \neg P \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to (P \neq t \land \neg P \underset{˙}{\leq} (t \underset{˙}{\lor} u))$
55		simpr	$⊢ ((((K \in HL \land P \in A \land t \in A) \land (u \in A \land v \in A \land w \in A) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land (P \neq t \land \neg P \underset{˙}{\leq} (t \underset{˙}{\lor} u))) \land \neg P \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to \neg P \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v)$
56	1 2 3	3dimlem4	$⊢ (((K \in HL \land P \in A \land t \in A) \land (u \in A \land v \in A) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u))) \land (P \neq t \land \neg P \underset{˙}{\leq} (t \underset{˙}{\lor} u)) \land \neg P \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to (P \neq t \land \neg u \underset{˙}{\leq} (P \underset{˙}{\lor} t) \land \neg v \underset{˙}{\leq} ((P \underset{˙}{\lor} t) \underset{˙}{\lor} u))$
57	53 54 55 56	syl3anc	$⊢ ((((K \in HL \land P \in A \land t \in A) \land (u \in A \land v \in A \land w \in A) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land (P \neq t \land \neg P \underset{˙}{\leq} (t \underset{˙}{\lor} u))) \land \neg P \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to (P \neq t \land \neg u \underset{˙}{\leq} (P \underset{˙}{\lor} t) \land \neg v \underset{˙}{\leq} ((P \underset{˙}{\lor} t) \underset{˙}{\lor} u))$
58	1 2 3	3dim1lem5	$⊢ ((t \in A \land u \in A \land v \in A) \land (P \neq t \land \neg u \underset{˙}{\leq} (P \underset{˙}{\lor} t) \land \neg v \underset{˙}{\leq} ((P \underset{˙}{\lor} t) \underset{˙}{\lor} u))) \to \exists q \in A \exists r \in A \exists s \in A (P \neq q \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} q) \underset{˙}{\lor} r))$
59	44 57 58	syl2anc	$⊢ ((((K \in HL \land P \in A \land t \in A) \land (u \in A \land v \in A \land w \in A) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land (P \neq t \land \neg P \underset{˙}{\leq} (t \underset{˙}{\lor} u))) \land \neg P \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to \exists q \in A \exists r \in A \exists s \in A (P \neq q \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} q) \underset{˙}{\lor} r))$
60	42 59	pm2.61dan	$⊢ (((K \in HL \land P \in A \land t \in A) \land (u \in A \land v \in A \land w \in A) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land (P \neq t \land \neg P \underset{˙}{\leq} (t \underset{˙}{\lor} u))) \to \exists q \in A \exists r \in A \exists s \in A (P \neq q \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} q) \underset{˙}{\lor} r))$
61	60	anassrs	$⊢ ((((K \in HL \land P \in A \land t \in A) \land (u \in A \land v \in A \land w \in A) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land P \neq t) \land \neg P \underset{˙}{\leq} (t \underset{˙}{\lor} u)) \to \exists q \in A \exists r \in A \exists s \in A (P \neq q \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} q) \underset{˙}{\lor} r))$
62	27 61	pm2.61dan	$⊢ (((K \in HL \land P \in A \land t \in A) \land (u \in A \land v \in A \land w \in A) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \land P \neq t) \to \exists q \in A \exists r \in A \exists s \in A (P \neq q \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} q) \underset{˙}{\lor} r))$
63	10 62	pm2.61dane	$⊢ ((K \in HL \land P \in A \land t \in A) \land (u \in A \land v \in A \land w \in A) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v))) \to \exists q \in A \exists r \in A \exists s \in A (P \neq q \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} q) \underset{˙}{\lor} r))$
64	63	3exp	$⊢ (K \in HL \land P \in A \land t \in A) \to ((u \in A \land v \in A \land w \in A) \to ((t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to \exists q \in A \exists r \in A \exists s \in A (P \neq q \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} q) \underset{˙}{\lor} r))))$
65	64	3expd	$⊢ (K \in HL \land P \in A \land t \in A) \to (u \in A \to (v \in A \to (w \in A \to ((t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to \exists q \in A \exists r \in A \exists s \in A (P \neq q \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} q) \underset{˙}{\lor} r))))))$
66	65	3exp	$⊢ K \in HL \to (P \in A \to (t \in A \to (u \in A \to (v \in A \to (w \in A \to ((t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to \exists q \in A \exists r \in A \exists s \in A (P \neq q \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} q) \underset{˙}{\lor} r))))))))$
67	66	imp43	$⊢ ((K \in HL \land P \in A) \land (t \in A \land u \in A)) \to (v \in A \to (w \in A \to ((t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to \exists q \in A \exists r \in A \exists s \in A (P \neq q \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} q) \underset{˙}{\lor} r)))))$
68	67	impd	$⊢ ((K \in HL \land P \in A) \land (t \in A \land u \in A)) \to ((v \in A \land w \in A) \to ((t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to \exists q \in A \exists r \in A \exists s \in A (P \neq q \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} q) \underset{˙}{\lor} r))))$
69	68	rexlimdvv	$⊢ ((K \in HL \land P \in A) \land (t \in A \land u \in A)) \to (\exists v \in A \exists w \in A (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to \exists q \in A \exists r \in A \exists s \in A (P \neq q \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} q) \underset{˙}{\lor} r)))$
70	69	rexlimdvva	$⊢ (K \in HL \land P \in A) \to (\exists t \in A \exists u \in A \exists v \in A \exists w \in A (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land \neg w \underset{˙}{\leq} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to \exists q \in A \exists r \in A \exists s \in A (P \neq q \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} q) \underset{˙}{\lor} r)))$
71	5 70	mpd	$⊢ (K \in HL \land P \in A) \to \exists q \in A \exists r \in A \exists s \in A (P \neq q \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} q) \underset{˙}{\lor} r))$

Metamath Proof Explorer

Theorem 3dim1

Proof