Theorem idresdmsscocnv1

Description: A class postcomposed with its converse includes the identity relation restricted to its domain. (Contributed by BJ, 25-Oct-2026)

	Ref	Expression
Assertion	idresdmsscocnv1	$$⊢{\mathrm{I}\upharpoonright }_{\mathrm{dom}A}\subseteq A^{-1}\circ A$$

Proof

Step	Hyp	Ref	Expression
1		relres	$$⊢\mathrm{Rel}\left({\mathrm{I}\upharpoonright }_{\mathrm{dom}A}\right)$$
2		vex	$$⊢y\in \mathrm{V}$$
3	2	brresi	$$⊢x\left({\mathrm{I}\upharpoonright }_{\mathrm{dom}A}\right)y\leftrightarrow \left(x\in \mathrm{dom}A\wedge x\mathrm{I}y\right)$$
4		vex	$$⊢x\in \mathrm{V}$$
5	4	eldm	$$⊢x\in \mathrm{dom}A\leftrightarrow \exists zxAz$$
6		vex	$$⊢z\in \mathrm{V}$$
7	6 4	brcnv	$$⊢z{A}^{-1}x\leftrightarrow xAz$$
8	4 6 4	brcoi	$$⊢\left(xAz\wedge z{A}^{-1}x\right)\to x\left(A^{-1}\circ A\right)x$$
9	7 8	sylan2br	$$⊢\left(xAz\wedge xAz\right)\to x\left(A^{-1}\circ A\right)x$$
10	9	anidms	$$⊢xAz\to x\left(A^{-1}\circ A\right)x$$
11	10	exlimiv	$$⊢\exists zxAz\to x\left(A^{-1}\circ A\right)x$$
12	5 11	sylbi	$$⊢x\in \mathrm{dom}A\to x\left(A^{-1}\circ A\right)x$$
13	2	ideq	$$⊢x\mathrm{I}y\leftrightarrow x=y$$
14		breq2	$$⊢x=y\to \left(x\left(A^{-1}\circ A\right)x\leftrightarrow x\left(A^{-1}\circ A\right)y\right)$$
15	13 14	sylbi	$$⊢x\mathrm{I}y\to \left(x\left(A^{-1}\circ A\right)x\leftrightarrow x\left(A^{-1}\circ A\right)y\right)$$
16	15	biimpac	$$⊢\left(x\left(A^{-1}\circ A\right)x\wedge x\mathrm{I}y\right)\to x\left(A^{-1}\circ A\right)y$$
17	12 16	sylan	$$⊢\left(x\in \mathrm{dom}A\wedge x\mathrm{I}y\right)\to x\left(A^{-1}\circ A\right)y$$
18	3 17	sylbi	$$⊢x\left({\mathrm{I}\upharpoonright }_{\mathrm{dom}A}\right)y\to x\left(A^{-1}\circ A\right)y$$
19		df-br	$$⊢x\left({\mathrm{I}\upharpoonright }_{\mathrm{dom}A}\right)y\leftrightarrow ⟨x,y⟩\in \left({\mathrm{I}\upharpoonright }_{\mathrm{dom}A}\right)$$
20		df-br	$$⊢x\left(A^{-1}\circ A\right)y\leftrightarrow ⟨x,y⟩\in \left(A^{-1}\circ A\right)$$
21	18 19 20	3imtr3i	$$⊢⟨x,y⟩\in \left({\mathrm{I}\upharpoonright }_{\mathrm{dom}A}\right)\to ⟨x,y⟩\in \left(A^{-1}\circ A\right)$$
22	1 21	relssi	$$⊢{\mathrm{I}\upharpoonright }_{\mathrm{dom}A}\subseteq A^{-1}\circ A$$