Step |
Hyp |
Ref |
Expression |
1 |
|
df-cnvrefrels |
⊢ CnvRefRels = ( CnvRefs ∩ Rels ) |
2 |
|
df-cnvrefs |
⊢ CnvRefs = { 𝑟 ∣ ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ◡ S ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) } |
3 |
|
dmexg |
⊢ ( 𝑟 ∈ V → dom 𝑟 ∈ V ) |
4 |
3
|
elv |
⊢ dom 𝑟 ∈ V |
5 |
|
rnexg |
⊢ ( 𝑟 ∈ V → ran 𝑟 ∈ V ) |
6 |
5
|
elv |
⊢ ran 𝑟 ∈ V |
7 |
4 6
|
xpex |
⊢ ( dom 𝑟 × ran 𝑟 ) ∈ V |
8 |
|
inex2g |
⊢ ( ( dom 𝑟 × ran 𝑟 ) ∈ V → ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ∈ V ) |
9 |
|
brcnvssr |
⊢ ( ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ∈ V → ( ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ◡ S ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) ↔ ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) ⊆ ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ) ) |
10 |
7 8 9
|
mp2b |
⊢ ( ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ◡ S ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) ↔ ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) ⊆ ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ) |
11 |
|
elrels6 |
⊢ ( 𝑟 ∈ V → ( 𝑟 ∈ Rels ↔ ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) = 𝑟 ) ) |
12 |
11
|
elv |
⊢ ( 𝑟 ∈ Rels ↔ ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) = 𝑟 ) |
13 |
12
|
biimpi |
⊢ ( 𝑟 ∈ Rels → ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) = 𝑟 ) |
14 |
13
|
sseq1d |
⊢ ( 𝑟 ∈ Rels → ( ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) ⊆ ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ↔ 𝑟 ⊆ ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ) ) |
15 |
10 14
|
syl5bb |
⊢ ( 𝑟 ∈ Rels → ( ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ◡ S ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) ↔ 𝑟 ⊆ ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ) ) |
16 |
1 2 15
|
abeqinbi |
⊢ CnvRefRels = { 𝑟 ∈ Rels ∣ 𝑟 ⊆ ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) } |