relfld

Description: The double union of a relation is its field. (Contributed by NM, 17-Sep-2006)

		Ref	Expression
	Assertion	relfld	$⊢ Rel R \to ⋃ ⋃ R = dom R \cup ran R$

Step	Hyp	Ref	Expression
1		relssdmrn	$⊢ Rel R \to R \subseteq dom R \times ran R$
2		uniss	$⊢ R \subseteq dom R \times ran R \to ⋃ R \subseteq ⋃ (dom R \times ran R)$
3		uniss	$⊢ ⋃ R \subseteq ⋃ (dom R \times ran R) \to ⋃ ⋃ R \subseteq ⋃ ⋃ (dom R \times ran R)$
4	1 2 3	3syl	$⊢ Rel R \to ⋃ ⋃ R \subseteq ⋃ ⋃ (dom R \times ran R)$
5		unixpss	$⊢ ⋃ ⋃ (dom R \times ran R) \subseteq dom R \cup ran R$
6	4 5	sstrdi	$⊢ Rel R \to ⋃ ⋃ R \subseteq dom R \cup ran R$
7		dmrnssfld	$⊢ dom R \cup ran R \subseteq ⋃ ⋃ R$
8	7	a1i	$⊢ Rel R \to dom R \cup ran R \subseteq ⋃ ⋃ R$
9	6 8	eqssd	$⊢ Rel R \to ⋃ ⋃ R = dom R \cup ran R$

Metamath Proof Explorer