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	|- ( _I |` dom A ) C_ ( `' A o. A )

Proof

Step	Hyp	Ref	Expression
1		relres	|- Rel ( _I |` dom A )
2		vex	|- y e. _V
3	2	brresi	|- ( x ( _I |` dom A ) y <-> ( x e. dom A /\ x _I y ) )
4		vex	|- x e. _V
5	4	eldm	|- ( x e. dom A <-> E. z x A z )
6		vex	|- z e. _V
7	6 4	brcnv	|- ( z `' A x <-> x A z )
8	4 6 4	brcoi	|- ( ( x A z /\ z `' A x ) -> x ( `' A o. A ) x )
9	7 8	sylan2br	|- ( ( x A z /\ x A z ) -> x ( `' A o. A ) x )
10	9	anidms	|- ( x A z -> x ( `' A o. A ) x )
11	10	exlimiv	|- ( E. z x A z -> x ( `' A o. A ) x )
12	5 11	sylbi	|- ( x e. dom A -> x ( `' A o. A ) x )
13	2	ideq	|- ( x _I y <-> x = y )
14		breq2	|- ( x = y -> ( x ( `' A o. A ) x <-> x ( `' A o. A ) y ) )
15	13 14	sylbi	|- ( x _I y -> ( x ( `' A o. A ) x <-> x ( `' A o. A ) y ) )
16	15	biimpac	|- ( ( x ( `' A o. A ) x /\ x _I y ) -> x ( `' A o. A ) y )
17	12 16	sylan	|- ( ( x e. dom A /\ x _I y ) -> x ( `' A o. A ) y )
18	3 17	sylbi	|- ( x ( _I |` dom A ) y -> x ( `' A o. A ) y )
19		df-br	|- ( x ( _I |` dom A ) y <-> <. x , y >. e. ( _I |` dom A ) )
20		df-br	|- ( x ( `' A o. A ) y <-> <. x , y >. e. ( `' A o. A ) )
21	18 19 20	3imtr3i	|- ( <. x , y >. e. ( _I |` dom A ) -> <. x , y >. e. ( `' A o. A ) )
22	1 21	relssi	|- ( _I |` dom A ) C_ ( `' A o. A )