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 φ U = R / 𝑠 ˙
qusval.v φ V = Base R
qusval.f F = x V x ˙
qusval.e φ ˙ W
qusval.r φ R Z
Assertion quslem φ F : V onto V / ˙

Proof

Step Hyp Ref Expression
1 qusval.u φ U = R / 𝑠 ˙
2 qusval.v φ V = Base R
3 qusval.f F = x V x ˙
4 qusval.e φ ˙ W
5 qusval.r φ R Z
6 ecexg ˙ W x ˙ V
7 4 6 syl φ x ˙ V
8 7 ralrimivw φ x V x ˙ V
9 3 fnmpt x V x ˙ V F Fn V
10 8 9 syl φ F Fn V
11 dffn4 F Fn V F : V onto ran F
12 10 11 sylib φ F : V onto ran F
13 3 rnmpt ran F = y | x V y = x ˙
14 df-qs V / ˙ = y | x 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 φ F : V onto V / ˙