lhpexle1

Description: There exists an atom under a co-atom different from any given element. (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	lhpexle1	$⊢ (K \in HL \land W \in H) \to \exists p \in A (p \underset{˙}{\leq} W \land p \neq X)$

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	lhpexle	$⊢ (K \in HL \land W \in H) \to \exists p \in A p \underset{˙}{\leq} W$
5		tru	$⊢ ⊤$
6	5	jctr	$⊢ p \underset{˙}{\leq} W \to (p \underset{˙}{\leq} W \land ⊤)$
7	6	reximi	$⊢ \exists p \in A p \underset{˙}{\leq} W \to \exists p \in A (p \underset{˙}{\leq} W \land ⊤)$
8	4 7	syl	$⊢ (K \in HL \land W \in H) \to \exists p \in A (p \underset{˙}{\leq} W \land ⊤)$
9		simpll	$⊢ ((K \in HL \land W \in H) \land (X \in A \land X \underset{˙}{\leq} W)) \to K \in HL$
10		simprl	$⊢ ((K \in HL \land W \in H) \land (X \in A \land X \underset{˙}{\leq} W)) \to X \in A$
11		eqid	$⊢ {Base}_{K} = {Base}_{K}$
12	11 3	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
13	12	ad2antlr	$⊢ ((K \in HL \land W \in H) \land (X \in A \land X \underset{˙}{\leq} W)) \to W \in {Base}_{K}$
14		eqid	$⊢ <_{K} = <_{K}$
15	1 14 2 3	lhplt	$⊢ ((K \in HL \land W \in H) \land (X \in A \land X \underset{˙}{\leq} W)) \to X <_{K} W$
16	11 14 2	2atlt	$⊢ ((K \in HL \land X \in A \land W \in {Base}_{K}) \land X <_{K} W) \to \exists p \in A (p \neq X \land p <_{K} W)$
17	9 10 13 15 16	syl31anc	$⊢ ((K \in HL \land W \in H) \land (X \in A \land X \underset{˙}{\leq} W)) \to \exists p \in A (p \neq X \land p <_{K} W)$
18		simp3r	$⊢ (((K \in HL \land W \in H) \land (X \in A \land X \underset{˙}{\leq} W)) \land p \in A \land (p \neq X \land p <_{K} W)) \to p <_{K} W$
19		simp1ll	$⊢ (((K \in HL \land W \in H) \land (X \in A \land X \underset{˙}{\leq} W)) \land p \in A \land (p \neq X \land p <_{K} W)) \to K \in HL$
20		simp2	$⊢ (((K \in HL \land W \in H) \land (X \in A \land X \underset{˙}{\leq} W)) \land p \in A \land (p \neq X \land p <_{K} W)) \to p \in A$
21		simp1lr	$⊢ (((K \in HL \land W \in H) \land (X \in A \land X \underset{˙}{\leq} W)) \land p \in A \land (p \neq X \land p <_{K} W)) \to W \in H$
22	1 14	pltle	$⊢ (K \in HL \land p \in A \land W \in H) \to (p <_{K} W \to p \underset{˙}{\leq} W)$
23	19 20 21 22	syl3anc	$⊢ (((K \in HL \land W \in H) \land (X \in A \land X \underset{˙}{\leq} W)) \land p \in A \land (p \neq X \land p <_{K} W)) \to (p <_{K} W \to p \underset{˙}{\leq} W)$
24	18 23	mpd	$⊢ (((K \in HL \land W \in H) \land (X \in A \land X \underset{˙}{\leq} W)) \land p \in A \land (p \neq X \land p <_{K} W)) \to p \underset{˙}{\leq} W$
25		trud	$⊢ (((K \in HL \land W \in H) \land (X \in A \land X \underset{˙}{\leq} W)) \land p \in A \land (p \neq X \land p <_{K} W)) \to ⊤$
26		simp3l	$⊢ (((K \in HL \land W \in H) \land (X \in A \land X \underset{˙}{\leq} W)) \land p \in A \land (p \neq X \land p <_{K} W)) \to p \neq X$
27	24 25 26	3jca	$⊢ (((K \in HL \land W \in H) \land (X \in A \land X \underset{˙}{\leq} W)) \land p \in A \land (p \neq X \land p <_{K} W)) \to (p \underset{˙}{\leq} W \land ⊤ \land p \neq X)$
28	27	3expia	$⊢ (((K \in HL \land W \in H) \land (X \in A \land X \underset{˙}{\leq} W)) \land p \in A) \to ((p \neq X \land p <_{K} W) \to (p \underset{˙}{\leq} W \land ⊤ \land p \neq X))$
29	28	reximdva	$⊢ ((K \in HL \land W \in H) \land (X \in A \land X \underset{˙}{\leq} W)) \to (\exists p \in A (p \neq X \land p <_{K} W) \to \exists p \in A (p \underset{˙}{\leq} W \land ⊤ \land p \neq X))$
30	17 29	mpd	$⊢ ((K \in HL \land W \in H) \land (X \in A \land X \underset{˙}{\leq} W)) \to \exists p \in A (p \underset{˙}{\leq} W \land ⊤ \land p \neq X)$
31	8 30	lhpexle1lem	$⊢ (K \in HL \land W \in H) \to \exists p \in A (p \underset{˙}{\leq} W \land ⊤ \land p \neq X)$
32		3simpb	$⊢ (p \underset{˙}{\leq} W \land ⊤ \land p \neq X) \to (p \underset{˙}{\leq} W \land p \neq X)$
33	32	reximi	$⊢ \exists p \in A (p \underset{˙}{\leq} W \land ⊤ \land p \neq X) \to \exists p \in A (p \underset{˙}{\leq} W \land p \neq X)$
34	31 33	syl	$⊢ (K \in HL \land W \in H) \to \exists p \in A (p \underset{˙}{\leq} W \land p \neq X)$

Metamath Proof Explorer

Theorem lhpexle1

Proof