Theorem bj-idres

Description: Alternate expression for the restricted identity relation. The advantage of that expression is to expose it as a "bounded" class, being included in the Cartesian square of the restricting class. (Contributed by BJ, 27-Dec-2023)

This is an alternate of idinxpresid (see idinxpres ). See also elrid and elidinxp . (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-idres	|- ( _I |` A ) = ( _I i^i ( A X. A ) )

Proof

Step	Hyp	Ref	Expression
1		df-res	|- ( _I |` A ) = ( _I i^i ( A X. _V ) )
2		inss1	|- ( _I i^i ( A X. _V ) ) C_ _I
3		relinxp	|- Rel ( _I i^i ( A X. _V ) )
4		elin	|- ( <. x , y >. e. ( _I i^i ( A X. _V ) ) <-> ( <. x , y >. e. _I /\ <. x , y >. e. ( A X. _V ) ) )
5		bj-opelidb1	|- ( <. x , y >. e. _I <-> ( x e. _V /\ x = y ) )
6	5	simprbi	|- ( <. x , y >. e. _I -> x = y )
7		opelxp1	|- ( <. x , y >. e. ( A X. _V ) -> x e. A )
8		simpr	|- ( ( x = y /\ x e. A ) -> x e. A )
9		eleq1w	|- ( x = y -> ( x e. A <-> y e. A ) )
10	9	biimpa	|- ( ( x = y /\ x e. A ) -> y e. A )
11	8 10	jca	|- ( ( x = y /\ x e. A ) -> ( x e. A /\ y e. A ) )
12	6 7 11	syl2an	|- ( ( <. x , y >. e. _I /\ <. x , y >. e. ( A X. _V ) ) -> ( x e. A /\ y e. A ) )
13	4 12	sylbi	|- ( <. x , y >. e. ( _I i^i ( A X. _V ) ) -> ( x e. A /\ y e. A ) )
14		opelxpi	|- ( ( x e. A /\ y e. A ) -> <. x , y >. e. ( A X. A ) )
15	13 14	syl	|- ( <. x , y >. e. ( _I i^i ( A X. _V ) ) -> <. x , y >. e. ( A X. A ) )
16	3 15	relssi	|- ( _I i^i ( A X. _V ) ) C_ ( A X. A )
17	2 16	ssini	|- ( _I i^i ( A X. _V ) ) C_ ( _I i^i ( A X. A ) )
18		ssv	|- A C_ _V
19		xpss2	|- ( A C_ _V -> ( A X. A ) C_ ( A X. _V ) )
20		sslin	|- ( ( A X. A ) C_ ( A X. _V ) -> ( _I i^i ( A X. A ) ) C_ ( _I i^i ( A X. _V ) ) )
21	18 19 20	mp2b	|- ( _I i^i ( A X. A ) ) C_ ( _I i^i ( A X. _V ) )
22	17 21	eqssi	|- ( _I i^i ( A X. _V ) ) = ( _I i^i ( A X. A ) )
23	1 22	eqtri	|- ( _I |` A ) = ( _I i^i ( A X. A ) )