Theorem watvalN

Description: Value of the W atoms function. (Contributed by NM, 26-Jan-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	watomfval.a	|- A = ( Atoms ` K )
	watomfval.p	|- P = ( _|_P ` K )
	watomfval.w	|- W = ( WAtoms ` K )
Assertion	watvalN	|- ( ( K e. B /\ D e. A ) -> ( W ` D ) = ( A \ ( ( _|_P ` K ) ` { D } ) ) )

Proof

Step	Hyp	Ref	Expression
1		watomfval.a	|- A = ( Atoms ` K )
2		watomfval.p	|- P = ( _|_P ` K )
3		watomfval.w	|- W = ( WAtoms ` K )
4	1 2 3	watfvalN	|- ( K e. B -> W = ( d e. A |-> ( A \ ( ( _|_P ` K ) ` { d } ) ) ) )
5	4	fveq1d	|- ( K e. B -> ( W ` D ) = ( ( d e. A |-> ( A \ ( ( _|_P ` K ) ` { d } ) ) ) ` D ) )
6		sneq	|- ( d = D -> { d } = { D } )
7	6	fveq2d	|- ( d = D -> ( ( _|_P ` K ) ` { d } ) = ( ( _|_P ` K ) ` { D } ) )
8	7	difeq2d	|- ( d = D -> ( A \ ( ( _|_P ` K ) ` { d } ) ) = ( A \ ( ( _|_P ` K ) ` { D } ) ) )
9		eqid	|- ( d e. A |-> ( A \ ( ( _|_P ` K ) ` { d } ) ) ) = ( d e. A |-> ( A \ ( ( _|_P ` K ) ` { d } ) ) )
10	1	fvexi	|- A e. _V
11	10	difexi	|- ( A \ ( ( _|_P ` K ) ` { D } ) ) e. _V
12	8 9 11	fvmpt	|- ( D e. A -> ( ( d e. A |-> ( A \ ( ( _|_P ` K ) ` { d } ) ) ) ` D ) = ( A \ ( ( _|_P ` K ) ` { D } ) ) )
13	5 12	sylan9eq	|- ( ( K e. B /\ D e. A ) -> ( W ` D ) = ( A \ ( ( _|_P ` K ) ` { D } ) ) )