This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem qusbas

Description: Base set of a quotient structure. (Contributed by Mario Carneiro, 23-Feb-2015)

Ref Expression
Hypotheses qusbas.u ⊢ φ → U = R / 𝑠 ∼ ˙
qusbas.v ⊢ φ → V = Base R
qusbas.e ⊢ φ → ∼ ˙ ∈ W
qusbas.r ⊢ φ → R ∈ Z
Assertion qusbas ⊢ φ → V / ∼ ˙ = Base U

Proof

Step Hyp Ref Expression
1 qusbas.u ⊢ φ → U = R / 𝑠 ∼ ˙
2 qusbas.v ⊢ φ → V = Base R
3 qusbas.e ⊢ φ → ∼ ˙ ∈ W
4 qusbas.r ⊢ φ → R ∈ Z
5 eqid ⊢ x ∈ V ⟼ x ∼ ˙ = x ∈ V ⟼ x ∼ ˙
6 1 2 5 3 4 qusval ⊢ φ → U = x ∈ V ⟼ x ∼ ˙ “ 𝑠 R
7 1 2 5 3 4 quslem ⊢ φ → x ∈ V ⟼ x ∼ ˙ : V ⟶ onto V / ∼ ˙
8 6 2 7 4 imasbas ⊢ φ → V / ∼ ˙ = Base U