Metamath Proof Explorer


Theorem uniqs2

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

Ref Expression
Hypotheses qsss.1 ( 𝜑𝑅 Er 𝐴 )
qsss.2 ( 𝜑𝑅𝑉 )
Assertion uniqs2 ( 𝜑 ( 𝐴 / 𝑅 ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 qsss.1 ( 𝜑𝑅 Er 𝐴 )
2 qsss.2 ( 𝜑𝑅𝑉 )
3 uniqs ( 𝑅𝑉 ( 𝐴 / 𝑅 ) = ( 𝑅𝐴 ) )
4 2 3 syl ( 𝜑 ( 𝐴 / 𝑅 ) = ( 𝑅𝐴 ) )
5 erdm ( 𝑅 Er 𝐴 → dom 𝑅 = 𝐴 )
6 1 5 syl ( 𝜑 → dom 𝑅 = 𝐴 )
7 6 imaeq2d ( 𝜑 → ( 𝑅 “ dom 𝑅 ) = ( 𝑅𝐴 ) )
8 4 7 eqtr4d ( 𝜑 ( 𝐴 / 𝑅 ) = ( 𝑅 “ dom 𝑅 ) )
9 imadmrn ( 𝑅 “ dom 𝑅 ) = ran 𝑅
10 8 9 eqtrdi ( 𝜑 ( 𝐴 / 𝑅 ) = ran 𝑅 )
11 errn ( 𝑅 Er 𝐴 → ran 𝑅 = 𝐴 )
12 1 11 syl ( 𝜑 → ran 𝑅 = 𝐴 )
13 10 12 eqtrd ( 𝜑 ( 𝐴 / 𝑅 ) = 𝐴 )