atlrelat1

Description: An atomistic lattice with 0 is relatively atomic. Part of Lemma 7.2 of MaedaMaeda p. 30. ( chpssati , with /\ swapped, analog.) (Contributed by NM, 4-Dec-2011)

	Ref	Expression
Hypotheses	atlrelat1.b	$⊢ B = {Base}_{K}$
	atlrelat1.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	atlrelat1.s	$⊢ \underset{˙}{<} = <_{K}$
	atlrelat1.a	$⊢ A = Atoms (K)$
Assertion	atlrelat1	$⊢ ((K \in OML \land K \in CLat \land K \in AtLat) \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))$

Proof

Step	Hyp	Ref	Expression
1		atlrelat1.b	$⊢ B = {Base}_{K}$
2		atlrelat1.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		atlrelat1.s	$⊢ \underset{˙}{<} = <_{K}$
4		atlrelat1.a	$⊢ A = Atoms (K)$
5		simp13	$⊢ ((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B \land Y \in B) \to K \in AtLat$
6		atlpos	$⊢ K \in AtLat \to K \in Poset$
7	5 6	syl	$⊢ ((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B \land Y \in B) \to K \in Poset$
8	1 2 3	pltnle	$⊢ ((K \in Poset \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \to \neg Y \underset{˙}{\leq} X$
9	8	ex	$⊢ (K \in Poset \land X \in B \land Y \in B) \to (X \underset{˙}{<} Y \to \neg Y \underset{˙}{\leq} X)$
10	7 9	syld3an1	$⊢ ((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B \land Y \in B) \to (X \underset{˙}{<} Y \to \neg Y \underset{˙}{\leq} X)$
11		iman	$⊢ (p \underset{˙}{\leq} Y \to p \underset{˙}{\leq} X) \leftrightarrow \neg (p \underset{˙}{\leq} Y \land \neg p \underset{˙}{\leq} X)$
12		ancom	$⊢ (p \underset{˙}{\leq} Y \land \neg p \underset{˙}{\leq} X) \leftrightarrow (\neg p \underset{˙}{\leq} X \land p \underset{˙}{\leq} Y)$
13	11 12	xchbinx	$⊢ (p \underset{˙}{\leq} Y \to p \underset{˙}{\leq} X) \leftrightarrow \neg (\neg p \underset{˙}{\leq} X \land p \underset{˙}{\leq} Y)$
14	13	ralbii	$⊢ \forall p \in A (p \underset{˙}{\leq} Y \to p \underset{˙}{\leq} X) \leftrightarrow \forall p \in A \neg (\neg p \underset{˙}{\leq} X \land p \underset{˙}{\leq} Y)$
15	1 2 4	atlatle	$⊢ ((K \in OML \land K \in CLat \land K \in AtLat) \land Y \in B \land X \in B) \to (Y \underset{˙}{\leq} X \leftrightarrow \forall p \in A (p \underset{˙}{\leq} Y \to p \underset{˙}{\leq} X))$
16	15	3com23	$⊢ ((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B \land Y \in B) \to (Y \underset{˙}{\leq} X \leftrightarrow \forall p \in A (p \underset{˙}{\leq} Y \to p \underset{˙}{\leq} X))$
17	16	biimprd	$⊢ ((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} Y \to p \underset{˙}{\leq} X) \to Y \underset{˙}{\leq} X)$
18	14 17	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 \neg (\neg p \underset{˙}{\leq} X \land p \underset{˙}{\leq} Y) \to Y \underset{˙}{\leq} X)$
19	18	con3d	$⊢ ((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B \land Y \in B) \to (\neg Y \underset{˙}{\leq} X \to \neg \forall p \in A \neg (\neg p \underset{˙}{\leq} X \land p \underset{˙}{\leq} Y))$
20		dfrex2	$⊢ \exists p \in A (\neg p \underset{˙}{\leq} X \land p \underset{˙}{\leq} Y) \leftrightarrow \neg \forall p \in A \neg (\neg p \underset{˙}{\leq} X \land p \underset{˙}{\leq} Y)$
21	19 20	syl6ibr	$⊢ ((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B \land Y \in B) \to (\neg Y \underset{˙}{\leq} X \to \exists p \in A (\neg p \underset{˙}{\leq} X \land p \underset{˙}{\leq} Y))$
22	10 21	syld	$⊢ ((K \in OML \land K \in CLat \land K \in AtLat) \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))$

Metamath Proof Explorer

Theorem atlrelat1

Proof