Theorem unidmrn

Description: The double union of the converse of a class is its field. (Contributed by NM, 4-Jun-2008)

	Ref	Expression
Assertion	unidmrn	⊢ ∪ ∪ ◡ 𝐴 = ( dom 𝐴 ∪ ran 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		relcnv	⊢ Rel ◡ 𝐴
2		relfld	⊢ ( Rel ◡ 𝐴 → ∪ ∪ ◡ 𝐴 = ( dom ◡ 𝐴 ∪ ran ◡ 𝐴 ) )
3	1 2	ax-mp	⊢ ∪ ∪ ◡ 𝐴 = ( dom ◡ 𝐴 ∪ ran ◡ 𝐴 )
4	3	equncomi	⊢ ∪ ∪ ◡ 𝐴 = ( ran ◡ 𝐴 ∪ dom ◡ 𝐴 )
5		dfdm4	⊢ dom 𝐴 = ran ◡ 𝐴
6		df-rn	⊢ ran 𝐴 = dom ◡ 𝐴
7	5 6	uneq12i	⊢ ( dom 𝐴 ∪ ran 𝐴 ) = ( ran ◡ 𝐴 ∪ dom ◡ 𝐴 )
8	4 7	eqtr4i	⊢ ∪ ∪ ◡ 𝐴 = ( dom 𝐴 ∪ ran 𝐴 )