Metamath Proof Explorer

Theorem pclvalN

Description: Value of 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 pclvalN 
|- ( ( K e. V /\ X C_ A ) -> ( U ` X ) = |^| { 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 1 fvexi 
 |-  A e. _V
5 4 elpw2 
 |-  ( X e. ~P A <-> X C_ A )
6 1 2 3 pclfvalN 
 |-  ( K e. V -> U = ( x e. ~P A |-> |^| { y e. S | x C_ y } ) )
7 6 fveq1d 
 |-  ( K e. V -> ( U ` X ) = ( ( x e. ~P A |-> |^| { y e. S | x C_ y } ) ` X ) )
8 7 adantr 
 |-  ( ( K e. V /\ X e. ~P A ) -> ( U ` X ) = ( ( x e. ~P A |-> |^| { y e. S | x C_ y } ) ` X ) )
9 eqid 
 |-  ( x e. ~P A |-> |^| { y e. S | x C_ y } ) = ( x e. ~P A |-> |^| { y e. S | x C_ y } )
10 sseq1 
 |-  ( x = X -> ( x C_ y <-> X C_ y ) )
11 10 rabbidv 
 |-  ( x = X -> { y e. S | x C_ y } = { y e. S | X C_ y } )
12 11 inteqd 
 |-  ( x = X -> |^| { y e. S | x C_ y } = |^| { y e. S | X C_ y } )
13 simpr 
 |-  ( ( K e. V /\ X e. ~P A ) -> X e. ~P A )
14 elpwi 
 |-  ( X e. ~P A -> X C_ A )
15 14 adantl 
 |-  ( ( K e. V /\ X e. ~P A ) -> X C_ A )
16 1 2 atpsubN 
 |-  ( K e. V -> A e. S )
17 16 adantr 
 |-  ( ( K e. V /\ X e. ~P A ) -> A e. S )
18 sseq2 
 |-  ( y = A -> ( X C_ y <-> X C_ A ) )
19 18 elrab3 
 |-  ( A e. S -> ( A e. { y e. S | X C_ y } <-> X C_ A ) )
20 17 19 syl 
 |-  ( ( K e. V /\ X e. ~P A ) -> ( A e. { y e. S | X C_ y } <-> X C_ A ) )
21 15 20 mpbird 
 |-  ( ( K e. V /\ X e. ~P A ) -> A e. { y e. S | X C_ y } )
22 21 ne0d 
 |-  ( ( K e. V /\ X e. ~P A ) -> { y e. S | X C_ y } =/= (/) )
23 intex 
 |-  ( { y e. S | X C_ y } =/= (/) <-> |^| { y e. S | X C_ y } e. _V )
24 22 23 sylib 
 |-  ( ( K e. V /\ X e. ~P A ) -> |^| { y e. S | X C_ y } e. _V )
25 9 12 13 24 fvmptd3 
 |-  ( ( K e. V /\ X e. ~P A ) -> ( ( x e. ~P A |-> |^| { y e. S | x C_ y } ) ` X ) = |^| { y e. S | X C_ y } )
26 8 25 eqtrd 
 |-  ( ( K e. V /\ X e. ~P A ) -> ( U ` X ) = |^| { y e. S | X C_ y } )
27 5 26 sylan2br 
 |-  ( ( K e. V /\ X C_ A ) -> ( U ` X ) = |^| { y e. S | X C_ y } )