Metamath Proof Explorer

Theorem domssex2

Description: A corollary of disjenex . If F is an injection from A to B then there is a right inverse g of F from B to a superset of A . (Contributed by Mario Carneiro, 7-Feb-2015) (Revised by Mario Carneiro, 24-Jun-2015)

Ref Expression
Assertion domssex2 
|- ( ( F : A -1-1-> B /\ A e. V /\ B e. W ) -> E. g ( g : B -1-1-> _V /\ ( g o. F ) = ( _I |` A ) ) )

Proof

Step Hyp Ref Expression
1 f1f 
 |-  ( F : A -1-1-> B -> F : A --> B )
2 fex2 
 |-  ( ( F : A --> B /\ A e. V /\ B e. W ) -> F e. _V )
3 1 2 syl3an1 
 |-  ( ( F : A -1-1-> B /\ A e. V /\ B e. W ) -> F e. _V )
4 f1stres 
 |-  ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) : ( ( B \ ran F ) X. { ~P U. ran A } ) --> ( B \ ran F )
5 difexg 
 |-  ( B e. W -> ( B \ ran F ) e. _V )
6 5 3ad2ant3 
 |-  ( ( F : A -1-1-> B /\ A e. V /\ B e. W ) -> ( B \ ran F ) e. _V )
7 snex 
 |-  { ~P U. ran A } e. _V
8 xpexg 
 |-  ( ( ( B \ ran F ) e. _V /\ { ~P U. ran A } e. _V ) -> ( ( B \ ran F ) X. { ~P U. ran A } ) e. _V )
9 6 7 8 sylancl 
 |-  ( ( F : A -1-1-> B /\ A e. V /\ B e. W ) -> ( ( B \ ran F ) X. { ~P U. ran A } ) e. _V )
10 fex2 
 |-  ( ( ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) : ( ( B \ ran F ) X. { ~P U. ran A } ) --> ( B \ ran F ) /\ ( ( B \ ran F ) X. { ~P U. ran A } ) e. _V /\ ( B \ ran F ) e. _V ) -> ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) e. _V )
11 4 9 6 10 mp3an2i 
 |-  ( ( F : A -1-1-> B /\ A e. V /\ B e. W ) -> ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) e. _V )
12 unexg 
 |-  ( ( F e. _V /\ ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) e. _V ) -> ( F u. ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) ) e. _V )
13 3 11 12 syl2anc 
 |-  ( ( F : A -1-1-> B /\ A e. V /\ B e. W ) -> ( F u. ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) ) e. _V )
14 cnvexg 
 |-  ( ( F u. ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) ) e. _V -> `' ( F u. ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) ) e. _V )
15 13 14 syl 
 |-  ( ( F : A -1-1-> B /\ A e. V /\ B e. W ) -> `' ( F u. ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) ) e. _V )
16 eqid 
 |-  `' ( F u. ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) ) = `' ( F u. ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) )
17 16 domss2 
 |-  ( ( F : A -1-1-> B /\ A e. V /\ B e. W ) -> ( `' ( F u. ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) ) : B -1-1-onto-> ran `' ( F u. ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) ) /\ A C_ ran `' ( F u. ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) ) /\ ( `' ( F u. ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) ) o. F ) = ( _I |` A ) ) )
18 17 simp1d 
 |-  ( ( F : A -1-1-> B /\ A e. V /\ B e. W ) -> `' ( F u. ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) ) : B -1-1-onto-> ran `' ( F u. ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) ) )
19 f1of1 
 |-  ( `' ( F u. ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) ) : B -1-1-onto-> ran `' ( F u. ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) ) -> `' ( F u. ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) ) : B -1-1-> ran `' ( F u. ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) ) )
20 18 19 syl 
 |-  ( ( F : A -1-1-> B /\ A e. V /\ B e. W ) -> `' ( F u. ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) ) : B -1-1-> ran `' ( F u. ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) ) )
21 ssv 
 |-  ran `' ( F u. ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) ) C_ _V
22 f1ss 
 |-  ( ( `' ( F u. ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) ) : B -1-1-> ran `' ( F u. ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) ) /\ ran `' ( F u. ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) ) C_ _V ) -> `' ( F u. ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) ) : B -1-1-> _V )
23 20 21 22 sylancl 
 |-  ( ( F : A -1-1-> B /\ A e. V /\ B e. W ) -> `' ( F u. ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) ) : B -1-1-> _V )
24 17 simp3d 
 |-  ( ( F : A -1-1-> B /\ A e. V /\ B e. W ) -> ( `' ( F u. ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) ) o. F ) = ( _I |` A ) )
25 23 24 jca 
 |-  ( ( F : A -1-1-> B /\ A e. V /\ B e. W ) -> ( `' ( F u. ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) ) : B -1-1-> _V /\ ( `' ( F u. ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) ) o. F ) = ( _I |` A ) ) )
26 f1eq1 
 |-  ( g = `' ( F u. ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) ) -> ( g : B -1-1-> _V <-> `' ( F u. ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) ) : B -1-1-> _V ) )
27 coeq1 
 |-  ( g = `' ( F u. ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) ) -> ( g o. F ) = ( `' ( F u. ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) ) o. F ) )
28 27 eqeq1d 
 |-  ( g = `' ( F u. ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) ) -> ( ( g o. F ) = ( _I |` A ) <-> ( `' ( F u. ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) ) o. F ) = ( _I |` A ) ) )
29 26 28 anbi12d 
 |-  ( g = `' ( F u. ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) ) -> ( ( g : B -1-1-> _V /\ ( g o. F ) = ( _I |` A ) ) <-> ( `' ( F u. ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) ) : B -1-1-> _V /\ ( `' ( F u. ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) ) o. F ) = ( _I |` A ) ) ) )
30 15 25 29 spcedv 
 |-  ( ( F : A -1-1-> B /\ A e. V /\ B e. W ) -> E. g ( g : B -1-1-> _V /\ ( g o. F ) = ( _I |` A ) ) )