Metamath Proof Explorer


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 } ) ) )