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 𝐴 = ∪ ∪ ( ◡ 𝐴 ∘ 𝐴 )

Proof

Step Hyp Ref Expression
1 cnvco ⊢ ◡ ( ◡ 𝐴 ∘ 𝐴 ) = ( ◡ 𝐴 ∘ ◡ ◡ 𝐴 )
2 cocnvcnv2 ⊢ ( ◡ 𝐴 ∘ ◡ ◡ 𝐴 ) = ( ◡ 𝐴 ∘ 𝐴 )
3 1 2 eqtri ⊢ ◡ ( ◡ 𝐴 ∘ 𝐴 ) = ( ◡ 𝐴 ∘ 𝐴 )
4 3 unieqi ⊢ ∪ ◡ ( ◡ 𝐴 ∘ 𝐴 ) = ∪ ( ◡ 𝐴 ∘ 𝐴 )
5 4 unieqi ⊢ ∪ ∪ ◡ ( ◡ 𝐴 ∘ 𝐴 ) = ∪ ∪ ( ◡ 𝐴 ∘ 𝐴 )
6 unidmrn ⊢ ∪ ∪ ◡ ( ◡ 𝐴 ∘ 𝐴 ) = ( dom ( ◡ 𝐴 ∘ 𝐴 ) ∪ ran ( ◡ 𝐴 ∘ 𝐴 ) )
7 5 6 eqtr3i ⊢ ∪ ∪ ( ◡ 𝐴 ∘ 𝐴 ) = ( dom ( ◡ 𝐴 ∘ 𝐴 ) ∪ ran ( ◡ 𝐴 ∘ 𝐴 ) )
8 df-rn ⊢ ran 𝐴 = dom ◡ 𝐴
9 8 eqcomi ⊢ dom ◡ 𝐴 = ran 𝐴
10 dmcoeq ⊢ ( dom ◡ 𝐴 = ran 𝐴 → dom ( ◡ 𝐴 ∘ 𝐴 ) = dom 𝐴 )
11 9 10 ax-mp ⊢ dom ( ◡ 𝐴 ∘ 𝐴 ) = dom 𝐴
12 rncoeq ⊢ ( dom ◡ 𝐴 = ran 𝐴 → ran ( ◡ 𝐴 ∘ 𝐴 ) = ran ◡ 𝐴 )
13 9 12 ax-mp ⊢ ran ( ◡ 𝐴 ∘ 𝐴 ) = ran ◡ 𝐴
14 dfdm4 ⊢ dom 𝐴 = ran ◡ 𝐴
15 13 14 eqtr4i ⊢ ran ( ◡ 𝐴 ∘ 𝐴 ) = dom 𝐴
16 11 15 uneq12i ⊢ ( dom ( ◡ 𝐴 ∘ 𝐴 ) ∪ ran ( ◡ 𝐴 ∘ 𝐴 ) ) = ( dom 𝐴 ∪ dom 𝐴 )
17 unidm ⊢ ( dom 𝐴 ∪ dom 𝐴 ) = dom 𝐴
18 7 16 17 3eqtrri ⊢ dom 𝐴 = ∪ ∪ ( ◡ 𝐴 ∘ 𝐴 )