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	⊢ ( 𝜑 → 𝑈 = ( 𝑅 /s ∼ ) )
	qusval.v	⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
	qusval.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ∼ )
	qusval.e	⊢ ( 𝜑 → ∼ ∈ 𝑊 )
	qusval.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑍 )
Assertion	quslem	⊢ ( 𝜑 → 𝐹 : 𝑉 –onto→ ( 𝑉 / ∼ ) )

Proof

Step	Hyp	Ref	Expression
1		qusval.u	⊢ ( 𝜑 → 𝑈 = ( 𝑅 /s ∼ ) )
2		qusval.v	⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
3		qusval.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ∼ )
4		qusval.e	⊢ ( 𝜑 → ∼ ∈ 𝑊 )
5		qusval.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑍 )
6		ecexg	⊢ ( ∼ ∈ 𝑊 → [ 𝑥 ] ∼ ∈ V )
7	4 6	syl	⊢ ( 𝜑 → [ 𝑥 ] ∼ ∈ V )
8	7	ralrimivw	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑉 [ 𝑥 ] ∼ ∈ V )
9	3	fnmpt	⊢ ( ∀ 𝑥 ∈ 𝑉 [ 𝑥 ] ∼ ∈ V → 𝐹 Fn 𝑉 )
10	8 9	syl	⊢ ( 𝜑 → 𝐹 Fn 𝑉 )
11		dffn4	⊢ ( 𝐹 Fn 𝑉 ↔ 𝐹 : 𝑉 –onto→ ran 𝐹 )
12	10 11	sylib	⊢ ( 𝜑 → 𝐹 : 𝑉 –onto→ ran 𝐹 )
13	3	rnmpt	⊢ ran 𝐹 = { 𝑦 ∣ ∃ 𝑥 ∈ 𝑉 𝑦 = [ 𝑥 ] ∼ }
14		df-qs	⊢ ( 𝑉 / ∼ ) = { 𝑦 ∣ ∃ 𝑥 ∈ 𝑉 𝑦 = [ 𝑥 ] ∼ }
15	13 14	eqtr4i	⊢ ran 𝐹 = ( 𝑉 / ∼ )
16		foeq3	⊢ ( ran 𝐹 = ( 𝑉 / ∼ ) → ( 𝐹 : 𝑉 –onto→ ran 𝐹 ↔ 𝐹 : 𝑉 –onto→ ( 𝑉 / ∼ ) ) )
17	15 16	ax-mp	⊢ ( 𝐹 : 𝑉 –onto→ ran 𝐹 ↔ 𝐹 : 𝑉 –onto→ ( 𝑉 / ∼ ) )
18	12 17	sylib	⊢ ( 𝜑 → 𝐹 : 𝑉 –onto→ ( 𝑉 / ∼ ) )