This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝑅 ∈ PosetRel → ( dom 𝑅 = ∪ ∪ 𝑅 ∧ ran 𝑅 = ∪ ∪ 𝑅 ) )

Proof

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