Metamath Proof Explorer

Theorem psdmrn

Description: The domain and range of a poset equal its field. (Contributed by NM, 13-May-2008)

Ref Expression
Assertion psdmrn ⊢ R ∈ PosetRel → dom ⁡ R = ⋃ ⋃ R ∧ ran ⁡ R = ⋃ ⋃ R

Proof

Step Hyp Ref Expression
1 ssun1 ⊢ dom ⁡ R ⊆ dom ⁡ R ∪ ran ⁡ R
2 dmrnssfld ⊢ dom ⁡ R ∪ ran ⁡ R ⊆ ⋃ ⋃ R
3 1 2 sstri ⊢ dom ⁡ R ⊆ ⋃ ⋃ R
4 3 a1i ⊢ R ∈ PosetRel → dom ⁡ R ⊆ ⋃ ⋃ R
5 pslem ⊢ R ∈ PosetRel → x R x ∧ x R x → x R x ∧ x ∈ ⋃ ⋃ R → x R x ∧ x R x ∧ x R x → x = x
6 5 simp2d ⊢ R ∈ PosetRel → x ∈ ⋃ ⋃ R → x R x
7 vex ⊢ x ∈ V
8 7 7 breldm ⊢ x R x → x ∈ dom ⁡ R
9 6 8 syl6 ⊢ R ∈ PosetRel → x ∈ ⋃ ⋃ R → x ∈ dom ⁡ R
10 9 ssrdv ⊢ R ∈ PosetRel → ⋃ ⋃ R ⊆ dom ⁡ R
11 4 10 eqssd ⊢ R ∈ PosetRel → dom ⁡ R = ⋃ ⋃ R
12 ssun2 ⊢ ran ⁡ R ⊆ dom ⁡ R ∪ ran ⁡ R
13 12 2 sstri ⊢ ran ⁡ R ⊆ ⋃ ⋃ R
14 13 a1i ⊢ R ∈ PosetRel → ran ⁡ R ⊆ ⋃ ⋃ R
15 7 7 brelrn ⊢ x R x → x ∈ ran ⁡ R
16 6 15 syl6 ⊢ R ∈ PosetRel → x ∈ ⋃ ⋃ R → x ∈ ran ⁡ R
17 16 ssrdv ⊢ R ∈ PosetRel → ⋃ ⋃ R ⊆ ran ⁡ R
18 14 17 eqssd ⊢ R ∈ PosetRel → ran ⁡ R = ⋃ ⋃ R
19 11 18 jca ⊢ R ∈ PosetRel → dom ⁡ R = ⋃ ⋃ R ∧ ran ⁡ R = ⋃ ⋃ R