Metamath Proof Explorer


Theorem qusbas

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

Ref Expression
Hypotheses qusbas.u ( 𝜑𝑈 = ( 𝑅 /s ) )
qusbas.v ( 𝜑𝑉 = ( Base ‘ 𝑅 ) )
qusbas.e ( 𝜑𝑊 )
qusbas.r ( 𝜑𝑅𝑍 )
Assertion qusbas ( 𝜑 → ( 𝑉 / ) = ( Base ‘ 𝑈 ) )

Proof

Step Hyp Ref Expression
1 qusbas.u ( 𝜑𝑈 = ( 𝑅 /s ) )
2 qusbas.v ( 𝜑𝑉 = ( Base ‘ 𝑅 ) )
3 qusbas.e ( 𝜑𝑊 )
4 qusbas.r ( 𝜑𝑅𝑍 )
5 eqid ( 𝑥𝑉 ↦ [ 𝑥 ] ) = ( 𝑥𝑉 ↦ [ 𝑥 ] )
6 1 2 5 3 4 qusval ( 𝜑𝑈 = ( ( 𝑥𝑉 ↦ [ 𝑥 ] ) “s 𝑅 ) )
7 1 2 5 3 4 quslem ( 𝜑 → ( 𝑥𝑉 ↦ [ 𝑥 ] ) : 𝑉onto→ ( 𝑉 / ) )
8 6 2 7 4 imasbas ( 𝜑 → ( 𝑉 / ) = ( Base ‘ 𝑈 ) )