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

Metamath Proof Explorer

Theorem uniqs2

Description: The union of a quotient set. (Contributed by Mario Carneiro, 11-Jul-2014)

Ref Expression
Hypotheses qsss.1 
|- ( ph -> R Er A )
qsss.2 
|- ( ph -> R e. V )
Assertion uniqs2 
|- ( ph -> U. ( A /. R ) = A )

Proof

Step Hyp Ref Expression
1 qsss.1 
 |-  ( ph -> R Er A )
2 qsss.2 
 |-  ( ph -> R e. V )
3 uniqsw 
 |-  ( R e. V -> U. ( A /. R ) = ( R " A ) )
4 2 3 syl 
 |-  ( ph -> U. ( A /. R ) = ( R " A ) )
5 erdm 
 |-  ( R Er A -> dom R = A )
6 1 5 syl 
 |-  ( ph -> dom R = A )
7 6 imaeq2d 
 |-  ( ph -> ( R " dom R ) = ( R " A ) )
8 4 7 eqtr4d 
 |-  ( ph -> U. ( A /. R ) = ( R " dom R ) )
9 imadmrn 
 |-  ( R " dom R ) = ran R
10 8 9 eqtrdi 
 |-  ( ph -> U. ( A /. R ) = ran R )
11 errn 
 |-  ( R Er A -> ran R = A )
12 1 11 syl 
 |-  ( ph -> ran R = A )
13 10 12 eqtrd 
 |-  ( ph -> U. ( A /. R ) = A )