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 ⊢ φ → 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 / ∼ ˙