Theorem pclvalN 33843

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

Hypotheses

Ref	Expression
pclfval.a	|- A = ( Atoms ` K )
pclfval.s	|- S = ( PSubSp ` K )
pclfval.c	|- U = ( PCl ` K )

Assertion

Ref	Expression
pclvalN	|- ( ( K e. V /\ X C_ A ) -> ( U ` X ) = |^| { y e. S | X C_ y } )

Distinct variable groups:   y, A   y, K   y, S   y, X

Allowed substitution hints:   U( y)   V( y)

Proof of Theorem pclvalN

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		pclfval.a	. . . 4 |- A = ( Atoms ` K )
2		fvex 5802	. . . 4 |- ( Atoms ` K ) e. _V
3	1, 2	eqeltri 2535	. . 3 |- A e. _V
4	3	elpw2 4557	. 2 |- ( X e. ~P A <-> X C_ A )
5		pclfval.s	. . . . . 6 |- S = ( PSubSp ` K )
6		pclfval.c	. . . . . 6 |- U = ( PCl ` K )
7	1, 5, 6	pclfvalN 33842	. . . . 5 |- ( K e. V -> U = ( x e. ~P A |-> |^| { y e. S | x C_ y } ) )
8	7	fveq1d 5794	. . . 4 |- ( K e. V -> ( U ` X ) = ( ( x e. ~P A |-> |^| { y e. S | x C_ y } ) ` X ) )
9	8	adantr 465	. . 3 |- ( ( K e. V /\ X e. ~P A ) -> ( U ` X ) = ( ( x e. ~P A |-> |^| { y e. S | x C_ y } ) ` X ) )
10		simpr 461	. . . 4 |- ( ( K e. V /\ X e. ~P A ) -> X e. ~P A )
11		elpwi 3970	. . . . . . . 8 |- ( X e. ~P A -> X C_ A )
12	11	adantl 466	. . . . . . 7 |- ( ( K e. V /\ X e. ~P A ) -> X C_ A )
13	1, 5	atpsubN 33706	. . . . . . . . 9 |- ( K e. V -> A e. S )
14	13	adantr 465	. . . . . . . 8 |- ( ( K e. V /\ X e. ~P A ) -> A e. S )
15		sseq2 3479	. . . . . . . . 9 |- ( y = A -> ( X C_ y <-> X C_ A ) )
16	15	elrab3 3218	. . . . . . . 8 |- ( A e. S -> ( A e. { y e. S | X C_ y } <-> X C_ A ) )
17	14, 16	syl 16	. . . . . . 7 |- ( ( K e. V /\ X e. ~P A ) -> ( A e. { y e. S | X C_ y } <-> X C_ A ) )
18	12, 17	mpbird 232	. . . . . 6 |- ( ( K e. V /\ X e. ~P A ) -> A e. { y e. S | X C_ y } )
19		ne0i 3744	. . . . . 6 |- ( A e. { y e. S | X C_ y } -> { y e. S | X C_ y } =/= (/) )
20	18, 19	syl 16	. . . . 5 |- ( ( K e. V /\ X e. ~P A ) -> { y e. S | X C_ y } =/= (/) )
21		intex 4549	. . . . 5 |- ( { y e. S | X C_ y } =/= (/) <-> |^| { y e. S | X C_ y } e. _V )
22	20, 21	sylib 196	. . . 4 |- ( ( K e. V /\ X e. ~P A ) -> |^| { y e. S | X C_ y } e. _V )
23		sseq1 3478	. . . . . . 7 |- ( x = X -> ( x C_ y <-> X C_ y ) )
24	23	rabbidv 3063	. . . . . 6 |- ( x = X -> { y e. S | x C_ y } = { y e. S | X C_ y } )
25	24	inteqd 4234	. . . . 5 |- ( x = X -> |^| { y e. S | x C_ y } = |^| { y e. S | X C_ y } )
26		eqid 2451	. . . . 5 |- ( x e. ~P A |-> |^| { y e. S | x C_ y } ) = ( x e. ~P A |-> |^| { y e. S | x C_ y } )
27	25, 26	fvmptg 5874	. . . 4 |- ( ( X e. ~P A /\ |^| { y e. S | X C_ y } e. _V ) -> ( ( x e. ~P A |-> |^| { y e. S | x C_ y } ) ` X ) = |^| { y e. S | X C_ y } )
28	10, 22, 27	syl2anc 661	. . 3 |- ( ( K e. V /\ X e. ~P A ) -> ( ( x e. ~P A |-> |^| { y e. S | x C_ y } ) ` X ) = |^| { y e. S | X C_ y } )
29	9, 28	eqtrd 2492	. 2 |- ( ( K e. V /\ X e. ~P A ) -> ( U ` X ) = |^| { y e. S | X C_ y } )
30	4, 29	sylan2br 476	1 |- ( ( K e. V /\ X C_ A ) -> ( U ` X ) = |^| { y e. S | X C_ y } )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1370   e. wcel 1758   =/= wne 2644   {crab 2799   _Vcvv 3071   C_ wss 3429   (/)c0 3738   ~Pcpw 3961   |^|cint 4229   |-> cmpt 4451   ` cfv 5519   Atomscatm 33217   PSubSpcpsubsp 33449   PClcpclN 33840

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-rep 4504  ax-sep 4514  ax-nul 4522  ax-pow 4571  ax-pr 4632

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-reu 2802  df-rab 2804  df-v 3073  df-sbc 3288  df-csb 3390  df-dif 3432  df-un 3434  df-in 3436  df-ss 3443  df-nul 3739  df-if 3893  df-pw 3963  df-sn 3979  df-pr 3981  df-op 3985  df-uni 4193  df-int 4230  df-iun 4274  df-br 4394  df-opab 4452  df-mpt 4453  df-id 4737  df-xp 4947  df-rel 4948  df-cnv 4949  df-co 4950  df-dm 4951  df-rn 4952  df-res 4953  df-ima 4954  df-iota 5482  df-fun 5521  df-fn 5522  df-f 5523  df-f1 5524  df-fo 5525  df-f1o 5526  df-fv 5527  df-ov 6196  df-psubsp 33456  df-pclN 33841

This theorem is referenced by:  pclclN  33844  elpclN  33845  elpcliN  33846  pclssN  33847  pclssidN  33848  pclidN  33849