Description: The range of a poset equals it domain. (Contributed by NM, 7-Jul-2008)
Ref | Expression | ||
---|---|---|---|
Hypothesis | psref.1 | ⊢ 𝑋 = dom 𝑅 | |
Assertion | psrn | ⊢ ( 𝑅 ∈ PosetRel → 𝑋 = ran 𝑅 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | psref.1 | ⊢ 𝑋 = dom 𝑅 | |
2 | psdmrn | ⊢ ( 𝑅 ∈ PosetRel → ( dom 𝑅 = ∪ ∪ 𝑅 ∧ ran 𝑅 = ∪ ∪ 𝑅 ) ) | |
3 | eqtr3 | ⊢ ( ( dom 𝑅 = ∪ ∪ 𝑅 ∧ ran 𝑅 = ∪ ∪ 𝑅 ) → dom 𝑅 = ran 𝑅 ) | |
4 | 2 3 | syl | ⊢ ( 𝑅 ∈ PosetRel → dom 𝑅 = ran 𝑅 ) |
5 | 1 4 | syl5eq | ⊢ ( 𝑅 ∈ PosetRel → 𝑋 = ran 𝑅 ) |