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

Metamath Proof Explorer

Theorem relcnvfld

Description: if R is a relation, its double union equals the double union of its converse. (Contributed by FL, 5-Jan-2009)

		Ref	Expression
	Assertion	relcnvfld	$⊢ Rel R \to ⋃ ⋃ R = ⋃ ⋃ R^{-1}$

Step	Hyp	Ref	Expression
1		relfld	$⊢ Rel R \to ⋃ ⋃ R = dom R \cup ran R$
2		unidmrn	$⊢ ⋃ ⋃ R^{-1} = dom R \cup ran R$
3	1 2	eqtr4di	$⊢ Rel R \to ⋃ ⋃ R = ⋃ ⋃ R^{-1}$