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 ⊢ ( 𝜑 → 𝑈 = ( 𝑅 /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→ ( 𝑉 / ∼ ) )