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

Metamath Proof Explorer

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 ⊢ ⋃ ⋃ A -1 = dom ⁡ A ∪ ran ⁡ A

Proof

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