Theorem watfvalN

Description: 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	watfvalN	|- ( K e. B -> W = ( d e. A |-> ( 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		elex	|- ( K e. B -> K e. _V )
5		fveq2	|- ( k = K -> ( Atoms ` k ) = ( Atoms ` K ) )
6	5 1	eqtr4di	|- ( k = K -> ( Atoms ` k ) = A )
7		fveq2	|- ( k = K -> ( _|_P ` k ) = ( _|_P ` K ) )
8	7	fveq1d	|- ( k = K -> ( ( _|_P ` k ) ` { d } ) = ( ( _|_P ` K ) ` { d } ) )
9	6 8	difeq12d	|- ( k = K -> ( ( Atoms ` k ) \ ( ( _|_P ` k ) ` { d } ) ) = ( A \ ( ( _|_P ` K ) ` { d } ) ) )
10	6 9	mpteq12dv	|- ( k = K -> ( d e. ( Atoms ` k ) |-> ( ( Atoms ` k ) \ ( ( _|_P ` k ) ` { d } ) ) ) = ( d e. A |-> ( A \ ( ( _|_P ` K ) ` { d } ) ) ) )
11		df-watsN	|- WAtoms = ( k e. _V |-> ( d e. ( Atoms ` k ) |-> ( ( Atoms ` k ) \ ( ( _|_P ` k ) ` { d } ) ) ) )
12	10 11 1	mptfvmpt	|- ( K e. _V -> ( WAtoms ` K ) = ( d e. A |-> ( A \ ( ( _|_P ` K ) ` { d } ) ) ) )
13	3 12	syl5eq	|- ( K e. _V -> W = ( d e. A |-> ( A \ ( ( _|_P ` K ) ` { d } ) ) ) )
14	4 13	syl	|- ( K e. B -> W = ( d e. A |-> ( A \ ( ( _|_P ` K ) ` { d } ) ) ) )