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 ( ∼ ∩ ( 𝑉 × 𝑉 ) ) ) )