Step |
Hyp |
Ref |
Expression |
1 |
|
relcnv |
⊢ Rel ◡ 𝑅 |
2 |
|
relxp |
⊢ Rel ( { 𝑥 } × ( ◡ 𝑅 “ { 𝑥 } ) ) |
3 |
2
|
rgenw |
⊢ ∀ 𝑥 ∈ 𝐴 Rel ( { 𝑥 } × ( ◡ 𝑅 “ { 𝑥 } ) ) |
4 |
|
reliun |
⊢ ( Rel ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × ( ◡ 𝑅 “ { 𝑥 } ) ) ↔ ∀ 𝑥 ∈ 𝐴 Rel ( { 𝑥 } × ( ◡ 𝑅 “ { 𝑥 } ) ) ) |
5 |
3 4
|
mpbir |
⊢ Rel ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × ( ◡ 𝑅 “ { 𝑥 } ) ) |
6 |
|
vex |
⊢ 𝑧 ∈ V |
7 |
|
vex |
⊢ 𝑦 ∈ V |
8 |
6 7
|
opeldm |
⊢ ( 〈 𝑧 , 𝑦 〉 ∈ ◡ 𝑅 → 𝑧 ∈ dom ◡ 𝑅 ) |
9 |
|
df-rn |
⊢ ran 𝑅 = dom ◡ 𝑅 |
10 |
8 9
|
eleqtrrdi |
⊢ ( 〈 𝑧 , 𝑦 〉 ∈ ◡ 𝑅 → 𝑧 ∈ ran 𝑅 ) |
11 |
|
ssel2 |
⊢ ( ( ran 𝑅 ⊆ 𝐴 ∧ 𝑧 ∈ ran 𝑅 ) → 𝑧 ∈ 𝐴 ) |
12 |
10 11
|
sylan2 |
⊢ ( ( ran 𝑅 ⊆ 𝐴 ∧ 〈 𝑧 , 𝑦 〉 ∈ ◡ 𝑅 ) → 𝑧 ∈ 𝐴 ) |
13 |
12
|
ex |
⊢ ( ran 𝑅 ⊆ 𝐴 → ( 〈 𝑧 , 𝑦 〉 ∈ ◡ 𝑅 → 𝑧 ∈ 𝐴 ) ) |
14 |
13
|
pm4.71rd |
⊢ ( ran 𝑅 ⊆ 𝐴 → ( 〈 𝑧 , 𝑦 〉 ∈ ◡ 𝑅 ↔ ( 𝑧 ∈ 𝐴 ∧ 〈 𝑧 , 𝑦 〉 ∈ ◡ 𝑅 ) ) ) |
15 |
6 7
|
elimasn |
⊢ ( 𝑦 ∈ ( ◡ 𝑅 “ { 𝑧 } ) ↔ 〈 𝑧 , 𝑦 〉 ∈ ◡ 𝑅 ) |
16 |
15
|
anbi2i |
⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝑦 ∈ ( ◡ 𝑅 “ { 𝑧 } ) ) ↔ ( 𝑧 ∈ 𝐴 ∧ 〈 𝑧 , 𝑦 〉 ∈ ◡ 𝑅 ) ) |
17 |
14 16
|
bitr4di |
⊢ ( ran 𝑅 ⊆ 𝐴 → ( 〈 𝑧 , 𝑦 〉 ∈ ◡ 𝑅 ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑦 ∈ ( ◡ 𝑅 “ { 𝑧 } ) ) ) ) |
18 |
|
sneq |
⊢ ( 𝑥 = 𝑧 → { 𝑥 } = { 𝑧 } ) |
19 |
18
|
imaeq2d |
⊢ ( 𝑥 = 𝑧 → ( ◡ 𝑅 “ { 𝑥 } ) = ( ◡ 𝑅 “ { 𝑧 } ) ) |
20 |
19
|
opeliunxp2 |
⊢ ( 〈 𝑧 , 𝑦 〉 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × ( ◡ 𝑅 “ { 𝑥 } ) ) ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑦 ∈ ( ◡ 𝑅 “ { 𝑧 } ) ) ) |
21 |
17 20
|
bitr4di |
⊢ ( ran 𝑅 ⊆ 𝐴 → ( 〈 𝑧 , 𝑦 〉 ∈ ◡ 𝑅 ↔ 〈 𝑧 , 𝑦 〉 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × ( ◡ 𝑅 “ { 𝑥 } ) ) ) ) |
22 |
1 5 21
|
eqrelrdv |
⊢ ( ran 𝑅 ⊆ 𝐴 → ◡ 𝑅 = ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × ( ◡ 𝑅 “ { 𝑥 } ) ) ) |