Step |
Hyp |
Ref |
Expression |
1 |
|
dfrefrels2 |
⊢ RefRels = { 𝑟 ∈ Rels ∣ ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ⊆ 𝑟 } |
2 |
|
dfsymrels2 |
⊢ SymRels = { 𝑟 ∈ Rels ∣ ◡ 𝑟 ⊆ 𝑟 } |
3 |
1 2
|
ineq12i |
⊢ ( RefRels ∩ SymRels ) = ( { 𝑟 ∈ Rels ∣ ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ⊆ 𝑟 } ∩ { 𝑟 ∈ Rels ∣ ◡ 𝑟 ⊆ 𝑟 } ) |
4 |
|
inrab |
⊢ ( { 𝑟 ∈ Rels ∣ ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ⊆ 𝑟 } ∩ { 𝑟 ∈ Rels ∣ ◡ 𝑟 ⊆ 𝑟 } ) = { 𝑟 ∈ Rels ∣ ( ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ⊆ 𝑟 ∧ ◡ 𝑟 ⊆ 𝑟 ) } |
5 |
|
symrefref2 |
⊢ ( ◡ 𝑟 ⊆ 𝑟 → ( ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ⊆ 𝑟 ↔ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ) ) |
6 |
5
|
pm5.32ri |
⊢ ( ( ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ⊆ 𝑟 ∧ ◡ 𝑟 ⊆ 𝑟 ) ↔ ( ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ ◡ 𝑟 ⊆ 𝑟 ) ) |
7 |
6
|
rabbii |
⊢ { 𝑟 ∈ Rels ∣ ( ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ⊆ 𝑟 ∧ ◡ 𝑟 ⊆ 𝑟 ) } = { 𝑟 ∈ Rels ∣ ( ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ ◡ 𝑟 ⊆ 𝑟 ) } |
8 |
3 4 7
|
3eqtri |
⊢ ( RefRels ∩ SymRels ) = { 𝑟 ∈ Rels ∣ ( ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ ◡ 𝑟 ⊆ 𝑟 ) } |