hlrelat3

Description: The Hilbert lattice is relatively atomic. Stronger version of hlrelat . (Contributed by NM, 2-May-2012)

	Ref	Expression
Hypotheses	hlrelat3.b	$⊢ B = {Base}_{K}$
	hlrelat3.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	hlrelat3.s	$⊢ \underset{˙}{<} = <_{K}$
	hlrelat3.j	$⊢ \underset{˙}{\lor} = join (K)$
	hlrelat3.c	$⊢ C = ⋖_{K}$
	hlrelat3.a	$⊢ A = Atoms (K)$
Assertion	hlrelat3	$⊢ ((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \to \exists p \in A (X C (X \underset{˙}{\lor} p) \land (X \underset{˙}{\lor} p) \underset{˙}{\leq} Y)$

Proof

Step	Hyp	Ref	Expression
1		hlrelat3.b	$⊢ B = {Base}_{K}$
2		hlrelat3.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		hlrelat3.s	$⊢ \underset{˙}{<} = <_{K}$
4		hlrelat3.j	$⊢ \underset{˙}{\lor} = join (K)$
5		hlrelat3.c	$⊢ C = ⋖_{K}$
6		hlrelat3.a	$⊢ A = Atoms (K)$
7	1 2 3 6	hlrelat1	$⊢ (K \in HL \land X \in B \land Y \in B) \to (X \underset{˙}{<} Y \to \exists p \in A (\neg p \underset{˙}{\leq} X \land p \underset{˙}{\leq} Y))$
8	7	imp	$⊢ ((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \to \exists p \in A (\neg p \underset{˙}{\leq} X \land p \underset{˙}{\leq} Y)$
9		simp3l	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in A \land (\neg p \underset{˙}{\leq} X \land p \underset{˙}{\leq} Y)) \to \neg p \underset{˙}{\leq} X$
10		simp1l1	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in A \land (\neg p \underset{˙}{\leq} X \land p \underset{˙}{\leq} Y)) \to K \in HL$
11		simp1l2	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in A \land (\neg p \underset{˙}{\leq} X \land p \underset{˙}{\leq} Y)) \to X \in B$
12		simp2	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in A \land (\neg p \underset{˙}{\leq} X \land p \underset{˙}{\leq} Y)) \to p \in A$
13	1 2 4 5 6	cvr1	$⊢ (K \in HL \land X \in B \land p \in A) \to (\neg p \underset{˙}{\leq} X \leftrightarrow X C (X \underset{˙}{\lor} p))$
14	10 11 12 13	syl3anc	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in A \land (\neg p \underset{˙}{\leq} X \land p \underset{˙}{\leq} Y)) \to (\neg p \underset{˙}{\leq} X \leftrightarrow X C (X \underset{˙}{\lor} p))$
15	9 14	mpbid	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in A \land (\neg p \underset{˙}{\leq} X \land p \underset{˙}{\leq} Y)) \to X C (X \underset{˙}{\lor} p)$
16		simp1l	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in A \land (\neg p \underset{˙}{\leq} X \land p \underset{˙}{\leq} Y)) \to (K \in HL \land X \in B \land Y \in B)$
17		simp1r	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in A \land (\neg p \underset{˙}{\leq} X \land p \underset{˙}{\leq} Y)) \to X \underset{˙}{<} Y$
18	2 3	pltle	$⊢ (K \in HL \land X \in B \land Y \in B) \to (X \underset{˙}{<} Y \to X \underset{˙}{\leq} Y)$
19	16 17 18	sylc	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in A \land (\neg p \underset{˙}{\leq} X \land p \underset{˙}{\leq} Y)) \to X \underset{˙}{\leq} Y$
20		simp3r	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in A \land (\neg p \underset{˙}{\leq} X \land p \underset{˙}{\leq} Y)) \to p \underset{˙}{\leq} Y$
21	10	hllatd	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in A \land (\neg p \underset{˙}{\leq} X \land p \underset{˙}{\leq} Y)) \to K \in Lat$
22	1 6	atbase	$⊢ p \in A \to p \in B$
23	12 22	syl	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in A \land (\neg p \underset{˙}{\leq} X \land p \underset{˙}{\leq} Y)) \to p \in B$
24		simp1l3	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in A \land (\neg p \underset{˙}{\leq} X \land p \underset{˙}{\leq} Y)) \to Y \in B$
25	1 2 4	latjle12	$⊢ (K \in Lat \land (X \in B \land p \in B \land Y \in B)) \to ((X \underset{˙}{\leq} Y \land p \underset{˙}{\leq} Y) \leftrightarrow (X \underset{˙}{\lor} p) \underset{˙}{\leq} Y)$
26	21 11 23 24 25	syl13anc	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in A \land (\neg p \underset{˙}{\leq} X \land p \underset{˙}{\leq} Y)) \to ((X \underset{˙}{\leq} Y \land p \underset{˙}{\leq} Y) \leftrightarrow (X \underset{˙}{\lor} p) \underset{˙}{\leq} Y)$
27	19 20 26	mpbi2and	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in A \land (\neg p \underset{˙}{\leq} X \land p \underset{˙}{\leq} Y)) \to (X \underset{˙}{\lor} p) \underset{˙}{\leq} Y$
28	15 27	jca	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in A \land (\neg p \underset{˙}{\leq} X \land p \underset{˙}{\leq} Y)) \to (X C (X \underset{˙}{\lor} p) \land (X \underset{˙}{\lor} p) \underset{˙}{\leq} Y)$
29	28	3exp	$⊢ ((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \to (p \in A \to ((\neg p \underset{˙}{\leq} X \land p \underset{˙}{\leq} Y) \to (X C (X \underset{˙}{\lor} p) \land (X \underset{˙}{\lor} p) \underset{˙}{\leq} Y)))$
30	29	reximdvai	$⊢ ((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \to (\exists p \in A (\neg p \underset{˙}{\leq} X \land p \underset{˙}{\leq} Y) \to \exists p \in A (X C (X \underset{˙}{\lor} p) \land (X \underset{˙}{\lor} p) \underset{˙}{\leq} Y))$
31	8 30	mpd	$⊢ ((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \to \exists p \in A (X C (X \underset{˙}{\lor} p) \land (X \underset{˙}{\lor} p) \underset{˙}{\leq} Y)$

Metamath Proof Explorer

Theorem hlrelat3

Proof