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	$$⊢\mathrm{dom}A=\bigcup \bigcup \left(A^{-1}\circ A\right)$$

Proof

Step	Hyp	Ref	Expression
1		cnvco	$$⊢{\left(A^{-1}\circ A\right)}^{-1}=A^{-1}\circ {A^{-1}}^{-1}$$
2		cocnvcnv2	$$⊢A^{-1}\circ {A^{-1}}^{-1}=A^{-1}\circ A$$
3	1 2	eqtri	$$⊢{\left(A^{-1}\circ A\right)}^{-1}=A^{-1}\circ A$$
4	3	unieqi	$$⊢\bigcup {\left(A^{-1}\circ A\right)}^{-1}=\bigcup \left(A^{-1}\circ A\right)$$
5	4	unieqi	$$⊢\bigcup \bigcup {\left(A^{-1}\circ A\right)}^{-1}=\bigcup \bigcup \left(A^{-1}\circ A\right)$$
6		unidmrn	$$⊢\bigcup \bigcup {\left(A^{-1}\circ A\right)}^{-1}=\mathrm{dom}\left(A^{-1}\circ A\right)\cup \mathrm{ran}\left(A^{-1}\circ A\right)$$
7	5 6	eqtr3i	$$⊢\bigcup \bigcup \left(A^{-1}\circ A\right)=\mathrm{dom}\left(A^{-1}\circ A\right)\cup \mathrm{ran}\left(A^{-1}\circ A\right)$$
8		dmcocnv1	$$⊢\mathrm{dom}\left(A^{-1}\circ A\right)=\mathrm{dom}A$$
9		rncocnv1	$$⊢\mathrm{ran}\left(A^{-1}\circ A\right)=\mathrm{dom}A$$
10	8 9	uneq12i	$$⊢\mathrm{dom}\left(A^{-1}\circ A\right)\cup \mathrm{ran}\left(A^{-1}\circ A\right)=\mathrm{dom}A\cup \mathrm{dom}A$$
11		unidm	$$⊢\mathrm{dom}A\cup \mathrm{dom}A=\mathrm{dom}A$$
12	7 10 11	3eqtrri	$$⊢\mathrm{dom}A=\bigcup \bigcup \left(A^{-1}\circ A\right)$$