Step |
Hyp |
Ref |
Expression |
1 |
|
istsr.1 |
⊢ 𝑋 = dom 𝑅 |
2 |
|
dmeq |
⊢ ( 𝑟 = 𝑅 → dom 𝑟 = dom 𝑅 ) |
3 |
2 1
|
eqtr4di |
⊢ ( 𝑟 = 𝑅 → dom 𝑟 = 𝑋 ) |
4 |
3
|
sqxpeqd |
⊢ ( 𝑟 = 𝑅 → ( dom 𝑟 × dom 𝑟 ) = ( 𝑋 × 𝑋 ) ) |
5 |
|
id |
⊢ ( 𝑟 = 𝑅 → 𝑟 = 𝑅 ) |
6 |
|
cnveq |
⊢ ( 𝑟 = 𝑅 → ◡ 𝑟 = ◡ 𝑅 ) |
7 |
5 6
|
uneq12d |
⊢ ( 𝑟 = 𝑅 → ( 𝑟 ∪ ◡ 𝑟 ) = ( 𝑅 ∪ ◡ 𝑅 ) ) |
8 |
4 7
|
sseq12d |
⊢ ( 𝑟 = 𝑅 → ( ( dom 𝑟 × dom 𝑟 ) ⊆ ( 𝑟 ∪ ◡ 𝑟 ) ↔ ( 𝑋 × 𝑋 ) ⊆ ( 𝑅 ∪ ◡ 𝑅 ) ) ) |
9 |
|
df-tsr |
⊢ TosetRel = { 𝑟 ∈ PosetRel ∣ ( dom 𝑟 × dom 𝑟 ) ⊆ ( 𝑟 ∪ ◡ 𝑟 ) } |
10 |
8 9
|
elrab2 |
⊢ ( 𝑅 ∈ TosetRel ↔ ( 𝑅 ∈ PosetRel ∧ ( 𝑋 × 𝑋 ) ⊆ ( 𝑅 ∪ ◡ 𝑅 ) ) ) |