Theorem istsr2

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	istsr2	⊢ ( 𝑅 ∈ TosetRel ↔ ( 𝑅 ∈ PosetRel ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑅 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		istsr.1	⊢ 𝑋 = dom 𝑅
2	1	istsr	⊢ ( 𝑅 ∈ TosetRel ↔ ( 𝑅 ∈ PosetRel ∧ ( 𝑋 × 𝑋 ) ⊆ ( 𝑅 ∪ ◡ 𝑅 ) ) )
3		qfto	⊢ ( ( 𝑋 × 𝑋 ) ⊆ ( 𝑅 ∪ ◡ 𝑅 ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑅 𝑦 ∨ 𝑦 𝑅 𝑥 ) )
4	3	anbi2i	⊢ ( ( 𝑅 ∈ PosetRel ∧ ( 𝑋 × 𝑋 ) ⊆ ( 𝑅 ∪ ◡ 𝑅 ) ) ↔ ( 𝑅 ∈ PosetRel ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑅 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) )
5	2 4	bitri	⊢ ( 𝑅 ∈ TosetRel ↔ ( 𝑅 ∈ PosetRel ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑅 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) )