Metamath Proof Explorer


Theorem psubclssatN

Description: A closed projective subspace is a set of atoms. (Contributed by NM, 25-Jan-2012) (New usage is discouraged.)

Ref Expression
Hypotheses psubclssat.a
|- A = ( Atoms ` K )
psubclssat.c
|- C = ( PSubCl ` K )
Assertion psubclssatN
|- ( ( K e. D /\ X e. C ) -> X C_ A )

Proof

Step Hyp Ref Expression
1 psubclssat.a
 |-  A = ( Atoms ` K )
2 psubclssat.c
 |-  C = ( PSubCl ` K )
3 eqid
 |-  ( _|_P ` K ) = ( _|_P ` K )
4 1 3 2 psubcliN
 |-  ( ( K e. D /\ X e. C ) -> ( X C_ A /\ ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` X ) ) = X ) )
5 4 simpld
 |-  ( ( K e. D /\ X e. C ) -> X C_ A )