Step |
Hyp |
Ref |
Expression |
1 |
|
df-symrels |
⊢ SymRels = ( Syms ∩ Rels ) |
2 |
|
df-syms |
⊢ Syms = { 𝑟 ∣ ◡ ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) S ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) } |
3 |
|
inex1g |
⊢ ( 𝑟 ∈ V → ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) ∈ V ) |
4 |
3
|
elv |
⊢ ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) ∈ V |
5 |
|
brssr |
⊢ ( ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) ∈ V → ( ◡ ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) S ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) ↔ ◡ ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) ⊆ ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) ) ) |
6 |
4 5
|
ax-mp |
⊢ ( ◡ ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) S ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) ↔ ◡ ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) ⊆ ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) ) |
7 |
|
elrels6 |
⊢ ( 𝑟 ∈ V → ( 𝑟 ∈ Rels ↔ ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) = 𝑟 ) ) |
8 |
7
|
elv |
⊢ ( 𝑟 ∈ Rels ↔ ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) = 𝑟 ) |
9 |
8
|
biimpi |
⊢ ( 𝑟 ∈ Rels → ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) = 𝑟 ) |
10 |
9
|
cnveqd |
⊢ ( 𝑟 ∈ Rels → ◡ ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) = ◡ 𝑟 ) |
11 |
10 9
|
sseq12d |
⊢ ( 𝑟 ∈ Rels → ( ◡ ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) ⊆ ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) ↔ ◡ 𝑟 ⊆ 𝑟 ) ) |
12 |
6 11
|
syl5bb |
⊢ ( 𝑟 ∈ Rels → ( ◡ ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) S ( 𝑟 ∩ ( dom 𝑟 × ran 𝑟 ) ) ↔ ◡ 𝑟 ⊆ 𝑟 ) ) |
13 |
1 2 12
|
abeqinbi |
⊢ SymRels = { 𝑟 ∈ Rels ∣ ◡ 𝑟 ⊆ 𝑟 } |