atlatle

Description: The ordering of two Hilbert lattice elements is determined by the atoms under them. ( chrelat3 analog.) (Contributed by NM, 5-Nov-2012)

	Ref	Expression
Hypotheses	atlatle.b	$⊢ B = {Base}_{K}$
	atlatle.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	atlatle.a	$⊢ A = Atoms (K)$
Assertion	atlatle	$⊢ ((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B \land Y \in B) \to (X \underset{˙}{\leq} Y \leftrightarrow \forall p \in A (p \underset{˙}{\leq} X \to p \underset{˙}{\leq} Y))$

Proof

Step	Hyp	Ref	Expression
1		atlatle.b	$⊢ B = {Base}_{K}$
2		atlatle.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		atlatle.a	$⊢ A = Atoms (K)$
4		simpl13	$⊢ (((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B \land Y \in B) \land p \in A) \to K \in AtLat$
5		atlpos	$⊢ K \in AtLat \to K \in Poset$
6	4 5	syl	$⊢ (((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B \land Y \in B) \land p \in A) \to K \in Poset$
7	1 3	atbase	$⊢ p \in A \to p \in B$
8	7	adantl	$⊢ (((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B \land Y \in B) \land p \in A) \to p \in B$
9		simpl2	$⊢ (((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B \land Y \in B) \land p \in A) \to X \in B$
10		simpl3	$⊢ (((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B \land Y \in B) \land p \in A) \to Y \in B$
11	1 2	postr	$⊢ (K \in Poset \land (p \in B \land X \in B \land Y \in B)) \to ((p \underset{˙}{\leq} X \land X \underset{˙}{\leq} Y) \to p \underset{˙}{\leq} Y)$
12	6 8 9 10 11	syl13anc	$⊢ (((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B \land Y \in B) \land p \in A) \to ((p \underset{˙}{\leq} X \land X \underset{˙}{\leq} Y) \to p \underset{˙}{\leq} Y)$
13	12	expcomd	$⊢ (((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B \land Y \in B) \land p \in A) \to (X \underset{˙}{\leq} Y \to (p \underset{˙}{\leq} X \to p \underset{˙}{\leq} Y))$
14	13	ralrimdva	$⊢ ((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B \land Y \in B) \to (X \underset{˙}{\leq} Y \to \forall p \in A (p \underset{˙}{\leq} X \to p \underset{˙}{\leq} Y))$
15		ss2rab	$⊢ \{p \in A \| p \underset{˙}{\leq} X\} \subseteq \{p \in A \| p \underset{˙}{\leq} Y\} \leftrightarrow \forall p \in A (p \underset{˙}{\leq} X \to p \underset{˙}{\leq} Y)$
16		simpl12	$⊢ (((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B \land Y \in B) \land \{p \in A \| p \underset{˙}{\leq} X\} \subseteq \{p \in A \| p \underset{˙}{\leq} Y\}) \to K \in CLat$
17		ssrab2	$⊢ \{p \in A \| p \underset{˙}{\leq} Y\} \subseteq A$
18	1 3	atssbase	$⊢ A \subseteq B$
19	17 18	sstri	$⊢ \{p \in A \| p \underset{˙}{\leq} Y\} \subseteq B$
20		eqid	$⊢ lub (K) = lub (K)$
21	1 2 20	lubss	$⊢ (K \in CLat \land \{p \in A \| p \underset{˙}{\leq} Y\} \subseteq B \land \{p \in A \| p \underset{˙}{\leq} X\} \subseteq \{p \in A \| p \underset{˙}{\leq} Y\}) \to lub (K) (\{p \in A \| p \underset{˙}{\leq} X\}) \underset{˙}{\leq} lub (K) (\{p \in A \| p \underset{˙}{\leq} Y\})$
22	19 21	mp3an2	$⊢ (K \in CLat \land \{p \in A \| p \underset{˙}{\leq} X\} \subseteq \{p \in A \| p \underset{˙}{\leq} Y\}) \to lub (K) (\{p \in A \| p \underset{˙}{\leq} X\}) \underset{˙}{\leq} lub (K) (\{p \in A \| p \underset{˙}{\leq} Y\})$
23	16 22	sylancom	$⊢ (((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B \land Y \in B) \land \{p \in A \| p \underset{˙}{\leq} X\} \subseteq \{p \in A \| p \underset{˙}{\leq} Y\}) \to lub (K) (\{p \in A \| p \underset{˙}{\leq} X\}) \underset{˙}{\leq} lub (K) (\{p \in A \| p \underset{˙}{\leq} Y\})$
24	23	ex	$⊢ ((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B \land Y \in B) \to (\{p \in A \| p \underset{˙}{\leq} X\} \subseteq \{p \in A \| p \underset{˙}{\leq} Y\} \to lub (K) (\{p \in A \| p \underset{˙}{\leq} X\}) \underset{˙}{\leq} lub (K) (\{p \in A \| p \underset{˙}{\leq} Y\}))$
25	1 2 20 3	atlatmstc	$⊢ ((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B) \to lub (K) (\{p \in A \| p \underset{˙}{\leq} X\}) = X$
26	25	3adant3	$⊢ ((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B \land Y \in B) \to lub (K) (\{p \in A \| p \underset{˙}{\leq} X\}) = X$
27	1 2 20 3	atlatmstc	$⊢ ((K \in OML \land K \in CLat \land K \in AtLat) \land Y \in B) \to lub (K) (\{p \in A \| p \underset{˙}{\leq} Y\}) = Y$
28	27	3adant2	$⊢ ((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B \land Y \in B) \to lub (K) (\{p \in A \| p \underset{˙}{\leq} Y\}) = Y$
29	26 28	breq12d	$⊢ ((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B \land Y \in B) \to (lub (K) (\{p \in A \| p \underset{˙}{\leq} X\}) \underset{˙}{\leq} lub (K) (\{p \in A \| p \underset{˙}{\leq} Y\}) \leftrightarrow X \underset{˙}{\leq} Y)$
30	24 29	sylibd	$⊢ ((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B \land Y \in B) \to (\{p \in A \| p \underset{˙}{\leq} X\} \subseteq \{p \in A \| p \underset{˙}{\leq} Y\} \to X \underset{˙}{\leq} Y)$
31	15 30	syl5bir	$⊢ ((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B \land Y \in B) \to (\forall p \in A (p \underset{˙}{\leq} X \to p \underset{˙}{\leq} Y) \to X \underset{˙}{\leq} Y)$
32	14 31	impbid	$⊢ ((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B \land Y \in B) \to (X \underset{˙}{\leq} Y \leftrightarrow \forall p \in A (p \underset{˙}{\leq} X \to p \underset{˙}{\leq} Y))$

Metamath Proof Explorer

Theorem atlatle

Proof