Theorem iss2

Description: A subclass of the identity relation is the intersection of identity relation with Cartesian product of the domain and range of the class. (Contributed by Peter Mazsa, 22-Jul-2019)

	Ref	Expression
Assertion	iss2	|- ( A C_ _I <-> A = ( _I i^i ( dom A X. ran A ) ) )

Proof

Step	Hyp	Ref	Expression
1		ssel	|- ( A C_ _I -> ( <. x , y >. e. A -> <. x , y >. e. _I ) )
2		vex	|- x e. _V
3		vex	|- y e. _V
4	2 3	opeldm	|- ( <. x , y >. e. A -> x e. dom A )
5	1 4	jca2	|- ( A C_ _I -> ( <. x , y >. e. A -> ( <. x , y >. e. _I /\ x e. dom A ) ) )
6	2 3	opelrn	|- ( <. x , y >. e. A -> y e. ran A )
7	1 6	jca2	|- ( A C_ _I -> ( <. x , y >. e. A -> ( <. x , y >. e. _I /\ y e. ran A ) ) )
8	5 7	jcad	|- ( A C_ _I -> ( <. x , y >. e. A -> ( ( <. x , y >. e. _I /\ x e. dom A ) /\ ( <. x , y >. e. _I /\ y e. ran A ) ) ) )
9		anandi	|- ( ( <. x , y >. e. _I /\ ( x e. dom A /\ y e. ran A ) ) <-> ( ( <. x , y >. e. _I /\ x e. dom A ) /\ ( <. x , y >. e. _I /\ y e. ran A ) ) )
10	8 9	syl6ibr	|- ( A C_ _I -> ( <. x , y >. e. A -> ( <. x , y >. e. _I /\ ( x e. dom A /\ y e. ran A ) ) ) )
11		df-br	|- ( x _I y <-> <. x , y >. e. _I )
12	3	ideq	|- ( x _I y <-> x = y )
13	11 12	bitr3i	|- ( <. x , y >. e. _I <-> x = y )
14	2	eldm2	|- ( x e. dom A <-> E. y <. x , y >. e. A )
15		opeq2	|- ( x = y -> <. x , x >. = <. x , y >. )
16	15	eleq1d	|- ( x = y -> ( <. x , x >. e. A <-> <. x , y >. e. A ) )
17	16	biimprcd	|- ( <. x , y >. e. A -> ( x = y -> <. x , x >. e. A ) )
18	13 17	syl5bi	|- ( <. x , y >. e. A -> ( <. x , y >. e. _I -> <. x , x >. e. A ) )
19	1 18	sylcom	|- ( A C_ _I -> ( <. x , y >. e. A -> <. x , x >. e. A ) )
20	19	exlimdv	|- ( A C_ _I -> ( E. y <. x , y >. e. A -> <. x , x >. e. A ) )
21	14 20	syl5bi	|- ( A C_ _I -> ( x e. dom A -> <. x , x >. e. A ) )
22	16	imbi2d	|- ( x = y -> ( ( x e. dom A -> <. x , x >. e. A ) <-> ( x e. dom A -> <. x , y >. e. A ) ) )
23	21 22	syl5ibcom	|- ( A C_ _I -> ( x = y -> ( x e. dom A -> <. x , y >. e. A ) ) )
24	23	imp	|- ( ( A C_ _I /\ x = y ) -> ( x e. dom A -> <. x , y >. e. A ) )
25	24	adantrd	|- ( ( A C_ _I /\ x = y ) -> ( ( x e. dom A /\ y e. ran A ) -> <. x , y >. e. A ) )
26	25	ex	|- ( A C_ _I -> ( x = y -> ( ( x e. dom A /\ y e. ran A ) -> <. x , y >. e. A ) ) )
27	13 26	syl5bi	|- ( A C_ _I -> ( <. x , y >. e. _I -> ( ( x e. dom A /\ y e. ran A ) -> <. x , y >. e. A ) ) )
28	27	impd	|- ( A C_ _I -> ( ( <. x , y >. e. _I /\ ( x e. dom A /\ y e. ran A ) ) -> <. x , y >. e. A ) )
29	10 28	impbid	|- ( A C_ _I -> ( <. x , y >. e. A <-> ( <. x , y >. e. _I /\ ( x e. dom A /\ y e. ran A ) ) ) )
30		opelinxp	|- ( <. x , y >. e. ( _I i^i ( dom A X. ran A ) ) <-> ( ( x e. dom A /\ y e. ran A ) /\ <. x , y >. e. _I ) )
31	30	biancomi	|- ( <. x , y >. e. ( _I i^i ( dom A X. ran A ) ) <-> ( <. x , y >. e. _I /\ ( x e. dom A /\ y e. ran A ) ) )
32	29 31	bitr4di	|- ( A C_ _I -> ( <. x , y >. e. A <-> <. x , y >. e. ( _I i^i ( dom A X. ran A ) ) ) )
33	32	alrimivv	|- ( A C_ _I -> A. x A. y ( <. x , y >. e. A <-> <. x , y >. e. ( _I i^i ( dom A X. ran A ) ) ) )
34		reli	|- Rel _I
35		relss	|- ( A C_ _I -> ( Rel _I -> Rel A ) )
36	34 35	mpi	|- ( A C_ _I -> Rel A )
37		relinxp	|- Rel ( _I i^i ( dom A X. ran A ) )
38		eqrel	|- ( ( Rel A /\ Rel ( _I i^i ( dom A X. ran A ) ) ) -> ( A = ( _I i^i ( dom A X. ran A ) ) <-> A. x A. y ( <. x , y >. e. A <-> <. x , y >. e. ( _I i^i ( dom A X. ran A ) ) ) ) )
39	36 37 38	sylancl	|- ( A C_ _I -> ( A = ( _I i^i ( dom A X. ran A ) ) <-> A. x A. y ( <. x , y >. e. A <-> <. x , y >. e. ( _I i^i ( dom A X. ran A ) ) ) ) )
40	33 39	mpbird	|- ( A C_ _I -> A = ( _I i^i ( dom A X. ran A ) ) )
41		inss1	|- ( _I i^i ( dom A X. ran A ) ) C_ _I
42		sseq1	|- ( A = ( _I i^i ( dom A X. ran A ) ) -> ( A C_ _I <-> ( _I i^i ( dom A X. ran A ) ) C_ _I ) )
43	41 42	mpbiri	|- ( A = ( _I i^i ( dom A X. ran A ) ) -> A C_ _I )
44	40 43	impbii	|- ( A C_ _I <-> A = ( _I i^i ( dom A X. ran A ) ) )