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 /. .~ ) )