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

Metamath Proof Explorer

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