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 ⊢ X = dom ⁡ R
Assertion istsr2 ⊢ R ∈ TosetRel ↔ R ∈ PosetRel ∧ ∀ x ∈ X ∀ y ∈ X x R y ∨ y R x

Proof

Step Hyp Ref Expression
1 istsr.1 ⊢ X = dom ⁡ R
2 1 istsr ⊢ R ∈ TosetRel ↔ R ∈ PosetRel ∧ X × X ⊆ R ∪ R -1
3 qfto ⊢ X × X ⊆ R ∪ R -1 ↔ ∀ x ∈ X ∀ y ∈ X x R y ∨ y R x
4 3 anbi2i ⊢ R ∈ PosetRel ∧ X × X ⊆ R ∪ R -1 ↔ R ∈ PosetRel ∧ ∀ x ∈ X ∀ y ∈ X x R y ∨ y R x
5 2 4 bitri ⊢ R ∈ TosetRel ↔ R ∈ PosetRel ∧ ∀ x ∈ X ∀ y ∈ X x R y ∨ y R x