lhpexle2lem

	Ref	Expression
Hypotheses	lhpex1.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	lhpex1.a	$⊢ A = Atoms (K)$
	lhpex1.h	$⊢ H = LHyp (K)$
Assertion	lhpexle2lem	$⊢ ((K \in HL \land W \in H) \land (X \in A \land X \underset{˙}{\leq} W) \land (Y \in A \land Y \underset{˙}{\leq} W)) \to \exists p \in A (p \underset{˙}{\leq} W \land p \neq X \land p \neq Y)$

Proof

Step	Hyp	Ref	Expression
1		lhpex1.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		lhpex1.a	$⊢ A = Atoms (K)$
3		lhpex1.h	$⊢ H = LHyp (K)$
4		simpl1	$⊢ (((K \in HL \land W \in H) \land (X \in A \land X \underset{˙}{\leq} W) \land (Y \in A \land Y \underset{˙}{\leq} W)) \land X = Y) \to (K \in HL \land W \in H)$
5	1 2 3	lhpexle1	$⊢ (K \in HL \land W \in H) \to \exists p \in A (p \underset{˙}{\leq} W \land p \neq X)$
6	4 5	syl	$⊢ (((K \in HL \land W \in H) \land (X \in A \land X \underset{˙}{\leq} W) \land (Y \in A \land Y \underset{˙}{\leq} W)) \land X = Y) \to \exists p \in A (p \underset{˙}{\leq} W \land p \neq X)$
7		simp3l	$⊢ (((K \in HL \land W \in H) \land (X \in A \land X \underset{˙}{\leq} W) \land (Y \in A \land Y \underset{˙}{\leq} W)) \land X = Y \land (p \underset{˙}{\leq} W \land p \neq X)) \to p \underset{˙}{\leq} W$
8		simp3r	$⊢ (((K \in HL \land W \in H) \land (X \in A \land X \underset{˙}{\leq} W) \land (Y \in A \land Y \underset{˙}{\leq} W)) \land X = Y \land (p \underset{˙}{\leq} W \land p \neq X)) \to p \neq X$
9		simp2	$⊢ (((K \in HL \land W \in H) \land (X \in A \land X \underset{˙}{\leq} W) \land (Y \in A \land Y \underset{˙}{\leq} W)) \land X = Y \land (p \underset{˙}{\leq} W \land p \neq X)) \to X = Y$
10	8 9	neeqtrd	$⊢ (((K \in HL \land W \in H) \land (X \in A \land X \underset{˙}{\leq} W) \land (Y \in A \land Y \underset{˙}{\leq} W)) \land X = Y \land (p \underset{˙}{\leq} W \land p \neq X)) \to p \neq Y$
11	7 8 10	3jca	$⊢ (((K \in HL \land W \in H) \land (X \in A \land X \underset{˙}{\leq} W) \land (Y \in A \land Y \underset{˙}{\leq} W)) \land X = Y \land (p \underset{˙}{\leq} W \land p \neq X)) \to (p \underset{˙}{\leq} W \land p \neq X \land p \neq Y)$
12	11	3expia	$⊢ (((K \in HL \land W \in H) \land (X \in A \land X \underset{˙}{\leq} W) \land (Y \in A \land Y \underset{˙}{\leq} W)) \land X = Y) \to ((p \underset{˙}{\leq} W \land p \neq X) \to (p \underset{˙}{\leq} W \land p \neq X \land p \neq Y))$
13	12	reximdv	$⊢ (((K \in HL \land W \in H) \land (X \in A \land X \underset{˙}{\leq} W) \land (Y \in A \land Y \underset{˙}{\leq} W)) \land X = Y) \to (\exists p \in A (p \underset{˙}{\leq} W \land p \neq X) \to \exists p \in A (p \underset{˙}{\leq} W \land p \neq X \land p \neq Y))$
14	6 13	mpd	$⊢ (((K \in HL \land W \in H) \land (X \in A \land X \underset{˙}{\leq} W) \land (Y \in A \land Y \underset{˙}{\leq} W)) \land X = Y) \to \exists p \in A (p \underset{˙}{\leq} W \land p \neq X \land p \neq Y)$
15		simpl1l	$⊢ (((K \in HL \land W \in H) \land (X \in A \land X \underset{˙}{\leq} W) \land (Y \in A \land Y \underset{˙}{\leq} W)) \land X \neq Y) \to K \in HL$
16		simpl2l	$⊢ (((K \in HL \land W \in H) \land (X \in A \land X \underset{˙}{\leq} W) \land (Y \in A \land Y \underset{˙}{\leq} W)) \land X \neq Y) \to X \in A$
17		simpl3l	$⊢ (((K \in HL \land W \in H) \land (X \in A \land X \underset{˙}{\leq} W) \land (Y \in A \land Y \underset{˙}{\leq} W)) \land X \neq Y) \to Y \in A$
18		simpr	$⊢ (((K \in HL \land W \in H) \land (X \in A \land X \underset{˙}{\leq} W) \land (Y \in A \land Y \underset{˙}{\leq} W)) \land X \neq Y) \to X \neq Y$
19		eqid	$⊢ join (K) = join (K)$
20	1 19 2	hlsupr	$⊢ ((K \in HL \land X \in A \land Y \in A) \land X \neq Y) \to \exists p \in A (p \neq X \land p \neq Y \land p \underset{˙}{\leq} (X join (K) Y))$
21	15 16 17 18 20	syl31anc	$⊢ (((K \in HL \land W \in H) \land (X \in A \land X \underset{˙}{\leq} W) \land (Y \in A \land Y \underset{˙}{\leq} W)) \land X \neq Y) \to \exists p \in A (p \neq X \land p \neq Y \land p \underset{˙}{\leq} (X join (K) Y))$
22		eqid	$⊢ {Base}_{K} = {Base}_{K}$
23		simpl1l	$⊢ (((K \in HL \land W \in H) \land (X \in A \land X \underset{˙}{\leq} W) \land (Y \in A \land Y \underset{˙}{\leq} W)) \land ((X \neq Y \land p \in A) \land (p \neq X \land p \neq Y \land p \underset{˙}{\leq} (X join (K) Y)))) \to K \in HL$
24	23	hllatd	$⊢ (((K \in HL \land W \in H) \land (X \in A \land X \underset{˙}{\leq} W) \land (Y \in A \land Y \underset{˙}{\leq} W)) \land ((X \neq Y \land p \in A) \land (p \neq X \land p \neq Y \land p \underset{˙}{\leq} (X join (K) Y)))) \to K \in Lat$
25		simprlr	$⊢ (((K \in HL \land W \in H) \land (X \in A \land X \underset{˙}{\leq} W) \land (Y \in A \land Y \underset{˙}{\leq} W)) \land ((X \neq Y \land p \in A) \land (p \neq X \land p \neq Y \land p \underset{˙}{\leq} (X join (K) Y)))) \to p \in A$
26	22 2	atbase	$⊢ p \in A \to p \in {Base}_{K}$
27	25 26	syl	$⊢ (((K \in HL \land W \in H) \land (X \in A \land X \underset{˙}{\leq} W) \land (Y \in A \land Y \underset{˙}{\leq} W)) \land ((X \neq Y \land p \in A) \land (p \neq X \land p \neq Y \land p \underset{˙}{\leq} (X join (K) Y)))) \to p \in {Base}_{K}$
28		simpl2l	$⊢ (((K \in HL \land W \in H) \land (X \in A \land X \underset{˙}{\leq} W) \land (Y \in A \land Y \underset{˙}{\leq} W)) \land ((X \neq Y \land p \in A) \land (p \neq X \land p \neq Y \land p \underset{˙}{\leq} (X join (K) Y)))) \to X \in A$
29		simpl3l	$⊢ (((K \in HL \land W \in H) \land (X \in A \land X \underset{˙}{\leq} W) \land (Y \in A \land Y \underset{˙}{\leq} W)) \land ((X \neq Y \land p \in A) \land (p \neq X \land p \neq Y \land p \underset{˙}{\leq} (X join (K) Y)))) \to Y \in A$
30	22 19 2	hlatjcl	$⊢ (K \in HL \land X \in A \land Y \in A) \to X join (K) Y \in {Base}_{K}$
31	23 28 29 30	syl3anc	$⊢ (((K \in HL \land W \in H) \land (X \in A \land X \underset{˙}{\leq} W) \land (Y \in A \land Y \underset{˙}{\leq} W)) \land ((X \neq Y \land p \in A) \land (p \neq X \land p \neq Y \land p \underset{˙}{\leq} (X join (K) Y)))) \to X join (K) Y \in {Base}_{K}$
32		simpl1r	$⊢ (((K \in HL \land W \in H) \land (X \in A \land X \underset{˙}{\leq} W) \land (Y \in A \land Y \underset{˙}{\leq} W)) \land ((X \neq Y \land p \in A) \land (p \neq X \land p \neq Y \land p \underset{˙}{\leq} (X join (K) Y)))) \to W \in H$
33	22 3	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
34	32 33	syl	$⊢ (((K \in HL \land W \in H) \land (X \in A \land X \underset{˙}{\leq} W) \land (Y \in A \land Y \underset{˙}{\leq} W)) \land ((X \neq Y \land p \in A) \land (p \neq X \land p \neq Y \land p \underset{˙}{\leq} (X join (K) Y)))) \to W \in {Base}_{K}$
35		simprr3	$⊢ (((K \in HL \land W \in H) \land (X \in A \land X \underset{˙}{\leq} W) \land (Y \in A \land Y \underset{˙}{\leq} W)) \land ((X \neq Y \land p \in A) \land (p \neq X \land p \neq Y \land p \underset{˙}{\leq} (X join (K) Y)))) \to p \underset{˙}{\leq} (X join (K) Y)$
36		simpl2r	$⊢ (((K \in HL \land W \in H) \land (X \in A \land X \underset{˙}{\leq} W) \land (Y \in A \land Y \underset{˙}{\leq} W)) \land ((X \neq Y \land p \in A) \land (p \neq X \land p \neq Y \land p \underset{˙}{\leq} (X join (K) Y)))) \to X \underset{˙}{\leq} W$
37		simpl3r	$⊢ (((K \in HL \land W \in H) \land (X \in A \land X \underset{˙}{\leq} W) \land (Y \in A \land Y \underset{˙}{\leq} W)) \land ((X \neq Y \land p \in A) \land (p \neq X \land p \neq Y \land p \underset{˙}{\leq} (X join (K) Y)))) \to Y \underset{˙}{\leq} W$
38	22 2	atbase	$⊢ X \in A \to X \in {Base}_{K}$
39	28 38	syl	$⊢ (((K \in HL \land W \in H) \land (X \in A \land X \underset{˙}{\leq} W) \land (Y \in A \land Y \underset{˙}{\leq} W)) \land ((X \neq Y \land p \in A) \land (p \neq X \land p \neq Y \land p \underset{˙}{\leq} (X join (K) Y)))) \to X \in {Base}_{K}$
40	22 2	atbase	$⊢ Y \in A \to Y \in {Base}_{K}$
41	29 40	syl	$⊢ (((K \in HL \land W \in H) \land (X \in A \land X \underset{˙}{\leq} W) \land (Y \in A \land Y \underset{˙}{\leq} W)) \land ((X \neq Y \land p \in A) \land (p \neq X \land p \neq Y \land p \underset{˙}{\leq} (X join (K) Y)))) \to Y \in {Base}_{K}$
42	22 1 19	latjle12	$⊢ (K \in Lat \land (X \in {Base}_{K} \land Y \in {Base}_{K} \land W \in {Base}_{K})) \to ((X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W) \leftrightarrow (X join (K) Y) \underset{˙}{\leq} W)$
43	24 39 41 34 42	syl13anc	$⊢ (((K \in HL \land W \in H) \land (X \in A \land X \underset{˙}{\leq} W) \land (Y \in A \land Y \underset{˙}{\leq} W)) \land ((X \neq Y \land p \in A) \land (p \neq X \land p \neq Y \land p \underset{˙}{\leq} (X join (K) Y)))) \to ((X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W) \leftrightarrow (X join (K) Y) \underset{˙}{\leq} W)$
44	36 37 43	mpbi2and	$⊢ (((K \in HL \land W \in H) \land (X \in A \land X \underset{˙}{\leq} W) \land (Y \in A \land Y \underset{˙}{\leq} W)) \land ((X \neq Y \land p \in A) \land (p \neq X \land p \neq Y \land p \underset{˙}{\leq} (X join (K) Y)))) \to (X join (K) Y) \underset{˙}{\leq} W$
45	22 1 24 27 31 34 35 44	lattrd	$⊢ (((K \in HL \land W \in H) \land (X \in A \land X \underset{˙}{\leq} W) \land (Y \in A \land Y \underset{˙}{\leq} W)) \land ((X \neq Y \land p \in A) \land (p \neq X \land p \neq Y \land p \underset{˙}{\leq} (X join (K) Y)))) \to p \underset{˙}{\leq} W$
46		simprr1	$⊢ (((K \in HL \land W \in H) \land (X \in A \land X \underset{˙}{\leq} W) \land (Y \in A \land Y \underset{˙}{\leq} W)) \land ((X \neq Y \land p \in A) \land (p \neq X \land p \neq Y \land p \underset{˙}{\leq} (X join (K) Y)))) \to p \neq X$
47		simprr2	$⊢ (((K \in HL \land W \in H) \land (X \in A \land X \underset{˙}{\leq} W) \land (Y \in A \land Y \underset{˙}{\leq} W)) \land ((X \neq Y \land p \in A) \land (p \neq X \land p \neq Y \land p \underset{˙}{\leq} (X join (K) Y)))) \to p \neq Y$
48	45 46 47	3jca	$⊢ (((K \in HL \land W \in H) \land (X \in A \land X \underset{˙}{\leq} W) \land (Y \in A \land Y \underset{˙}{\leq} W)) \land ((X \neq Y \land p \in A) \land (p \neq X \land p \neq Y \land p \underset{˙}{\leq} (X join (K) Y)))) \to (p \underset{˙}{\leq} W \land p \neq X \land p \neq Y)$
49	48	exp44	$⊢ ((K \in HL \land W \in H) \land (X \in A \land X \underset{˙}{\leq} W) \land (Y \in A \land Y \underset{˙}{\leq} W)) \to (X \neq Y \to (p \in A \to ((p \neq X \land p \neq Y \land p \underset{˙}{\leq} (X join (K) Y)) \to (p \underset{˙}{\leq} W \land p \neq X \land p \neq Y))))$
50	49	imp31	$⊢ ((((K \in HL \land W \in H) \land (X \in A \land X \underset{˙}{\leq} W) \land (Y \in A \land Y \underset{˙}{\leq} W)) \land X \neq Y) \land p \in A) \to ((p \neq X \land p \neq Y \land p \underset{˙}{\leq} (X join (K) Y)) \to (p \underset{˙}{\leq} W \land p \neq X \land p \neq Y))$
51	50	reximdva	$⊢ (((K \in HL \land W \in H) \land (X \in A \land X \underset{˙}{\leq} W) \land (Y \in A \land Y \underset{˙}{\leq} W)) \land X \neq Y) \to (\exists p \in A (p \neq X \land p \neq Y \land p \underset{˙}{\leq} (X join (K) Y)) \to \exists p \in A (p \underset{˙}{\leq} W \land p \neq X \land p \neq Y))$
52	21 51	mpd	$⊢ (((K \in HL \land W \in H) \land (X \in A \land X \underset{˙}{\leq} W) \land (Y \in A \land Y \underset{˙}{\leq} W)) \land X \neq Y) \to \exists p \in A (p \underset{˙}{\leq} W \land p \neq X \land p \neq Y)$
53	14 52	pm2.61dane	$⊢ ((K \in HL \land W \in H) \land (X \in A \land X \underset{˙}{\leq} W) \land (Y \in A \land Y \underset{˙}{\leq} W)) \to \exists p \in A (p \underset{˙}{\leq} W \land p \neq X \land p \neq Y)$

Metamath Proof Explorer

Theorem lhpexle2lem

Proof