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	imbitrrdi	\|- ( 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	biimtrid	\|- ( <. 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	biimtrid	\|- ( 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	biimtrid	\|- ( 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 ) ) )

Metamath Proof Explorer

Theorem iss2

Proof