Step |
Hyp |
Ref |
Expression |
1 |
|
relinxp |
⊢ Rel ( 𝑅 ∩ ( 𝐴 × ran ( 𝑅 ↾ 𝐴 ) ) ) |
2 |
|
relopabv |
⊢ Rel { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) } |
3 |
|
eleq1w |
⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) ) |
4 |
|
breq1 |
⊢ ( 𝑥 = 𝑧 → ( 𝑥 𝑅 𝑦 ↔ 𝑧 𝑅 𝑦 ) ) |
5 |
3 4
|
anbi12d |
⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑧 𝑅 𝑦 ) ) ) |
6 |
|
breq2 |
⊢ ( 𝑦 = 𝑤 → ( 𝑧 𝑅 𝑦 ↔ 𝑧 𝑅 𝑤 ) ) |
7 |
6
|
anbi2d |
⊢ ( 𝑦 = 𝑤 → ( ( 𝑧 ∈ 𝐴 ∧ 𝑧 𝑅 𝑦 ) ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑧 𝑅 𝑤 ) ) ) |
8 |
5 7
|
opelopabg |
⊢ ( ( 𝑧 ∈ V ∧ 𝑤 ∈ V ) → ( 〈 𝑧 , 𝑤 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) } ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑧 𝑅 𝑤 ) ) ) |
9 |
8
|
el2v |
⊢ ( 〈 𝑧 , 𝑤 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) } ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑧 𝑅 𝑤 ) ) |
10 |
|
brinxprnres |
⊢ ( 𝑤 ∈ V → ( 𝑧 ( 𝑅 ∩ ( 𝐴 × ran ( 𝑅 ↾ 𝐴 ) ) ) 𝑤 ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑧 𝑅 𝑤 ) ) ) |
11 |
10
|
elv |
⊢ ( 𝑧 ( 𝑅 ∩ ( 𝐴 × ran ( 𝑅 ↾ 𝐴 ) ) ) 𝑤 ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑧 𝑅 𝑤 ) ) |
12 |
|
df-br |
⊢ ( 𝑧 ( 𝑅 ∩ ( 𝐴 × ran ( 𝑅 ↾ 𝐴 ) ) ) 𝑤 ↔ 〈 𝑧 , 𝑤 〉 ∈ ( 𝑅 ∩ ( 𝐴 × ran ( 𝑅 ↾ 𝐴 ) ) ) ) |
13 |
9 11 12
|
3bitr2ri |
⊢ ( 〈 𝑧 , 𝑤 〉 ∈ ( 𝑅 ∩ ( 𝐴 × ran ( 𝑅 ↾ 𝐴 ) ) ) ↔ 〈 𝑧 , 𝑤 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) } ) |
14 |
1 2 13
|
eqrelriiv |
⊢ ( 𝑅 ∩ ( 𝐴 × ran ( 𝑅 ↾ 𝐴 ) ) ) = { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) } |