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