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 ⊢ ( 𝜑 → 𝑅 Er 𝐴 )
qsss.2 ⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
Assertion uniqs2 ( 𝜑 → ∪ ( 𝐴 / 𝑅 ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 qsss.1 ⊢ ( 𝜑 → 𝑅 Er 𝐴 )
2 qsss.2 ⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
3 uniqsw ⊢ ( 𝑅 ∈ 𝑉 → ∪ ( 𝐴 / 𝑅 ) = ( 𝑅 “ 𝐴 ) )
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 ⊢ ( 𝜑 → ∪ ( 𝐴 / 𝑅 ) = 𝐴 )