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

Metamath Proof Explorer

Theorem qusin

Description: Restrict the equivalence relation in a quotient structure to the base set. (Contributed by Mario Carneiro, 23-Feb-2015)

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

Proof

Step Hyp Ref Expression
1 qusin.u ⊢ φ → U = R / 𝑠 ∼ ˙
2 qusin.v ⊢ φ → V = Base R
3 qusin.e ⊢ φ → ∼ ˙ ∈ W
4 qusin.r ⊢ φ → R ∈ Z
5 qusin.s ⊢ φ → ∼ ˙ V ⊆ V
6 ecinxp ⊢ ∼ ˙ V ⊆ V ∧ x ∈ V → x ∼ ˙ = x ∼ ˙ ∩ V × V
7 5 6 sylan ⊢ φ ∧ x ∈ V → x ∼ ˙ = x ∼ ˙ ∩ V × V
8 7 mpteq2dva ⊢ φ → x ∈ V ⟼ x ∼ ˙ = x ∈ V ⟼ x ∼ ˙ ∩ V × V
9 8 oveq1d ⊢ φ → x ∈ V ⟼ x ∼ ˙ “ 𝑠 R = x ∈ V ⟼ x ∼ ˙ ∩ V × V “ 𝑠 R
10 eqid ⊢ x ∈ V ⟼ x ∼ ˙ = x ∈ V ⟼ x ∼ ˙
11 1 2 10 3 4 qusval ⊢ φ → U = x ∈ V ⟼ x ∼ ˙ “ 𝑠 R
12 eqidd ⊢ φ → R / 𝑠 ∼ ˙ ∩ V × V = R / 𝑠 ∼ ˙ ∩ V × V
13 eqid ⊢ x ∈ V ⟼ x ∼ ˙ ∩ V × V = x ∈ V ⟼ x ∼ ˙ ∩ V × V
14 inex1g ⊢ ∼ ˙ ∈ W → ∼ ˙ ∩ V × V ∈ V
15 3 14 syl ⊢ φ → ∼ ˙ ∩ V × V ∈ V
16 12 2 13 15 4 qusval ⊢ φ → R / 𝑠 ∼ ˙ ∩ V × V = x ∈ V ⟼ x ∼ ˙ ∩ V × V “ 𝑠 R
17 9 11 16 3eqtr4d ⊢ φ → U = R / 𝑠 ∼ ˙ ∩ V × V