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