Metamath Proof Explorer

Theorem 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=BaseK
atlrelat1.l ⊢≤˙=≤K
atlrelat1.s ⊢<˙=<K
atlrelat1.a ⊢A=Atoms⁡K
Assertion atlrelat1 ⊢K∈OML∧K∈CLat∧K∈AtLat∧X∈B∧Y∈B→X<˙Y→∃p∈A¬p≤˙X∧p≤˙Y

Proof

Step Hyp Ref Expression
1 atlrelat1.b ⊢B=BaseK
2 atlrelat1.l ⊢≤˙=≤K
3 atlrelat1.s ⊢<˙=<K
4 atlrelat1.a ⊢A=Atoms⁡K
5 simp13 ⊢K∈OML∧K∈CLat∧K∈AtLat∧X∈B∧Y∈B→K∈AtLat
6 atlpos ⊢K∈AtLat→K∈Poset
7 5 6 syl ⊢K∈OML∧K∈CLat∧K∈AtLat∧X∈B∧Y∈B→K∈Poset
8 1 2 3 pltnle ⊢K∈Poset∧X∈B∧Y∈B∧X<˙Y→¬Y≤˙X
9 8 ex ⊢K∈Poset∧X∈B∧Y∈B→X<˙Y→¬Y≤˙X
10 7 9 syld3an1 ⊢K∈OML∧K∈CLat∧K∈AtLat∧X∈B∧Y∈B→X<˙Y→¬Y≤˙X
11 iman ⊢p≤˙Y→p≤˙X↔¬p≤˙Y∧¬p≤˙X
12 ancom ⊢p≤˙Y∧¬p≤˙X↔¬p≤˙X∧p≤˙Y
13 11 12 xchbinx ⊢p≤˙Y→p≤˙X↔¬¬p≤˙X∧p≤˙Y
14 13 ralbii ⊢∀p∈Ap≤˙Y→p≤˙X↔∀p∈A¬¬p≤˙X∧p≤˙Y
15 1 2 4 atlatle ⊢K∈OML∧K∈CLat∧K∈AtLat∧Y∈B∧X∈B→Y≤˙X↔∀p∈Ap≤˙Y→p≤˙X
16 15 3com23 ⊢K∈OML∧K∈CLat∧K∈AtLat∧X∈B∧Y∈B→Y≤˙X↔∀p∈Ap≤˙Y→p≤˙X
17 16 biimprd ⊢K∈OML∧K∈CLat∧K∈AtLat∧X∈B∧Y∈B→∀p∈Ap≤˙Y→p≤˙X→Y≤˙X
18 14 17 biimtrrid ⊢K∈OML∧K∈CLat∧K∈AtLat∧X∈B∧Y∈B→∀p∈A¬¬p≤˙X∧p≤˙Y→Y≤˙X
19 18 con3d ⊢K∈OML∧K∈CLat∧K∈AtLat∧X∈B∧Y∈B→¬Y≤˙X→¬∀p∈A¬¬p≤˙X∧p≤˙Y
20 dfrex2 ⊢∃p∈A¬p≤˙X∧p≤˙Y↔¬∀p∈A¬¬p≤˙X∧p≤˙Y
21 19 20 syl6ibr ⊢K∈OML∧K∈CLat∧K∈AtLat∧X∈B∧Y∈B→¬Y≤˙X→∃p∈A¬p≤˙X∧p≤˙Y
22 10 21 syld ⊢K∈OML∧K∈CLat∧K∈AtLat∧X∈B∧Y∈B→X<˙Y→∃p∈A¬p≤˙X∧p≤˙Y