Metamath Proof Explorer


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 ∧ ∀ 𝑥𝑋𝑦𝑋 ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) ) )