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 
|- ( ph -> U = ( R /s .~ ) )
qusin.v 
|- ( ph -> V = ( Base ` R ) )
qusin.e 
|- ( ph -> .~ e. W )
qusin.r 
|- ( ph -> R e. Z )
qusin.s 
|- ( ph -> ( .~ " V ) C_ V )
Assertion qusin 
|- ( ph -> U = ( R /s ( .~ i^i ( V X. V ) ) ) )

Proof

Step Hyp Ref Expression
1 qusin.u 
 |-  ( ph -> U = ( R /s .~ ) )
2 qusin.v 
 |-  ( ph -> V = ( Base ` R ) )
3 qusin.e 
 |-  ( ph -> .~ e. W )
4 qusin.r 
 |-  ( ph -> R e. Z )
5 qusin.s 
 |-  ( ph -> ( .~ " V ) C_ V )
6 ecinxp 
 |-  ( ( ( .~ " V ) C_ V /\ x e. V ) -> [ x ] .~ = [ x ] ( .~ i^i ( V X. V ) ) )
7 5 6 sylan 
 |-  ( ( ph /\ x e. V ) -> [ x ] .~ = [ x ] ( .~ i^i ( V X. V ) ) )
8 7 mpteq2dva 
 |-  ( ph -> ( x e. V |-> [ x ] .~ ) = ( x e. V |-> [ x ] ( .~ i^i ( V X. V ) ) ) )
9 8 oveq1d 
 |-  ( ph -> ( ( x e. V |-> [ x ] .~ ) "s R ) = ( ( x e. V |-> [ x ] ( .~ i^i ( V X. V ) ) ) "s R ) )
10 eqid 
 |-  ( x e. V |-> [ x ] .~ ) = ( x e. V |-> [ x ] .~ )
11 1 2 10 3 4 qusval 
 |-  ( ph -> U = ( ( x e. V |-> [ x ] .~ ) "s R ) )
12 eqidd 
 |-  ( ph -> ( R /s ( .~ i^i ( V X. V ) ) ) = ( R /s ( .~ i^i ( V X. V ) ) ) )
13 eqid 
 |-  ( x e. V |-> [ x ] ( .~ i^i ( V X. V ) ) ) = ( x e. V |-> [ x ] ( .~ i^i ( V X. V ) ) )
14 inex1g 
 |-  ( .~ e. W -> ( .~ i^i ( V X. V ) ) e. _V )
15 3 14 syl 
 |-  ( ph -> ( .~ i^i ( V X. V ) ) e. _V )
16 12 2 13 15 4 qusval 
 |-  ( ph -> ( R /s ( .~ i^i ( V X. V ) ) ) = ( ( x e. V |-> [ x ] ( .~ i^i ( V X. V ) ) ) "s R ) )
17 9 11 16 3eqtr4d 
 |-  ( ph -> U = ( R /s ( .~ i^i ( V X. V ) ) ) )