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

Metamath Proof Explorer

Theorem dfdm2

Description: Alternate definition of domain df-dm that doesn't require dummy variables. (Contributed by NM, 2-Aug-2010)

Ref Expression
Assertion dfdm2 
|- dom A = U. U. ( `' A o. A )

Proof

Step Hyp Ref Expression
1 cnvco 
 |-  `' ( `' A o. A ) = ( `' A o. `' `' A )
2 cocnvcnv2 
 |-  ( `' A o. `' `' A ) = ( `' A o. A )
3 1 2 eqtri 
 |-  `' ( `' A o. A ) = ( `' A o. A )
4 3 unieqi 
 |-  U. `' ( `' A o. A ) = U. ( `' A o. A )
5 4 unieqi 
 |-  U. U. `' ( `' A o. A ) = U. U. ( `' A o. A )
6 unidmrn 
 |-  U. U. `' ( `' A o. A ) = ( dom ( `' A o. A ) u. ran ( `' A o. A ) )
7 5 6 eqtr3i 
 |-  U. U. ( `' A o. A ) = ( dom ( `' A o. A ) u. ran ( `' A o. A ) )
8 df-rn 
 |-  ran A = dom `' A
9 8 eqcomi 
 |-  dom `' A = ran A
10 dmcoeq 
 |-  ( dom `' A = ran A -> dom ( `' A o. A ) = dom A )
11 9 10 ax-mp 
 |-  dom ( `' A o. A ) = dom A
12 rncoeq 
 |-  ( dom `' A = ran A -> ran ( `' A o. A ) = ran `' A )
13 9 12 ax-mp 
 |-  ran ( `' A o. A ) = ran `' A
14 dfdm4 
 |-  dom A = ran `' A
15 13 14 eqtr4i 
 |-  ran ( `' A o. A ) = dom A
16 11 15 uneq12i 
 |-  ( dom ( `' A o. A ) u. ran ( `' A o. A ) ) = ( dom A u. dom A )
17 unidm 
 |-  ( dom A u. dom A ) = dom A
18 7 16 17 3eqtrri 
 |-  dom A = U. U. ( `' A o. A )