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