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 𝑅 = ∪ ∪ 𝑅 ) )