Theorem pclfvalN

Description: The projective subspace closure function. (Contributed by NM, 7-Sep-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pclfval.a	|- A = ( Atoms ` K )
	pclfval.s	|- S = ( PSubSp ` K )
	pclfval.c	|- U = ( PCl ` K )
Assertion	pclfvalN	|- ( K e. V -> U = ( x e. ~P A |-> |^| { y e. S | x C_ 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		elex	|- ( K e. V -> K e. _V )
5		fveq2	|- ( k = K -> ( Atoms ` k ) = ( Atoms ` K ) )
6	5 1	eqtr4di	|- ( k = K -> ( Atoms ` k ) = A )
7	6	pweqd	|- ( k = K -> ~P ( Atoms ` k ) = ~P A )
8		fveq2	|- ( k = K -> ( PSubSp ` k ) = ( PSubSp ` K ) )
9	8 2	eqtr4di	|- ( k = K -> ( PSubSp ` k ) = S )
10	9	rabeqdv	|- ( k = K -> { y e. ( PSubSp ` k ) | x C_ y } = { y e. S | x C_ y } )
11	10	inteqd	|- ( k = K -> |^| { y e. ( PSubSp ` k ) | x C_ y } = |^| { y e. S | x C_ y } )
12	7 11	mpteq12dv	|- ( k = K -> ( x e. ~P ( Atoms ` k ) |-> |^| { y e. ( PSubSp ` k ) | x C_ y } ) = ( x e. ~P A |-> |^| { y e. S | x C_ y } ) )
13		df-pclN	|- PCl = ( k e. _V |-> ( x e. ~P ( Atoms ` k ) |-> |^| { y e. ( PSubSp ` k ) | x C_ y } ) )
14	1	fvexi	|- A e. _V
15	14	pwex	|- ~P A e. _V
16	15	mptex	|- ( x e. ~P A |-> |^| { y e. S | x C_ y } ) e. _V
17	12 13 16	fvmpt	|- ( K e. _V -> ( PCl ` K ) = ( x e. ~P A |-> |^| { y e. S | x C_ y } ) )
18	3 17	syl5eq	|- ( K e. _V -> U = ( x e. ~P A |-> |^| { y e. S | x C_ y } ) )
19	4 18	syl	|- ( K e. V -> U = ( x e. ~P A |-> |^| { y e. S | x C_ y } ) )