Metamath Proof Explorer


Theorem hlrelat5N

Description: An atomistic lattice with 0 is relatively atomic, using the definition in Remark 2 of Kalmbach p. 149. (Contributed by NM, 21-Oct-2011) (New usage is discouraged.)

Ref Expression
Hypotheses hlrelat5.b B = Base K
hlrelat5.l ˙ = K
hlrelat5.s < ˙ = < K
hlrelat5.j ˙ = join K
hlrelat5.a A = Atoms K
Assertion hlrelat5N K HL X B Y B X < ˙ Y p A X < ˙ X ˙ p p ˙ Y

Proof

Step Hyp Ref Expression
1 hlrelat5.b B = Base K
2 hlrelat5.l ˙ = K
3 hlrelat5.s < ˙ = < K
4 hlrelat5.j ˙ = join K
5 hlrelat5.a A = Atoms K
6 1 2 3 5 hlrelat1 K HL X B Y B X < ˙ Y p A ¬ p ˙ X p ˙ Y
7 6 imp K HL X B Y B X < ˙ Y p A ¬ p ˙ X p ˙ Y
8 hllat K HL K Lat
9 id X B X B
10 1 5 atbase p A p B
11 ovexd p B X ˙ p V
12 2 3 pltval K Lat X B X ˙ p V X < ˙ X ˙ p X ˙ X ˙ p X X ˙ p
13 11 12 syl3an3 K Lat X B p B X < ˙ X ˙ p X ˙ X ˙ p X X ˙ p
14 1 2 4 latlej1 K Lat X B p B X ˙ X ˙ p
15 14 biantrurd K Lat X B p B X X ˙ p X ˙ X ˙ p X X ˙ p
16 13 15 bitr4d K Lat X B p B X < ˙ X ˙ p X X ˙ p
17 1 2 4 latleeqj1 K Lat p B X B p ˙ X p ˙ X = X
18 17 3com23 K Lat X B p B p ˙ X p ˙ X = X
19 1 4 latjcom K Lat X B p B X ˙ p = p ˙ X
20 19 eqeq1d K Lat X B p B X ˙ p = X p ˙ X = X
21 18 20 bitr4d K Lat X B p B p ˙ X X ˙ p = X
22 21 notbid K Lat X B p B ¬ p ˙ X ¬ X ˙ p = X
23 nesym X X ˙ p ¬ X ˙ p = X
24 22 23 bitr4di K Lat X B p B ¬ p ˙ X X X ˙ p
25 16 24 bitr4d K Lat X B p B X < ˙ X ˙ p ¬ p ˙ X
26 8 9 10 25 syl3an K HL X B p A X < ˙ X ˙ p ¬ p ˙ X
27 26 3expa K HL X B p A X < ˙ X ˙ p ¬ p ˙ X
28 27 anbi1d K HL X B p A X < ˙ X ˙ p p ˙ Y ¬ p ˙ X p ˙ Y
29 28 rexbidva K HL X B p A X < ˙ X ˙ p p ˙ Y p A ¬ p ˙ X p ˙ Y
30 29 3adant3 K HL X B Y B p A X < ˙ X ˙ p p ˙ Y p A ¬ p ˙ X p ˙ Y
31 30 adantr K HL X B Y B X < ˙ Y p A X < ˙ X ˙ p p ˙ Y p A ¬ p ˙ X p ˙ Y
32 7 31 mpbird K HL X B Y B X < ˙ Y p A X < ˙ X ˙ p p ˙ Y