Metamath Proof Explorer


Theorem isat

Description: The predicate "is an atom". ( ela analog.) (Contributed by NM, 18-Sep-2011)

Ref Expression
Hypotheses isatom.b
|- B = ( Base ` K )
isatom.z
|- .0. = ( 0. ` K )
isatom.c
|- C = ( 
isatom.a
|- A = ( Atoms ` K )
Assertion isat
|- ( K e. D -> ( P e. A <-> ( P e. B /\ .0. C P ) ) )

Proof

Step Hyp Ref Expression
1 isatom.b
 |-  B = ( Base ` K )
2 isatom.z
 |-  .0. = ( 0. ` K )
3 isatom.c
 |-  C = ( 
4 isatom.a
 |-  A = ( Atoms ` K )
5 1 2 3 4 pats
 |-  ( K e. D -> A = { x e. B | .0. C x } )
6 5 eleq2d
 |-  ( K e. D -> ( P e. A <-> P e. { x e. B | .0. C x } ) )
7 breq2
 |-  ( x = P -> ( .0. C x <-> .0. C P ) )
8 7 elrab
 |-  ( P e. { x e. B | .0. C x } <-> ( P e. B /\ .0. C P ) )
9 6 8 bitrdi
 |-  ( K e. D -> ( P e. A <-> ( P e. B /\ .0. C P ) ) )