psdmrn

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

		Ref	Expression
	Assertion	psdmrn	$⊢ R \in PosetRel \to (dom R = ⋃ ⋃ R \land ran R = ⋃ ⋃ R)$

Step	Hyp	Ref	Expression
1		ssun1	$⊢ dom R \subseteq dom R \cup ran R$
2		dmrnssfld	$⊢ dom R \cup ran R \subseteq ⋃ ⋃ R$
3	1 2	sstri	$⊢ dom R \subseteq ⋃ ⋃ R$
4	3	a1i	$⊢ R \in PosetRel \to dom R \subseteq ⋃ ⋃ R$
5		pslem	$⊢ R \in PosetRel \to (((x R x \land x R x) \to x R x) \land (x \in ⋃ ⋃ R \to x R x) \land ((x R x \land x R x) \to x = x))$
6	5	simp2d	$⊢ R \in PosetRel \to (x \in ⋃ ⋃ R \to x R x)$
7		vex	$⊢ x \in V$
8	7 7	breldm	$⊢ x R x \to x \in dom R$
9	6 8	syl6	$⊢ R \in PosetRel \to (x \in ⋃ ⋃ R \to x \in dom R)$
10	9	ssrdv	$⊢ R \in PosetRel \to ⋃ ⋃ R \subseteq dom R$
11	4 10	eqssd	$⊢ R \in PosetRel \to dom R = ⋃ ⋃ R$
12		ssun2	$⊢ ran R \subseteq dom R \cup ran R$
13	12 2	sstri	$⊢ ran R \subseteq ⋃ ⋃ R$
14	13	a1i	$⊢ R \in PosetRel \to ran R \subseteq ⋃ ⋃ R$
15	7 7	brelrn	$⊢ x R x \to x \in ran R$
16	6 15	syl6	$⊢ R \in PosetRel \to (x \in ⋃ ⋃ R \to x \in ran R)$
17	16	ssrdv	$⊢ R \in PosetRel \to ⋃ ⋃ R \subseteq ran R$
18	14 17	eqssd	$⊢ R \in PosetRel \to ran R = ⋃ ⋃ R$
19	11 18	jca	$⊢ R \in PosetRel \to (dom R = ⋃ ⋃ R \land ran R = ⋃ ⋃ R)$

Metamath Proof Explorer