This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 } )