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

Metamath Proof Explorer

Theorem divsfval

Description: Value of the function in qusval . (Contributed by Mario Carneiro, 24-Feb-2015) (Revised by Mario Carneiro, 12-Aug-2015) (Revised by AV, 12-Jul-2024)

Ref Expression
Hypotheses ercpbl.r 
|- ( ph -> .~ Er V )
ercpbl.v 
|- ( ph -> V e. W )
ercpbl.f 
|- F = ( x e. V |-> [ x ] .~ )
Assertion divsfval 
|- ( ph -> ( F ` A ) = [ A ] .~ )

Proof

Step Hyp Ref Expression
1 ercpbl.r 
 |-  ( ph -> .~ Er V )
2 ercpbl.v 
 |-  ( ph -> V e. W )
3 ercpbl.f 
 |-  F = ( x e. V |-> [ x ] .~ )
4 1 ecss 
 |-  ( ph -> [ A ] .~ C_ V )
5 2 4 ssexd 
 |-  ( ph -> [ A ] .~ e. _V )
6 eceq1 
 |-  ( x = A -> [ x ] .~ = [ A ] .~ )
7 6 3 fvmptg 
 |-  ( ( A e. V /\ [ A ] .~ e. _V ) -> ( F ` A ) = [ A ] .~ )
8 5 7 sylan2 
 |-  ( ( A e. V /\ ph ) -> ( F ` A ) = [ A ] .~ )
9 8 expcom 
 |-  ( ph -> ( A e. V -> ( F ` A ) = [ A ] .~ ) )
10 3 dmeqi 
 |-  dom F = dom ( x e. V |-> [ x ] .~ )
11 1 ecss 
 |-  ( ph -> [ x ] .~ C_ V )
12 2 11 ssexd 
 |-  ( ph -> [ x ] .~ e. _V )
13 12 ralrimivw 
 |-  ( ph -> A. x e. V [ x ] .~ e. _V )
14 dmmptg 
 |-  ( A. x e. V [ x ] .~ e. _V -> dom ( x e. V |-> [ x ] .~ ) = V )
15 13 14 syl 
 |-  ( ph -> dom ( x e. V |-> [ x ] .~ ) = V )
16 10 15 eqtrid 
 |-  ( ph -> dom F = V )
17 16 eleq2d 
 |-  ( ph -> ( A e. dom F <-> A e. V ) )
18 17 notbid 
 |-  ( ph -> ( -. A e. dom F <-> -. A e. V ) )
19 ndmfv 
 |-  ( -. A e. dom F -> ( F ` A ) = (/) )
20 18 19 biimtrrdi 
 |-  ( ph -> ( -. A e. V -> ( F ` A ) = (/) ) )
21 ecdmn0 
 |-  ( A e. dom .~ <-> [ A ] .~ =/= (/) )
22 erdm 
 |-  ( .~ Er V -> dom .~ = V )
23 1 22 syl 
 |-  ( ph -> dom .~ = V )
24 23 eleq2d 
 |-  ( ph -> ( A e. dom .~ <-> A e. V ) )
25 24 biimpd 
 |-  ( ph -> ( A e. dom .~ -> A e. V ) )
26 21 25 biimtrrid 
 |-  ( ph -> ( [ A ] .~ =/= (/) -> A e. V ) )
27 26 necon1bd 
 |-  ( ph -> ( -. A e. V -> [ A ] .~ = (/) ) )
28 20 27 jcad 
 |-  ( ph -> ( -. A e. V -> ( ( F ` A ) = (/) /\ [ A ] .~ = (/) ) ) )
29 eqtr3 
 |-  ( ( ( F ` A ) = (/) /\ [ A ] .~ = (/) ) -> ( F ` A ) = [ A ] .~ )
30 28 29 syl6 
 |-  ( ph -> ( -. A e. V -> ( F ` A ) = [ A ] .~ ) )
31 9 30 pm2.61d 
 |-  ( ph -> ( F ` A ) = [ A ] .~ )