lhpexle3lem

Description: There exists atom under a co-atom different from any three other atoms. TODO: study if adant*, simp* usage can be improved. (Contributed by NM, 9-Jul-2013)

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

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 Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X = Y) \to (K \in HL \land W \in H)$
5	1 2 3	lhpexle2	$⊢ (K \in HL \land W \in H) \to \exists p \in A (p \underset{˙}{\leq} W \land p \neq X \land p \neq Z)$
6	4 5	syl	$⊢ (((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X = Y) \to \exists p \in A (p \underset{˙}{\leq} W \land p \neq X \land p \neq Z)$
7		simp31	$⊢ ((((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X = Y) \land p \in A \land (p \underset{˙}{\leq} W \land p \neq X \land p \neq Z)) \to p \underset{˙}{\leq} W$
8		simp32	$⊢ ((((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X = Y) \land p \in A \land (p \underset{˙}{\leq} W \land p \neq X \land p \neq Z)) \to p \neq X$
9		simp1r	$⊢ ((((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X = Y) \land p \in A \land (p \underset{˙}{\leq} W \land p \neq X \land p \neq Z)) \to X = Y$
10	8 9	neeqtrd	$⊢ ((((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X = Y) \land p \in A \land (p \underset{˙}{\leq} W \land p \neq X \land p \neq Z)) \to p \neq Y$
11		simp33	$⊢ ((((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X = Y) \land p \in A \land (p \underset{˙}{\leq} W \land p \neq X \land p \neq Z)) \to p \neq Z$
12	8 10 11	3jca	$⊢ ((((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X = Y) \land p \in A \land (p \underset{˙}{\leq} W \land p \neq X \land p \neq Z)) \to (p \neq X \land p \neq Y \land p \neq Z)$
13	7 12	jca	$⊢ ((((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X = Y) \land p \in A \land (p \underset{˙}{\leq} W \land p \neq X \land p \neq Z)) \to (p \underset{˙}{\leq} W \land (p \neq X \land p \neq Y \land p \neq Z))$
14	13	3exp	$⊢ (((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X = Y) \to (p \in A \to ((p \underset{˙}{\leq} W \land p \neq X \land p \neq Z) \to (p \underset{˙}{\leq} W \land (p \neq X \land p \neq Y \land p \neq Z))))$
15	14	reximdvai	$⊢ (((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X = Y) \to (\exists p \in A (p \underset{˙}{\leq} W \land p \neq X \land p \neq Z) \to \exists p \in A (p \underset{˙}{\leq} W \land (p \neq X \land p \neq Y \land p \neq Z)))$
16	6 15	mpd	$⊢ (((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X = Y) \to \exists p \in A (p \underset{˙}{\leq} W \land (p \neq X \land p \neq Y \land p \neq Z))$
17		simprrr	$⊢ ((((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y \land Z \underset{˙}{\leq} (X join (K) Y)) \land (p \in A \land (\neg p \underset{˙}{\leq} (X join (K) Y) \land p \underset{˙}{\leq} W))) \to p \underset{˙}{\leq} W$
18		simp11l	$⊢ (((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y \land Z \underset{˙}{\leq} (X join (K) Y)) \to K \in HL$
19	18	adantr	$⊢ ((((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y \land Z \underset{˙}{\leq} (X join (K) Y)) \land (p \in A \land (\neg p \underset{˙}{\leq} (X join (K) Y) \land p \underset{˙}{\leq} W))) \to K \in HL$
20	19	hllatd	$⊢ ((((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y \land Z \underset{˙}{\leq} (X join (K) Y)) \land (p \in A \land (\neg p \underset{˙}{\leq} (X join (K) Y) \land p \underset{˙}{\leq} W))) \to K \in Lat$
21		eqid	$⊢ {Base}_{K} = {Base}_{K}$
22	21 2	atbase	$⊢ p \in A \to p \in {Base}_{K}$
23	22	ad2antrl	$⊢ ((((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y \land Z \underset{˙}{\leq} (X join (K) Y)) \land (p \in A \land (\neg p \underset{˙}{\leq} (X join (K) Y) \land p \underset{˙}{\leq} W))) \to p \in {Base}_{K}$
24		simp121	$⊢ (((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y \land Z \underset{˙}{\leq} (X join (K) Y)) \to X \in A$
25	24	adantr	$⊢ ((((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y \land Z \underset{˙}{\leq} (X join (K) Y)) \land (p \in A \land (\neg p \underset{˙}{\leq} (X join (K) Y) \land p \underset{˙}{\leq} W))) \to X \in A$
26	21 2	atbase	$⊢ X \in A \to X \in {Base}_{K}$
27	25 26	syl	$⊢ ((((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y \land Z \underset{˙}{\leq} (X join (K) Y)) \land (p \in A \land (\neg p \underset{˙}{\leq} (X join (K) Y) \land p \underset{˙}{\leq} W))) \to X \in {Base}_{K}$
28		simp122	$⊢ (((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y \land Z \underset{˙}{\leq} (X join (K) Y)) \to Y \in A$
29	28	adantr	$⊢ ((((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y \land Z \underset{˙}{\leq} (X join (K) Y)) \land (p \in A \land (\neg p \underset{˙}{\leq} (X join (K) Y) \land p \underset{˙}{\leq} W))) \to Y \in A$
30	21 2	atbase	$⊢ Y \in A \to Y \in {Base}_{K}$
31	29 30	syl	$⊢ ((((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y \land Z \underset{˙}{\leq} (X join (K) Y)) \land (p \in A \land (\neg p \underset{˙}{\leq} (X join (K) Y) \land p \underset{˙}{\leq} W))) \to Y \in {Base}_{K}$
32		simprrl	$⊢ ((((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y \land Z \underset{˙}{\leq} (X join (K) Y)) \land (p \in A \land (\neg p \underset{˙}{\leq} (X join (K) Y) \land p \underset{˙}{\leq} W))) \to \neg p \underset{˙}{\leq} (X join (K) Y)$
33		eqid	$⊢ join (K) = join (K)$
34	21 1 33	latnlej1l	$⊢ (K \in Lat \land (p \in {Base}_{K} \land X \in {Base}_{K} \land Y \in {Base}_{K}) \land \neg p \underset{˙}{\leq} (X join (K) Y)) \to p \neq X$
35	20 23 27 31 32 34	syl131anc	$⊢ ((((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y \land Z \underset{˙}{\leq} (X join (K) Y)) \land (p \in A \land (\neg p \underset{˙}{\leq} (X join (K) Y) \land p \underset{˙}{\leq} W))) \to p \neq X$
36	21 1 33	latnlej1r	$⊢ (K \in Lat \land (p \in {Base}_{K} \land X \in {Base}_{K} \land Y \in {Base}_{K}) \land \neg p \underset{˙}{\leq} (X join (K) Y)) \to p \neq Y$
37	20 23 27 31 32 36	syl131anc	$⊢ ((((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y \land Z \underset{˙}{\leq} (X join (K) Y)) \land (p \in A \land (\neg p \underset{˙}{\leq} (X join (K) Y) \land p \underset{˙}{\leq} W))) \to p \neq Y$
38		simpl3	$⊢ ((((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y \land Z \underset{˙}{\leq} (X join (K) Y)) \land (p \in A \land (\neg p \underset{˙}{\leq} (X join (K) Y) \land p \underset{˙}{\leq} W))) \to Z \underset{˙}{\leq} (X join (K) Y)$
39		nbrne2	$⊢ (Z \underset{˙}{\leq} (X join (K) Y) \land \neg p \underset{˙}{\leq} (X join (K) Y)) \to Z \neq p$
40	39	necomd	$⊢ (Z \underset{˙}{\leq} (X join (K) Y) \land \neg p \underset{˙}{\leq} (X join (K) Y)) \to p \neq Z$
41	38 32 40	syl2anc	$⊢ ((((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y \land Z \underset{˙}{\leq} (X join (K) Y)) \land (p \in A \land (\neg p \underset{˙}{\leq} (X join (K) Y) \land p \underset{˙}{\leq} W))) \to p \neq Z$
42	35 37 41	3jca	$⊢ ((((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y \land Z \underset{˙}{\leq} (X join (K) Y)) \land (p \in A \land (\neg p \underset{˙}{\leq} (X join (K) Y) \land p \underset{˙}{\leq} W))) \to (p \neq X \land p \neq Y \land p \neq Z)$
43	17 42	jca	$⊢ ((((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y \land Z \underset{˙}{\leq} (X join (K) Y)) \land (p \in A \land (\neg p \underset{˙}{\leq} (X join (K) Y) \land p \underset{˙}{\leq} W))) \to (p \underset{˙}{\leq} W \land (p \neq X \land p \neq Y \land p \neq Z))$
44		simp11	$⊢ (((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y \land Z \underset{˙}{\leq} (X join (K) Y)) \to (K \in HL \land W \in H)$
45		simp131	$⊢ (((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y \land Z \underset{˙}{\leq} (X join (K) Y)) \to X \underset{˙}{\leq} W$
46		simp132	$⊢ (((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y \land Z \underset{˙}{\leq} (X join (K) Y)) \to Y \underset{˙}{\leq} W$
47		eqid	$⊢ <_{K} = <_{K}$
48	1 47 33 2 3	lhp2lt	$⊢ ((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 join (K) Y) <_{K} W$
49	44 24 45 28 46 48	syl122anc	$⊢ (((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y \land Z \underset{˙}{\leq} (X join (K) Y)) \to (X join (K) Y) <_{K} W$
50	21 33 2	hlatjcl	$⊢ (K \in HL \land X \in A \land Y \in A) \to X join (K) Y \in {Base}_{K}$
51	18 24 28 50	syl3anc	$⊢ (((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y \land Z \underset{˙}{\leq} (X join (K) Y)) \to X join (K) Y \in {Base}_{K}$
52		simp11r	$⊢ (((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y \land Z \underset{˙}{\leq} (X join (K) Y)) \to W \in H$
53	21 3	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
54	52 53	syl	$⊢ (((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y \land Z \underset{˙}{\leq} (X join (K) Y)) \to W \in {Base}_{K}$
55	21 1 47 2	hlrelat1	$⊢ (K \in HL \land X join (K) Y \in {Base}_{K} \land W \in {Base}_{K}) \to ((X join (K) Y) <_{K} W \to \exists p \in A (\neg p \underset{˙}{\leq} (X join (K) Y) \land p \underset{˙}{\leq} W))$
56	18 51 54 55	syl3anc	$⊢ (((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y \land Z \underset{˙}{\leq} (X join (K) Y)) \to ((X join (K) Y) <_{K} W \to \exists p \in A (\neg p \underset{˙}{\leq} (X join (K) Y) \land p \underset{˙}{\leq} W))$
57	49 56	mpd	$⊢ (((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y \land Z \underset{˙}{\leq} (X join (K) Y)) \to \exists p \in A (\neg p \underset{˙}{\leq} (X join (K) Y) \land p \underset{˙}{\leq} W)$
58	43 57	reximddv	$⊢ (((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y \land Z \underset{˙}{\leq} (X join (K) Y)) \to \exists p \in A (p \underset{˙}{\leq} W \land (p \neq X \land p \neq Y \land p \neq Z))$
59	58	3expa	$⊢ ((((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y) \land Z \underset{˙}{\leq} (X join (K) Y)) \to \exists p \in A (p \underset{˙}{\leq} W \land (p \neq X \land p \neq Y \land p \neq Z))$
60		simp11l	$⊢ (((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y \land \neg Z \underset{˙}{\leq} (X join (K) Y)) \to K \in HL$
61	60	adantr	$⊢ ((((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y \land \neg Z \underset{˙}{\leq} (X join (K) 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$
62	61	hllatd	$⊢ ((((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y \land \neg Z \underset{˙}{\leq} (X join (K) 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$
63	22	ad2antrl	$⊢ ((((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y \land \neg Z \underset{˙}{\leq} (X join (K) 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}$
64		simp121	$⊢ (((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y \land \neg Z \underset{˙}{\leq} (X join (K) Y)) \to X \in A$
65	64	adantr	$⊢ ((((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y \land \neg Z \underset{˙}{\leq} (X join (K) 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$
66		simp122	$⊢ (((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y \land \neg Z \underset{˙}{\leq} (X join (K) Y)) \to Y \in A$
67	66	adantr	$⊢ ((((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y \land \neg Z \underset{˙}{\leq} (X join (K) 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$
68	61 65 67 50	syl3anc	$⊢ ((((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y \land \neg Z \underset{˙}{\leq} (X join (K) 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}$
69		simp11r	$⊢ (((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y \land \neg Z \underset{˙}{\leq} (X join (K) Y)) \to W \in H$
70	69	adantr	$⊢ ((((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y \land \neg Z \underset{˙}{\leq} (X join (K) 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$
71	70 53	syl	$⊢ ((((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y \land \neg Z \underset{˙}{\leq} (X join (K) 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}$
72		simprr3	$⊢ ((((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y \land \neg Z \underset{˙}{\leq} (X join (K) 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)$
73		simp131	$⊢ (((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y \land \neg Z \underset{˙}{\leq} (X join (K) Y)) \to X \underset{˙}{\leq} W$
74	73	adantr	$⊢ ((((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y \land \neg Z \underset{˙}{\leq} (X join (K) 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$
75		simp132	$⊢ (((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y \land \neg Z \underset{˙}{\leq} (X join (K) Y)) \to Y \underset{˙}{\leq} W$
76	75	adantr	$⊢ ((((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y \land \neg Z \underset{˙}{\leq} (X join (K) 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$
77	65 26	syl	$⊢ ((((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y \land \neg Z \underset{˙}{\leq} (X join (K) 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}$
78	67 30	syl	$⊢ ((((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y \land \neg Z \underset{˙}{\leq} (X join (K) 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}$
79	21 1 33	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)$
80	62 77 78 71 79	syl13anc	$⊢ ((((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y \land \neg Z \underset{˙}{\leq} (X join (K) 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)$
81	74 76 80	mpbi2and	$⊢ ((((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y \land \neg Z \underset{˙}{\leq} (X join (K) 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$
82	21 1 62 63 68 71 72 81	lattrd	$⊢ ((((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y \land \neg Z \underset{˙}{\leq} (X join (K) 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$
83		simprr1	$⊢ ((((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y \land \neg Z \underset{˙}{\leq} (X join (K) 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$
84		simprr2	$⊢ ((((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y \land \neg Z \underset{˙}{\leq} (X join (K) 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$
85		simpl3	$⊢ ((((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y \land \neg Z \underset{˙}{\leq} (X join (K) Y)) \land (p \in A \land (p \neq X \land p \neq Y \land p \underset{˙}{\leq} (X join (K) Y)))) \to \neg Z \underset{˙}{\leq} (X join (K) Y)$
86		nbrne2	$⊢ (p \underset{˙}{\leq} (X join (K) Y) \land \neg Z \underset{˙}{\leq} (X join (K) Y)) \to p \neq Z$
87	72 85 86	syl2anc	$⊢ ((((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y \land \neg Z \underset{˙}{\leq} (X join (K) Y)) \land (p \in A \land (p \neq X \land p \neq Y \land p \underset{˙}{\leq} (X join (K) Y)))) \to p \neq Z$
88	83 84 87	3jca	$⊢ ((((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y \land \neg Z \underset{˙}{\leq} (X join (K) 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 \land p \neq Y \land p \neq Z)$
89	82 88	jca	$⊢ ((((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y \land \neg Z \underset{˙}{\leq} (X join (K) 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 \land p \neq Z))$
90		simp2	$⊢ (((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y \land \neg Z \underset{˙}{\leq} (X join (K) Y)) \to X \neq Y$
91	1 33 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))$
92	60 64 66 90 91	syl31anc	$⊢ (((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y \land \neg Z \underset{˙}{\leq} (X join (K) Y)) \to \exists p \in A (p \neq X \land p \neq Y \land p \underset{˙}{\leq} (X join (K) Y))$
93	89 92	reximddv	$⊢ (((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y \land \neg Z \underset{˙}{\leq} (X join (K) Y)) \to \exists p \in A (p \underset{˙}{\leq} W \land (p \neq X \land p \neq Y \land p \neq Z))$
94	93	3expa	$⊢ ((((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y) \land \neg Z \underset{˙}{\leq} (X join (K) Y)) \to \exists p \in A (p \underset{˙}{\leq} W \land (p \neq X \land p \neq Y \land p \neq Z))$
95	59 94	pm2.61dan	$⊢ (((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \land X \neq Y) \to \exists p \in A (p \underset{˙}{\leq} W \land (p \neq X \land p \neq Y \land p \neq Z))$
96	16 95	pm2.61dane	$⊢ ((K \in HL \land W \in H) \land (X \in A \land Y \in A \land Z \in A) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W)) \to \exists p \in A (p \underset{˙}{\leq} W \land (p \neq X \land p \neq Y \land p \neq Z))$

Metamath Proof Explorer

Theorem lhpexle3lem

Proof