Metamath Proof Explorer


Theorem isat3

Description: The predicate "is an atom". ( elat2 analog.) (Contributed by NM, 27-Apr-2014)

Ref Expression
Hypotheses isat3.b B = Base K
isat3.l ˙ = K
isat3.z 0 ˙ = 0. K
isat3.a A = Atoms K
Assertion isat3 K AtLat P A P B P 0 ˙ x B x ˙ P x = P x = 0 ˙

Proof

Step Hyp Ref Expression
1 isat3.b B = Base K
2 isat3.l ˙ = K
3 isat3.z 0 ˙ = 0. K
4 isat3.a A = Atoms K
5 eqid K = K
6 1 3 5 4 isat K AtLat P A P B 0 ˙ K P
7 simpl K AtLat P B K AtLat
8 1 3 atl0cl K AtLat 0 ˙ B
9 8 adantr K AtLat P B 0 ˙ B
10 simpr K AtLat P B P B
11 eqid < K = < K
12 1 2 11 5 cvrval2 K AtLat 0 ˙ B P B 0 ˙ K P 0 ˙ < K P x B 0 ˙ < K x x ˙ P x = P
13 7 9 10 12 syl3anc K AtLat P B 0 ˙ K P 0 ˙ < K P x B 0 ˙ < K x x ˙ P x = P
14 1 11 3 atlltn0 K AtLat P B 0 ˙ < K P P 0 ˙
15 1 11 3 atlltn0 K AtLat x B 0 ˙ < K x x 0 ˙
16 15 adantlr K AtLat P B x B 0 ˙ < K x x 0 ˙
17 16 imbi1d K AtLat P B x B 0 ˙ < K x x = P x 0 ˙ x = P
18 17 imbi2d K AtLat P B x B x ˙ P 0 ˙ < K x x = P x ˙ P x 0 ˙ x = P
19 impexp 0 ˙ < K x x ˙ P x = P 0 ˙ < K x x ˙ P x = P
20 bi2.04 0 ˙ < K x x ˙ P x = P x ˙ P 0 ˙ < K x x = P
21 19 20 bitri 0 ˙ < K x x ˙ P x = P x ˙ P 0 ˙ < K x x = P
22 orcom x = P x = 0 ˙ x = 0 ˙ x = P
23 neor x = 0 ˙ x = P x 0 ˙ x = P
24 22 23 bitri x = P x = 0 ˙ x 0 ˙ x = P
25 24 imbi2i x ˙ P x = P x = 0 ˙ x ˙ P x 0 ˙ x = P
26 18 21 25 3bitr4g K AtLat P B x B 0 ˙ < K x x ˙ P x = P x ˙ P x = P x = 0 ˙
27 26 ralbidva K AtLat P B x B 0 ˙ < K x x ˙ P x = P x B x ˙ P x = P x = 0 ˙
28 14 27 anbi12d K AtLat P B 0 ˙ < K P x B 0 ˙ < K x x ˙ P x = P P 0 ˙ x B x ˙ P x = P x = 0 ˙
29 13 28 bitr2d K AtLat P B P 0 ˙ x B x ˙ P x = P x = 0 ˙ 0 ˙ K P
30 29 pm5.32da K AtLat P B P 0 ˙ x B x ˙ P x = P x = 0 ˙ P B 0 ˙ K P
31 6 30 bitr4d K AtLat P A P B P 0 ˙ x B x ˙ P x = P x = 0 ˙
32 3anass P B P 0 ˙ x B x ˙ P x = P x = 0 ˙ P B P 0 ˙ x B x ˙ P x = P x = 0 ˙
33 31 32 bitr4di K AtLat P A P B P 0 ˙ x B x ˙ P x = P x = 0 ˙