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

Metamath Proof Explorer

Theorem quslem

Description: The function in qusval is a surjection onto a quotient set. (Contributed by Mario Carneiro, 23-Feb-2015)

Ref Expression
Hypotheses qusval.u 
|- ( ph -> U = ( R /s .~ ) )
qusval.v 
|- ( ph -> V = ( Base ` R ) )
qusval.f 
|- F = ( x e. V |-> [ x ] .~ )
qusval.e 
|- ( ph -> .~ e. W )
qusval.r 
|- ( ph -> R e. Z )
Assertion quslem 
|- ( ph -> F : V -onto-> ( V /. .~ ) )

Proof

Step Hyp Ref Expression
1 qusval.u 
 |-  ( ph -> U = ( R /s .~ ) )
2 qusval.v 
 |-  ( ph -> V = ( Base ` R ) )
3 qusval.f 
 |-  F = ( x e. V |-> [ x ] .~ )
4 qusval.e 
 |-  ( ph -> .~ e. W )
5 qusval.r 
 |-  ( ph -> R e. Z )
6 ecexg 
 |-  ( .~ e. W -> [ x ] .~ e. _V )
7 4 6 syl 
 |-  ( ph -> [ x ] .~ e. _V )
8 7 ralrimivw 
 |-  ( ph -> A. x e. V [ x ] .~ e. _V )
9 3 fnmpt 
 |-  ( A. x e. V [ x ] .~ e. _V -> F Fn V )
10 8 9 syl 
 |-  ( ph -> F Fn V )
11 dffn4 
 |-  ( F Fn V <-> F : V -onto-> ran F )
12 10 11 sylib 
 |-  ( ph -> F : V -onto-> ran F )
13 3 rnmpt 
 |-  ran F = { y | E. x e. V y = [ x ] .~ }
14 df-qs 
 |-  ( V /. .~ ) = { y | E. x e. V y = [ x ] .~ }
15 13 14 eqtr4i 
 |-  ran F = ( V /. .~ )
16 foeq3 
 |-  ( ran F = ( V /. .~ ) -> ( F : V -onto-> ran F <-> F : V -onto-> ( V /. .~ ) ) )
17 15 16 ax-mp 
 |-  ( F : V -onto-> ran F <-> F : V -onto-> ( V /. .~ ) )
18 12 17 sylib 
 |-  ( ph -> F : V -onto-> ( V /. .~ ) )