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 ) ) )