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		df-rn	$$⊢\mathrm{ran}A=\mathrm{dom}{A}^{-1}$$
9	8	eqcomi	$$⊢\mathrm{dom}{A}^{-1}=\mathrm{ran}A$$
10		dmcoeq	$$⊢\mathrm{dom}{A}^{-1}=\mathrm{ran}A\to \mathrm{dom}\left(A^{-1}\circ A\right)=\mathrm{dom}A$$
11	9 10	ax-mp	$$⊢\mathrm{dom}\left(A^{-1}\circ A\right)=\mathrm{dom}A$$
12		rncoeq	$$⊢\mathrm{dom}{A}^{-1}=\mathrm{ran}A\to \mathrm{ran}\left(A^{-1}\circ A\right)=\mathrm{ran}{A}^{-1}$$
13	9 12	ax-mp	$$⊢\mathrm{ran}\left(A^{-1}\circ A\right)=\mathrm{ran}{A}^{-1}$$
14		dfdm4	$$⊢\mathrm{dom}A=\mathrm{ran}{A}^{-1}$$
15	13 14	eqtr4i	$$⊢\mathrm{ran}\left(A^{-1}\circ A\right)=\mathrm{dom}A$$
16	11 15	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$$
17		unidm	$$⊢\mathrm{dom}A\cup \mathrm{dom}A=\mathrm{dom}A$$
18	7 16 17	3eqtrri	$$⊢\mathrm{dom}A=\bigcup \bigcup \left(A^{-1}\circ A\right)$$