lhpexle3

Description: There exists atom under a co-atom different from any three other elements. (Contributed by NM, 24-Jul-2013)

	Ref	Expression
Hypotheses	lhpex1.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	lhpex1.a	$⊢ A = Atoms (K)$
	lhpex1.h	$⊢ H = LHyp (K)$
Assertion	lhpexle3	$⊢ (K \in HL \land W \in H) \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	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 Y)$
5		3anass	$⊢ (p \underset{˙}{\leq} W \land p \neq X \land p \neq Y) \leftrightarrow (p \underset{˙}{\leq} W \land (p \neq X \land p \neq Y))$
6	5	rexbii	$⊢ \exists p \in A (p \underset{˙}{\leq} W \land p \neq X \land p \neq Y) \leftrightarrow \exists p \in A (p \underset{˙}{\leq} W \land (p \neq X \land p \neq Y))$
7	4 6	sylib	$⊢ (K \in HL \land W \in H) \to \exists p \in A (p \underset{˙}{\leq} W \land (p \neq X \land p \neq Y))$
8	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)$
9	8	adantr	$⊢ ((K \in HL \land W \in H) \land (Z \in A \land Z \underset{˙}{\leq} W)) \to \exists p \in A (p \underset{˙}{\leq} W \land p \neq X \land p \neq Z)$
10		3anass	$⊢ (p \underset{˙}{\leq} W \land p \neq X \land p \neq Z) \leftrightarrow (p \underset{˙}{\leq} W \land (p \neq X \land p \neq Z))$
11	10	rexbii	$⊢ \exists p \in A (p \underset{˙}{\leq} W \land p \neq X \land p \neq Z) \leftrightarrow \exists p \in A (p \underset{˙}{\leq} W \land (p \neq X \land p \neq Z))$
12	9 11	sylib	$⊢ ((K \in HL \land W \in H) \land (Z \in A \land Z \underset{˙}{\leq} W)) \to \exists p \in A (p \underset{˙}{\leq} W \land (p \neq X \land p \neq Z))$
13	1 2 3	lhpexle2	$⊢ (K \in HL \land W \in H) \to \exists p \in A (p \underset{˙}{\leq} W \land p \neq Y \land p \neq Z)$
14		3anass	$⊢ (p \underset{˙}{\leq} W \land p \neq Y \land p \neq Z) \leftrightarrow (p \underset{˙}{\leq} W \land (p \neq Y \land p \neq Z))$
15	14	rexbii	$⊢ \exists p \in A (p \underset{˙}{\leq} W \land p \neq Y \land p \neq Z) \leftrightarrow \exists p \in A (p \underset{˙}{\leq} W \land (p \neq Y \land p \neq Z))$
16	13 15	sylib	$⊢ (K \in HL \land W \in H) \to \exists p \in A (p \underset{˙}{\leq} W \land (p \neq Y \land p \neq Z))$
17	16	3ad2ant1	$⊢ ((K \in HL \land W \in H) \land (Z \in A \land Z \underset{˙}{\leq} W) \land (Y \in A \land Y \underset{˙}{\leq} W)) \to \exists p \in A (p \underset{˙}{\leq} W \land (p \neq Y \land p \neq Z))$
18		simpl1	$⊢ (((K \in HL \land W \in H) \land (Z \in A \land Z \underset{˙}{\leq} W) \land (Y \in A \land Y \underset{˙}{\leq} W)) \land (X \in A \land X \underset{˙}{\leq} W)) \to (K \in HL \land W \in H)$
19		simpl3l	$⊢ (((K \in HL \land W \in H) \land (Z \in A \land Z \underset{˙}{\leq} W) \land (Y \in A \land Y \underset{˙}{\leq} W)) \land (X \in A \land X \underset{˙}{\leq} W)) \to Y \in A$
20		simpl2l	$⊢ (((K \in HL \land W \in H) \land (Z \in A \land Z \underset{˙}{\leq} W) \land (Y \in A \land Y \underset{˙}{\leq} W)) \land (X \in A \land X \underset{˙}{\leq} W)) \to Z \in A$
21		simprl	$⊢ (((K \in HL \land W \in H) \land (Z \in A \land Z \underset{˙}{\leq} W) \land (Y \in A \land Y \underset{˙}{\leq} W)) \land (X \in A \land X \underset{˙}{\leq} W)) \to X \in A$
22		simpl3r	$⊢ (((K \in HL \land W \in H) \land (Z \in A \land Z \underset{˙}{\leq} W) \land (Y \in A \land Y \underset{˙}{\leq} W)) \land (X \in A \land X \underset{˙}{\leq} W)) \to Y \underset{˙}{\leq} W$
23		simpl2r	$⊢ (((K \in HL \land W \in H) \land (Z \in A \land Z \underset{˙}{\leq} W) \land (Y \in A \land Y \underset{˙}{\leq} W)) \land (X \in A \land X \underset{˙}{\leq} W)) \to Z \underset{˙}{\leq} W$
24		simprr	$⊢ (((K \in HL \land W \in H) \land (Z \in A \land Z \underset{˙}{\leq} W) \land (Y \in A \land Y \underset{˙}{\leq} W)) \land (X \in A \land X \underset{˙}{\leq} W)) \to X \underset{˙}{\leq} W$
25	1 2 3	lhpexle3lem	$⊢ ((K \in HL \land W \in H) \land (Y \in A \land Z \in A \land X \in A) \land (Y \underset{˙}{\leq} W \land Z \underset{˙}{\leq} W \land X \underset{˙}{\leq} W)) \to \exists p \in A (p \underset{˙}{\leq} W \land (p \neq Y \land p \neq Z \land p \neq X))$
26	18 19 20 21 22 23 24 25	syl133anc	$⊢ (((K \in HL \land W \in H) \land (Z \in A \land Z \underset{˙}{\leq} W) \land (Y \in A \land Y \underset{˙}{\leq} W)) \land (X \in A \land X \underset{˙}{\leq} W)) \to \exists p \in A (p \underset{˙}{\leq} W \land (p \neq Y \land p \neq Z \land p \neq X))$
27		df-3an	$⊢ (p \neq Y \land p \neq Z \land p \neq X) \leftrightarrow ((p \neq Y \land p \neq Z) \land p \neq X)$
28	27	anbi2i	$⊢ (p \underset{˙}{\leq} W \land (p \neq Y \land p \neq Z \land p \neq X)) \leftrightarrow (p \underset{˙}{\leq} W \land ((p \neq Y \land p \neq Z) \land p \neq X))$
29		3anass	$⊢ (p \underset{˙}{\leq} W \land (p \neq Y \land p \neq Z) \land p \neq X) \leftrightarrow (p \underset{˙}{\leq} W \land ((p \neq Y \land p \neq Z) \land p \neq X))$
30	28 29	bitr4i	$⊢ (p \underset{˙}{\leq} W \land (p \neq Y \land p \neq Z \land p \neq X)) \leftrightarrow (p \underset{˙}{\leq} W \land (p \neq Y \land p \neq Z) \land p \neq X)$
31	30	rexbii	$⊢ \exists p \in A (p \underset{˙}{\leq} W \land (p \neq Y \land p \neq Z \land p \neq X)) \leftrightarrow \exists p \in A (p \underset{˙}{\leq} W \land (p \neq Y \land p \neq Z) \land p \neq X)$
32	26 31	sylib	$⊢ (((K \in HL \land W \in H) \land (Z \in A \land Z \underset{˙}{\leq} W) \land (Y \in A \land Y \underset{˙}{\leq} W)) \land (X \in A \land X \underset{˙}{\leq} W)) \to \exists p \in A (p \underset{˙}{\leq} W \land (p \neq Y \land p \neq Z) \land p \neq X)$
33	17 32	lhpexle1lem	$⊢ ((K \in HL \land W \in H) \land (Z \in A \land Z \underset{˙}{\leq} W) \land (Y \in A \land Y \underset{˙}{\leq} W)) \to \exists p \in A (p \underset{˙}{\leq} W \land (p \neq Y \land p \neq Z) \land p \neq X)$
34		an31	$⊢ ((p \neq Y \land p \neq Z) \land p \neq X) \leftrightarrow ((p \neq X \land p \neq Z) \land p \neq Y)$
35	34	anbi2i	$⊢ (p \underset{˙}{\leq} W \land ((p \neq Y \land p \neq Z) \land p \neq X)) \leftrightarrow (p \underset{˙}{\leq} W \land ((p \neq X \land p \neq Z) \land p \neq Y))$
36		3anass	$⊢ (p \underset{˙}{\leq} W \land (p \neq X \land p \neq Z) \land p \neq Y) \leftrightarrow (p \underset{˙}{\leq} W \land ((p \neq X \land p \neq Z) \land p \neq Y))$
37	35 29 36	3bitr4i	$⊢ (p \underset{˙}{\leq} W \land (p \neq Y \land p \neq Z) \land p \neq X) \leftrightarrow (p \underset{˙}{\leq} W \land (p \neq X \land p \neq Z) \land p \neq Y)$
38	37	rexbii	$⊢ \exists p \in A (p \underset{˙}{\leq} W \land (p \neq Y \land p \neq Z) \land p \neq X) \leftrightarrow \exists p \in A (p \underset{˙}{\leq} W \land (p \neq X \land p \neq Z) \land p \neq Y)$
39	33 38	sylib	$⊢ ((K \in HL \land W \in H) \land (Z \in A \land Z \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 Z) \land p \neq Y)$
40	39	3expa	$⊢ (((K \in HL \land W \in H) \land (Z \in A \land Z \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 Z) \land p \neq Y)$
41	12 40	lhpexle1lem	$⊢ ((K \in HL \land W \in H) \land (Z \in A \land Z \underset{˙}{\leq} W)) \to \exists p \in A (p \underset{˙}{\leq} W \land (p \neq X \land p \neq Z) \land p \neq Y)$
42		an32	$⊢ ((p \neq X \land p \neq Z) \land p \neq Y) \leftrightarrow ((p \neq X \land p \neq Y) \land p \neq Z)$
43	42	anbi2i	$⊢ (p \underset{˙}{\leq} W \land ((p \neq X \land p \neq Z) \land p \neq Y)) \leftrightarrow (p \underset{˙}{\leq} W \land ((p \neq X \land p \neq Y) \land p \neq Z))$
44		3anass	$⊢ (p \underset{˙}{\leq} W \land (p \neq X \land p \neq Y) \land p \neq Z) \leftrightarrow (p \underset{˙}{\leq} W \land ((p \neq X \land p \neq Y) \land p \neq Z))$
45	43 36 44	3bitr4i	$⊢ (p \underset{˙}{\leq} W \land (p \neq X \land p \neq Z) \land p \neq Y) \leftrightarrow (p \underset{˙}{\leq} W \land (p \neq X \land p \neq Y) \land p \neq Z)$
46	45	rexbii	$⊢ \exists p \in A (p \underset{˙}{\leq} W \land (p \neq X \land p \neq Z) \land p \neq Y) \leftrightarrow \exists p \in A (p \underset{˙}{\leq} W \land (p \neq X \land p \neq Y) \land p \neq Z)$
47	41 46	sylib	$⊢ ((K \in HL \land W \in H) \land (Z \in A \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)$
48	7 47	lhpexle1lem	$⊢ (K \in HL \land W \in H) \to \exists p \in A (p \underset{˙}{\leq} W \land (p \neq X \land p \neq Y) \land p \neq Z)$
49		df-3an	$⊢ (p \neq X \land p \neq Y \land p \neq Z) \leftrightarrow ((p \neq X \land p \neq Y) \land p \neq Z)$
50	49	anbi2i	$⊢ (p \underset{˙}{\leq} W \land (p \neq X \land p \neq Y \land p \neq Z)) \leftrightarrow (p \underset{˙}{\leq} W \land ((p \neq X \land p \neq Y) \land p \neq Z))$
51	44 50	bitr4i	$⊢ (p \underset{˙}{\leq} W \land (p \neq X \land p \neq Y) \land p \neq Z) \leftrightarrow (p \underset{˙}{\leq} W \land (p \neq X \land p \neq Y \land p \neq Z))$
52	51	rexbii	$⊢ \exists p \in A (p \underset{˙}{\leq} W \land (p \neq X \land p \neq Y) \land p \neq Z) \leftrightarrow \exists p \in A (p \underset{˙}{\leq} W \land (p \neq X \land p \neq Y \land p \neq Z))$
53	48 52	sylib	$⊢ (K \in HL \land W \in H) \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 lhpexle3

Proof