Theorem bj-imdiridlem

Description: Lemma for bj-imdirid and bj-iminvid . (Contributed by BJ, 26-May-2024)

	Ref	Expression
Hypothesis	bj-imdiridlem.1	|- ( ( x C_ A /\ y C_ A ) -> ( ph <-> x = y ) )
Assertion	bj-imdiridlem	|- { <. x , y >. | ( ( x C_ A /\ y C_ A ) /\ ph ) } = ( _I |` ~P A )

Proof

Step	Hyp	Ref	Expression
1		bj-imdiridlem.1	|- ( ( x C_ A /\ y C_ A ) -> ( ph <-> x = y ) )
2	1	biimp3a	|- ( ( x C_ A /\ y C_ A /\ ph ) -> x = y )
3	2	3expib	|- ( x C_ A -> ( ( y C_ A /\ ph ) -> x = y ) )
4		equcomi	|- ( x = y -> y = x )
5	4	sseq1d	|- ( x = y -> ( y C_ A <-> x C_ A ) )
6	5	biimparc	|- ( ( x C_ A /\ x = y ) -> y C_ A )
7		simpr	|- ( ( ( x C_ A /\ x = y ) /\ y C_ A ) -> y C_ A )
8	1	biimpar	|- ( ( ( x C_ A /\ y C_ A ) /\ x = y ) -> ph )
9	8	an32s	|- ( ( ( x C_ A /\ x = y ) /\ y C_ A ) -> ph )
10	7 9	jca	|- ( ( ( x C_ A /\ x = y ) /\ y C_ A ) -> ( y C_ A /\ ph ) )
11	6 10	mpdan	|- ( ( x C_ A /\ x = y ) -> ( y C_ A /\ ph ) )
12	11	ex	|- ( x C_ A -> ( x = y -> ( y C_ A /\ ph ) ) )
13	3 12	impbid	|- ( x C_ A -> ( ( y C_ A /\ ph ) <-> x = y ) )
14	13	pm5.32i	|- ( ( x C_ A /\ ( y C_ A /\ ph ) ) <-> ( x C_ A /\ x = y ) )
15		anass	|- ( ( ( x C_ A /\ y C_ A ) /\ ph ) <-> ( x C_ A /\ ( y C_ A /\ ph ) ) )
16		velpw	|- ( x e. ~P A <-> x C_ A )
17		vex	|- y e. _V
18	17	ideq	|- ( x _I y <-> x = y )
19	16 18	anbi12i	|- ( ( x e. ~P A /\ x _I y ) <-> ( x C_ A /\ x = y ) )
20	14 15 19	3bitr4i	|- ( ( ( x C_ A /\ y C_ A ) /\ ph ) <-> ( x e. ~P A /\ x _I y ) )
21	20	opabbii	|- { <. x , y >. | ( ( x C_ A /\ y C_ A ) /\ ph ) } = { <. x , y >. | ( x e. ~P A /\ x _I y ) }
22		dfres2	|- ( _I |` ~P A ) = { <. x , y >. | ( x e. ~P A /\ x _I y ) }
23	21 22	eqtr4i	|- { <. x , y >. | ( ( x C_ A /\ y C_ A ) /\ ph ) } = ( _I |` ~P A )