This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ispsubclN

Description: The predicate "is a closed projective subspace". (Contributed by NM, 23-Jan-2012) (New usage is discouraged.)

Ref Expression
Hypotheses psubclset.a 
|- A = ( Atoms ` K )
psubclset.p 
|- ._|_ = ( _|_P ` K )
psubclset.c 
|- C = ( PSubCl ` K )
Assertion ispsubclN 
|- ( K e. D -> ( X e. C <-> ( X C_ A /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) ) )

Proof

Step Hyp Ref Expression
1 psubclset.a 
 |-  A = ( Atoms ` K )
2 psubclset.p 
 |-  ._|_ = ( _|_P ` K )
3 psubclset.c 
 |-  C = ( PSubCl ` K )
4 1 2 3 psubclsetN 
 |-  ( K e. D -> C = { x | ( x C_ A /\ ( ._|_ ` ( ._|_ ` x ) ) = x ) } )
5 4 eleq2d 
 |-  ( K e. D -> ( X e. C <-> X e. { x | ( x C_ A /\ ( ._|_ ` ( ._|_ ` x ) ) = x ) } ) )
6 1 fvexi 
 |-  A e. _V
7 6 ssex 
 |-  ( X C_ A -> X e. _V )
8 7 adantr 
 |-  ( ( X C_ A /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) -> X e. _V )
9 sseq1 
 |-  ( x = X -> ( x C_ A <-> X C_ A ) )
10 2fveq3 
 |-  ( x = X -> ( ._|_ ` ( ._|_ ` x ) ) = ( ._|_ ` ( ._|_ ` X ) ) )
11 id 
 |-  ( x = X -> x = X )
12 10 11 eqeq12d 
 |-  ( x = X -> ( ( ._|_ ` ( ._|_ ` x ) ) = x <-> ( ._|_ ` ( ._|_ ` X ) ) = X ) )
13 9 12 anbi12d 
 |-  ( x = X -> ( ( x C_ A /\ ( ._|_ ` ( ._|_ ` x ) ) = x ) <-> ( X C_ A /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) ) )
14 8 13 elab3 
 |-  ( X e. { x | ( x C_ A /\ ( ._|_ ` ( ._|_ ` x ) ) = x ) } <-> ( X C_ A /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) )
15 5 14 bitrdi 
 |-  ( K e. D -> ( X e. C <-> ( X C_ A /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) ) )