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		dmcocnv1	⊢ dom ( ◡ 𝐴 ∘ 𝐴 ) = dom 𝐴
9		rncocnv1	⊢ ran ( ◡ 𝐴 ∘ 𝐴 ) = dom 𝐴
10	8 9	uneq12i	⊢ ( dom ( ◡ 𝐴 ∘ 𝐴 ) ∪ ran ( ◡ 𝐴 ∘ 𝐴 ) ) = ( dom 𝐴 ∪ dom 𝐴 )
11		unidm	⊢ ( dom 𝐴 ∪ dom 𝐴 ) = dom 𝐴
12	7 10 11	3eqtrri	⊢ dom 𝐴 = ∪ ∪ ( ◡ 𝐴 ∘ 𝐴 )