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 ⊢ ( 𝜑 → 𝑈 = ( 𝑅 /s ∼ ) )
qusin.v ⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
qusin.e ⊢ ( 𝜑 → ∼ ∈ 𝑊 )
qusin.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑍 )
qusin.s ⊢ ( 𝜑 → ( ∼ “ 𝑉 ) ⊆ 𝑉 )
Assertion qusin ( 𝜑 → 𝑈 = ( 𝑅 /s ( ∼ ∩ ( 𝑉 × 𝑉 ) ) ) )

Proof

Step Hyp Ref Expression
1 qusin.u ⊢ ( 𝜑 → 𝑈 = ( 𝑅 /s ∼ ) )
2 qusin.v ⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
3 qusin.e ⊢ ( 𝜑 → ∼ ∈ 𝑊 )
4 qusin.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑍 )
5 qusin.s ⊢ ( 𝜑 → ( ∼ “ 𝑉 ) ⊆ 𝑉 )
6 ecinxp ⊢ ( ( ( ∼ “ 𝑉 ) ⊆ 𝑉 ∧ 𝑥 ∈ 𝑉 ) → [ 𝑥 ] ∼ = [ 𝑥 ] ( ∼ ∩ ( 𝑉 × 𝑉 ) ) )
7 5 6 sylan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → [ 𝑥 ] ∼ = [ 𝑥 ] ( ∼ ∩ ( 𝑉 × 𝑉 ) ) )
8 7 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ∼ ) = ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ( ∼ ∩ ( 𝑉 × 𝑉 ) ) ) )
9 8 oveq1d ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ∼ ) “s 𝑅 ) = ( ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ( ∼ ∩ ( 𝑉 × 𝑉 ) ) ) “s 𝑅 ) )
10 eqid ⊢ ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ∼ ) = ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ∼ )
11 1 2 10 3 4 qusval ⊢ ( 𝜑 → 𝑈 = ( ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ∼ ) “s 𝑅 ) )
12 eqidd ⊢ ( 𝜑 → ( 𝑅 /s ( ∼ ∩ ( 𝑉 × 𝑉 ) ) ) = ( 𝑅 /s ( ∼ ∩ ( 𝑉 × 𝑉 ) ) ) )
13 eqid ⊢ ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ( ∼ ∩ ( 𝑉 × 𝑉 ) ) ) = ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ( ∼ ∩ ( 𝑉 × 𝑉 ) ) )
14 inex1g ⊢ ( ∼ ∈ 𝑊 → ( ∼ ∩ ( 𝑉 × 𝑉 ) ) ∈ V )
15 3 14 syl ⊢ ( 𝜑 → ( ∼ ∩ ( 𝑉 × 𝑉 ) ) ∈ V )
16 12 2 13 15 4 qusval ⊢ ( 𝜑 → ( 𝑅 /s ( ∼ ∩ ( 𝑉 × 𝑉 ) ) ) = ( ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ( ∼ ∩ ( 𝑉 × 𝑉 ) ) ) “s 𝑅 ) )
17 9 11 16 3eqtr4d ⊢ ( 𝜑 → 𝑈 = ( 𝑅 /s ( ∼ ∩ ( 𝑉 × 𝑉 ) ) ) )