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