Metamath Proof Explorer


Theorem isat2

Description: The predicate "is an atom". ( elatcv0 analog.) (Contributed by NM, 18-Jun-2012)

Ref Expression
Hypotheses isatom.b B = Base K
isatom.z 0 ˙ = 0. K
isatom.c C = K
isatom.a A = Atoms K
Assertion isat2 K D P B P A 0 ˙ C P

Proof

Step Hyp Ref Expression
1 isatom.b B = Base K
2 isatom.z 0 ˙ = 0. K
3 isatom.c C = K
4 isatom.a A = Atoms K
5 1 2 3 4 isat K D P A P B 0 ˙ C P
6 5 baibd K D P B P A 0 ˙ C P