Step |
Hyp |
Ref |
Expression |
1 |
|
ecex2 |
⊢ ( ( 𝑅 ↾ 𝐴 ) ∈ 𝑉 → ( 𝑥 ∈ 𝐴 → [ 𝑥 ] 𝑅 ∈ V ) ) |
2 |
1
|
ralrimiv |
⊢ ( ( 𝑅 ↾ 𝐴 ) ∈ 𝑉 → ∀ 𝑥 ∈ 𝐴 [ 𝑥 ] 𝑅 ∈ V ) |
3 |
|
dfiun2g |
⊢ ( ∀ 𝑥 ∈ 𝐴 [ 𝑥 ] 𝑅 ∈ V → ∪ 𝑥 ∈ 𝐴 [ 𝑥 ] 𝑅 = ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = [ 𝑥 ] 𝑅 } ) |
4 |
2 3
|
syl |
⊢ ( ( 𝑅 ↾ 𝐴 ) ∈ 𝑉 → ∪ 𝑥 ∈ 𝐴 [ 𝑥 ] 𝑅 = ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = [ 𝑥 ] 𝑅 } ) |
5 |
4
|
eqcomd |
⊢ ( ( 𝑅 ↾ 𝐴 ) ∈ 𝑉 → ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = [ 𝑥 ] 𝑅 } = ∪ 𝑥 ∈ 𝐴 [ 𝑥 ] 𝑅 ) |
6 |
|
df-qs |
⊢ ( 𝐴 / 𝑅 ) = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = [ 𝑥 ] 𝑅 } |
7 |
6
|
unieqi |
⊢ ∪ ( 𝐴 / 𝑅 ) = ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = [ 𝑥 ] 𝑅 } |
8 |
|
df-ec |
⊢ [ 𝑥 ] 𝑅 = ( 𝑅 “ { 𝑥 } ) |
9 |
8
|
a1i |
⊢ ( 𝑥 ∈ 𝐴 → [ 𝑥 ] 𝑅 = ( 𝑅 “ { 𝑥 } ) ) |
10 |
9
|
iuneq2i |
⊢ ∪ 𝑥 ∈ 𝐴 [ 𝑥 ] 𝑅 = ∪ 𝑥 ∈ 𝐴 ( 𝑅 “ { 𝑥 } ) |
11 |
|
imaiun |
⊢ ( 𝑅 “ ∪ 𝑥 ∈ 𝐴 { 𝑥 } ) = ∪ 𝑥 ∈ 𝐴 ( 𝑅 “ { 𝑥 } ) |
12 |
|
iunid |
⊢ ∪ 𝑥 ∈ 𝐴 { 𝑥 } = 𝐴 |
13 |
12
|
imaeq2i |
⊢ ( 𝑅 “ ∪ 𝑥 ∈ 𝐴 { 𝑥 } ) = ( 𝑅 “ 𝐴 ) |
14 |
10 11 13
|
3eqtr2ri |
⊢ ( 𝑅 “ 𝐴 ) = ∪ 𝑥 ∈ 𝐴 [ 𝑥 ] 𝑅 |
15 |
5 7 14
|
3eqtr4g |
⊢ ( ( 𝑅 ↾ 𝐴 ) ∈ 𝑉 → ∪ ( 𝐴 / 𝑅 ) = ( 𝑅 “ 𝐴 ) ) |