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 = ⋃ ⋃ A -1 ∘ A

Proof

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