2atlt

Description: Given an atom less than an element, there is another atom less than the element. (Contributed by NM, 6-May-2012)

	Ref	Expression
Hypotheses	2atomslt.b	$⊢ B = {Base}_{K}$
	2atomslt.s	$⊢ \underset{˙}{<} = <_{K}$
	2atomslt.a	$⊢ A = Atoms (K)$
Assertion	2atlt	$⊢ ((K \in HL \land P \in A \land X \in B) \land P \underset{˙}{<} X) \to \exists q \in A (q \neq P \land q \underset{˙}{<} X)$

Proof

Step	Hyp	Ref	Expression
1		2atomslt.b	$⊢ B = {Base}_{K}$
2		2atomslt.s	$⊢ \underset{˙}{<} = <_{K}$
3		2atomslt.a	$⊢ A = Atoms (K)$
4	1 3	atbase	$⊢ P \in A \to P \in B$
5		eqid	$⊢ \leq_{K} = \leq_{K}$
6		eqid	$⊢ join (K) = join (K)$
7	1 5 2 6 3	hlrelat	$⊢ ((K \in HL \land P \in B \land X \in B) \land P \underset{˙}{<} X) \to \exists q \in A (P \underset{˙}{<} (P join (K) q) \land (P join (K) q) \leq_{K} X)$
8	4 7	syl3anl2	$⊢ ((K \in HL \land P \in A \land X \in B) \land P \underset{˙}{<} X) \to \exists q \in A (P \underset{˙}{<} (P join (K) q) \land (P join (K) q) \leq_{K} X)$
9		simp3l	$⊢ (((K \in HL \land P \in A \land X \in B) \land P \underset{˙}{<} X) \land q \in A \land (P \underset{˙}{<} (P join (K) q) \land (P join (K) q) \leq_{K} X)) \to P \underset{˙}{<} (P join (K) q)$
10		simp1l1	$⊢ (((K \in HL \land P \in A \land X \in B) \land P \underset{˙}{<} X) \land q \in A \land (P \underset{˙}{<} (P join (K) q) \land (P join (K) q) \leq_{K} X)) \to K \in HL$
11		simp1l2	$⊢ (((K \in HL \land P \in A \land X \in B) \land P \underset{˙}{<} X) \land q \in A \land (P \underset{˙}{<} (P join (K) q) \land (P join (K) q) \leq_{K} X)) \to P \in A$
12		simp2	$⊢ (((K \in HL \land P \in A \land X \in B) \land P \underset{˙}{<} X) \land q \in A \land (P \underset{˙}{<} (P join (K) q) \land (P join (K) q) \leq_{K} X)) \to q \in A$
13		eqid	$⊢ ⋖_{K} = ⋖_{K}$
14	2 6 3 13	atltcvr	$⊢ (K \in HL \land (P \in A \land P \in A \land q \in A)) \to (P \underset{˙}{<} (P join (K) q) \leftrightarrow P ⋖_{K} (P join (K) q))$
15	10 11 11 12 14	syl13anc	$⊢ (((K \in HL \land P \in A \land X \in B) \land P \underset{˙}{<} X) \land q \in A \land (P \underset{˙}{<} (P join (K) q) \land (P join (K) q) \leq_{K} X)) \to (P \underset{˙}{<} (P join (K) q) \leftrightarrow P ⋖_{K} (P join (K) q))$
16	9 15	mpbid	$⊢ (((K \in HL \land P \in A \land X \in B) \land P \underset{˙}{<} X) \land q \in A \land (P \underset{˙}{<} (P join (K) q) \land (P join (K) q) \leq_{K} X)) \to P ⋖_{K} (P join (K) q)$
17	6 13 3	atcvr1	$⊢ (K \in HL \land P \in A \land q \in A) \to (P \neq q \leftrightarrow P ⋖_{K} (P join (K) q))$
18	10 11 12 17	syl3anc	$⊢ (((K \in HL \land P \in A \land X \in B) \land P \underset{˙}{<} X) \land q \in A \land (P \underset{˙}{<} (P join (K) q) \land (P join (K) q) \leq_{K} X)) \to (P \neq q \leftrightarrow P ⋖_{K} (P join (K) q))$
19	16 18	mpbird	$⊢ (((K \in HL \land P \in A \land X \in B) \land P \underset{˙}{<} X) \land q \in A \land (P \underset{˙}{<} (P join (K) q) \land (P join (K) q) \leq_{K} X)) \to P \neq q$
20	19	necomd	$⊢ (((K \in HL \land P \in A \land X \in B) \land P \underset{˙}{<} X) \land q \in A \land (P \underset{˙}{<} (P join (K) q) \land (P join (K) q) \leq_{K} X)) \to q \neq P$
21	2 6 3	atlt	$⊢ (K \in HL \land q \in A \land P \in A) \to (q \underset{˙}{<} (q join (K) P) \leftrightarrow q \neq P)$
22	10 12 11 21	syl3anc	$⊢ (((K \in HL \land P \in A \land X \in B) \land P \underset{˙}{<} X) \land q \in A \land (P \underset{˙}{<} (P join (K) q) \land (P join (K) q) \leq_{K} X)) \to (q \underset{˙}{<} (q join (K) P) \leftrightarrow q \neq P)$
23	20 22	mpbird	$⊢ (((K \in HL \land P \in A \land X \in B) \land P \underset{˙}{<} X) \land q \in A \land (P \underset{˙}{<} (P join (K) q) \land (P join (K) q) \leq_{K} X)) \to q \underset{˙}{<} (q join (K) P)$
24	10	hllatd	$⊢ (((K \in HL \land P \in A \land X \in B) \land P \underset{˙}{<} X) \land q \in A \land (P \underset{˙}{<} (P join (K) q) \land (P join (K) q) \leq_{K} X)) \to K \in Lat$
25	11 4	syl	$⊢ (((K \in HL \land P \in A \land X \in B) \land P \underset{˙}{<} X) \land q \in A \land (P \underset{˙}{<} (P join (K) q) \land (P join (K) q) \leq_{K} X)) \to P \in B$
26	1 3	atbase	$⊢ q \in A \to q \in B$
27	26	3ad2ant2	$⊢ (((K \in HL \land P \in A \land X \in B) \land P \underset{˙}{<} X) \land q \in A \land (P \underset{˙}{<} (P join (K) q) \land (P join (K) q) \leq_{K} X)) \to q \in B$
28	1 6	latjcom	$⊢ (K \in Lat \land P \in B \land q \in B) \to P join (K) q = q join (K) P$
29	24 25 27 28	syl3anc	$⊢ (((K \in HL \land P \in A \land X \in B) \land P \underset{˙}{<} X) \land q \in A \land (P \underset{˙}{<} (P join (K) q) \land (P join (K) q) \leq_{K} X)) \to P join (K) q = q join (K) P$
30	23 29	breqtrrd	$⊢ (((K \in HL \land P \in A \land X \in B) \land P \underset{˙}{<} X) \land q \in A \land (P \underset{˙}{<} (P join (K) q) \land (P join (K) q) \leq_{K} X)) \to q \underset{˙}{<} (P join (K) q)$
31		simp3r	$⊢ (((K \in HL \land P \in A \land X \in B) \land P \underset{˙}{<} X) \land q \in A \land (P \underset{˙}{<} (P join (K) q) \land (P join (K) q) \leq_{K} X)) \to (P join (K) q) \leq_{K} X$
32		hlpos	$⊢ K \in HL \to K \in Poset$
33	10 32	syl	$⊢ (((K \in HL \land P \in A \land X \in B) \land P \underset{˙}{<} X) \land q \in A \land (P \underset{˙}{<} (P join (K) q) \land (P join (K) q) \leq_{K} X)) \to K \in Poset$
34	1 6	latjcl	$⊢ (K \in Lat \land P \in B \land q \in B) \to P join (K) q \in B$
35	24 25 27 34	syl3anc	$⊢ (((K \in HL \land P \in A \land X \in B) \land P \underset{˙}{<} X) \land q \in A \land (P \underset{˙}{<} (P join (K) q) \land (P join (K) q) \leq_{K} X)) \to P join (K) q \in B$
36		simp1l3	$⊢ (((K \in HL \land P \in A \land X \in B) \land P \underset{˙}{<} X) \land q \in A \land (P \underset{˙}{<} (P join (K) q) \land (P join (K) q) \leq_{K} X)) \to X \in B$
37	1 5 2	pltletr	$⊢ (K \in Poset \land (q \in B \land P join (K) q \in B \land X \in B)) \to ((q \underset{˙}{<} (P join (K) q) \land (P join (K) q) \leq_{K} X) \to q \underset{˙}{<} X)$
38	33 27 35 36 37	syl13anc	$⊢ (((K \in HL \land P \in A \land X \in B) \land P \underset{˙}{<} X) \land q \in A \land (P \underset{˙}{<} (P join (K) q) \land (P join (K) q) \leq_{K} X)) \to ((q \underset{˙}{<} (P join (K) q) \land (P join (K) q) \leq_{K} X) \to q \underset{˙}{<} X)$
39	30 31 38	mp2and	$⊢ (((K \in HL \land P \in A \land X \in B) \land P \underset{˙}{<} X) \land q \in A \land (P \underset{˙}{<} (P join (K) q) \land (P join (K) q) \leq_{K} X)) \to q \underset{˙}{<} X$
40	20 39	jca	$⊢ (((K \in HL \land P \in A \land X \in B) \land P \underset{˙}{<} X) \land q \in A \land (P \underset{˙}{<} (P join (K) q) \land (P join (K) q) \leq_{K} X)) \to (q \neq P \land q \underset{˙}{<} X)$
41	40	3exp	$⊢ ((K \in HL \land P \in A \land X \in B) \land P \underset{˙}{<} X) \to (q \in A \to ((P \underset{˙}{<} (P join (K) q) \land (P join (K) q) \leq_{K} X) \to (q \neq P \land q \underset{˙}{<} X)))$
42	41	reximdvai	$⊢ ((K \in HL \land P \in A \land X \in B) \land P \underset{˙}{<} X) \to (\exists q \in A (P \underset{˙}{<} (P join (K) q) \land (P join (K) q) \leq_{K} X) \to \exists q \in A (q \neq P \land q \underset{˙}{<} X))$
43	8 42	mpd	$⊢ ((K \in HL \land P \in A \land X \in B) \land P \underset{˙}{<} X) \to \exists q \in A (q \neq P \land q \underset{˙}{<} X)$

Metamath Proof Explorer

Theorem 2atlt

Proof