This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem istsr

Description: The predicate is a toset. (Contributed by FL, 1-Nov-2009) (Revised by Mario Carneiro, 22-Nov-2013)

Ref Expression
Hypothesis istsr.1 ⊢ 𝑋 = dom 𝑅
Assertion istsr ( 𝑅 ∈ TosetRel ↔ ( 𝑅 ∈ PosetRel ∧ ( 𝑋 × 𝑋 ) ⊆ ( 𝑅 ∪ ◡ 𝑅 ) ) )

Proof

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 ∧ ( 𝑋 × 𝑋 ) ⊆ ( 𝑅 ∪ ◡ 𝑅 ) ) )