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 |
⊢ ( 𝜑 → ∪ ( 𝐴 / 𝑅 ) = 𝐴 ) |