This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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