Theorem usgrexilem

Description: Lemma for usgrexi . (Contributed by AV, 12-Jan-2018) (Revised by AV, 10-Nov-2021)

	Ref	Expression
Hypothesis	usgrexi.p	|- P = { x e. ~P V | ( # ` x ) = 2 }
Assertion	usgrexilem	|- ( V e. W -> ( _I |` P ) : dom ( _I |` P ) -1-1-> { x e. ~P V | ( # ` x ) = 2 } )

Proof

Step	Hyp	Ref	Expression
1		usgrexi.p	|- P = { x e. ~P V | ( # ` x ) = 2 }
2		f1oi	|- ( _I |` P ) : P -1-1-onto-> P
3		f1of1	|- ( ( _I |` P ) : P -1-1-onto-> P -> ( _I |` P ) : P -1-1-> P )
4	2 3	ax-mp	|- ( _I |` P ) : P -1-1-> P
5		dmresi	|- dom ( _I |` P ) = P
6		f1eq2	|- ( dom ( _I |` P ) = P -> ( ( _I |` P ) : dom ( _I |` P ) -1-1-> P <-> ( _I |` P ) : P -1-1-> P ) )
7	5 6	ax-mp	|- ( ( _I |` P ) : dom ( _I |` P ) -1-1-> P <-> ( _I |` P ) : P -1-1-> P )
8	4 7	mpbir	|- ( _I |` P ) : dom ( _I |` P ) -1-1-> P
9	1	eqcomi	|- { x e. ~P V | ( # ` x ) = 2 } = P
10		f1eq3	|- ( { x e. ~P V | ( # ` x ) = 2 } = P -> ( ( _I |` P ) : dom ( _I |` P ) -1-1-> { x e. ~P V | ( # ` x ) = 2 } <-> ( _I |` P ) : dom ( _I |` P ) -1-1-> P ) )
11	9 10	mp1i	|- ( V e. W -> ( ( _I |` P ) : dom ( _I |` P ) -1-1-> { x e. ~P V | ( # ` x ) = 2 } <-> ( _I |` P ) : dom ( _I |` P ) -1-1-> P ) )
12	8 11	mpbiri	|- ( V e. W -> ( _I |` P ) : dom ( _I |` P ) -1-1-> { x e. ~P V | ( # ` x ) = 2 } )