Theorem elpclN

Description: Membership in the projective subspace closure function. (Contributed by NM, 13-Sep-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pclfval.a	|- A = ( Atoms ` K )
	pclfval.s	|- S = ( PSubSp ` K )
	pclfval.c	|- U = ( PCl ` K )
	elpcl.q	|- Q e. _V
Assertion	elpclN	|- ( ( K e. V /\ X C_ A ) -> ( Q e. ( U ` X ) <-> A. y e. S ( X C_ y -> Q e. y ) ) )

Proof

Step	Hyp	Ref	Expression
1		pclfval.a	|- A = ( Atoms ` K )
2		pclfval.s	|- S = ( PSubSp ` K )
3		pclfval.c	|- U = ( PCl ` K )
4		elpcl.q	|- Q e. _V
5	1 2 3	pclvalN	|- ( ( K e. V /\ X C_ A ) -> ( U ` X ) = |^| { y e. S | X C_ y } )
6	5	eleq2d	|- ( ( K e. V /\ X C_ A ) -> ( Q e. ( U ` X ) <-> Q e. |^| { y e. S | X C_ y } ) )
7	4	elintrab	|- ( Q e. |^| { y e. S | X C_ y } <-> A. y e. S ( X C_ y -> Q e. y ) )
8	6 7	bitrdi	|- ( ( K e. V /\ X C_ A ) -> ( Q e. ( U ` X ) <-> A. y e. S ( X C_ y -> Q e. y ) ) )