Metamath Proof Explorer

Theorem domss2

Description: A corollary of disjenex . If F is an injection from A to B then G is a right inverse 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
Hypothesis domss2.1 
|- G = `' ( F u. ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) )
Assertion domss2 
|- ( ( F : A -1-1-> B /\ A e. V /\ B e. W ) -> ( G : B -1-1-onto-> ran G /\ A C_ ran G /\ ( G o. F ) = ( _I |` A ) ) )

Proof

Step Hyp Ref Expression
1 domss2.1 
 |-  G = `' ( F u. ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) )
2 f1f1orn 
 |-  ( F : A -1-1-> B -> F : A -1-1-onto-> ran F )
3 2 3ad2ant1 
 |-  ( ( F : A -1-1-> B /\ A e. V /\ B e. W ) -> F : A -1-1-onto-> ran F )
4 simp2 
 |-  ( ( F : A -1-1-> B /\ A e. V /\ B e. W ) -> A e. V )
5 rnexg 
 |-  ( A e. V -> ran A e. _V )
6 4 5 syl 
 |-  ( ( F : A -1-1-> B /\ A e. V /\ B e. W ) -> ran A e. _V )
7 uniexg 
 |-  ( ran A e. _V -> U. ran A e. _V )
8 pwexg 
 |-  ( U. ran A e. _V -> ~P U. ran A e. _V )
9 6 7 8 3syl 
 |-  ( ( F : A -1-1-> B /\ A e. V /\ B e. W ) -> ~P U. ran A e. _V )
10 1stconst 
 |-  ( ~P U. ran A e. _V -> ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) : ( ( B \ ran F ) X. { ~P U. ran A } ) -1-1-onto-> ( B \ ran F ) )
11 9 10 syl 
 |-  ( ( F : A -1-1-> B /\ A e. V /\ B e. W ) -> ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) : ( ( B \ ran F ) X. { ~P U. ran A } ) -1-1-onto-> ( B \ ran F ) )
12 difexg 
 |-  ( B e. W -> ( B \ ran F ) e. _V )
13 12 3ad2ant3 
 |-  ( ( F : A -1-1-> B /\ A e. V /\ B e. W ) -> ( B \ ran F ) e. _V )
14 disjen 
 |-  ( ( A e. V /\ ( B \ ran F ) e. _V ) -> ( ( A i^i ( ( B \ ran F ) X. { ~P U. ran A } ) ) = (/) /\ ( ( B \ ran F ) X. { ~P U. ran A } ) ~~ ( B \ ran F ) ) )
15 4 13 14 syl2anc 
 |-  ( ( F : A -1-1-> B /\ A e. V /\ B e. W ) -> ( ( A i^i ( ( B \ ran F ) X. { ~P U. ran A } ) ) = (/) /\ ( ( B \ ran F ) X. { ~P U. ran A } ) ~~ ( B \ ran F ) ) )
16 15 simpld 
 |-  ( ( F : A -1-1-> B /\ A e. V /\ B e. W ) -> ( A i^i ( ( B \ ran F ) X. { ~P U. ran A } ) ) = (/) )
17 disjdif 
 |-  ( ran F i^i ( B \ ran F ) ) = (/)
18 17 a1i 
 |-  ( ( F : A -1-1-> B /\ A e. V /\ B e. W ) -> ( ran F i^i ( B \ ran F ) ) = (/) )
19 f1oun 
 |-  ( ( ( F : A -1-1-onto-> ran F /\ ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) : ( ( B \ ran F ) X. { ~P U. ran A } ) -1-1-onto-> ( B \ ran F ) ) /\ ( ( A i^i ( ( B \ ran F ) X. { ~P U. ran A } ) ) = (/) /\ ( ran F i^i ( B \ ran F ) ) = (/) ) ) -> ( F u. ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) ) : ( A u. ( ( B \ ran F ) X. { ~P U. ran A } ) ) -1-1-onto-> ( ran F u. ( B \ ran F ) ) )
20 3 11 16 18 19 syl22anc 
 |-  ( ( F : A -1-1-> B /\ A e. V /\ B e. W ) -> ( F u. ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) ) : ( A u. ( ( B \ ran F ) X. { ~P U. ran A } ) ) -1-1-onto-> ( ran F u. ( B \ ran F ) ) )
21 undif2 
 |-  ( ran F u. ( B \ ran F ) ) = ( ran F u. B )
22 f1f 
 |-  ( F : A -1-1-> B -> F : A --> B )
23 22 3ad2ant1 
 |-  ( ( F : A -1-1-> B /\ A e. V /\ B e. W ) -> F : A --> B )
24 23 frnd 
 |-  ( ( F : A -1-1-> B /\ A e. V /\ B e. W ) -> ran F C_ B )
25 ssequn1 
 |-  ( ran F C_ B <-> ( ran F u. B ) = B )
26 24 25 sylib 
 |-  ( ( F : A -1-1-> B /\ A e. V /\ B e. W ) -> ( ran F u. B ) = B )
27 21 26 eqtrid 
 |-  ( ( F : A -1-1-> B /\ A e. V /\ B e. W ) -> ( ran F u. ( B \ ran F ) ) = B )
28 27 f1oeq3d 
 |-  ( ( F : A -1-1-> B /\ A e. V /\ B e. W ) -> ( ( F u. ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) ) : ( A u. ( ( B \ ran F ) X. { ~P U. ran A } ) ) -1-1-onto-> ( ran F u. ( B \ ran F ) ) <-> ( F u. ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) ) : ( A u. ( ( B \ ran F ) X. { ~P U. ran A } ) ) -1-1-onto-> B ) )
29 20 28 mpbid 
 |-  ( ( F : A -1-1-> B /\ A e. V /\ B e. W ) -> ( F u. ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) ) : ( A u. ( ( B \ ran F ) X. { ~P U. ran A } ) ) -1-1-onto-> B )
30 f1ocnv 
 |-  ( ( F u. ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) ) : ( A u. ( ( B \ ran F ) X. { ~P U. ran A } ) ) -1-1-onto-> B -> `' ( F u. ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) ) : B -1-1-onto-> ( A u. ( ( B \ ran F ) X. { ~P U. ran A } ) ) )
31 29 30 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-onto-> ( A u. ( ( B \ ran F ) X. { ~P U. ran A } ) ) )
32 f1oeq1 
 |-  ( G = `' ( F u. ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) ) -> ( G : B -1-1-onto-> ( A u. ( ( B \ ran F ) X. { ~P U. ran A } ) ) <-> `' ( F u. ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) ) : B -1-1-onto-> ( A u. ( ( B \ ran F ) X. { ~P U. ran A } ) ) ) )
33 1 32 ax-mp 
 |-  ( G : B -1-1-onto-> ( A u. ( ( B \ ran F ) X. { ~P U. ran A } ) ) <-> `' ( F u. ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) ) : B -1-1-onto-> ( A u. ( ( B \ ran F ) X. { ~P U. ran A } ) ) )
34 31 33 sylibr 
 |-  ( ( F : A -1-1-> B /\ A e. V /\ B e. W ) -> G : B -1-1-onto-> ( A u. ( ( B \ ran F ) X. { ~P U. ran A } ) ) )
35 f1ofo 
 |-  ( G : B -1-1-onto-> ( A u. ( ( B \ ran F ) X. { ~P U. ran A } ) ) -> G : B -onto-> ( A u. ( ( B \ ran F ) X. { ~P U. ran A } ) ) )
36 forn 
 |-  ( G : B -onto-> ( A u. ( ( B \ ran F ) X. { ~P U. ran A } ) ) -> ran G = ( A u. ( ( B \ ran F ) X. { ~P U. ran A } ) ) )
37 34 35 36 3syl 
 |-  ( ( F : A -1-1-> B /\ A e. V /\ B e. W ) -> ran G = ( A u. ( ( B \ ran F ) X. { ~P U. ran A } ) ) )
38 37 f1oeq3d 
 |-  ( ( F : A -1-1-> B /\ A e. V /\ B e. W ) -> ( G : B -1-1-onto-> ran G <-> G : B -1-1-onto-> ( A u. ( ( B \ ran F ) X. { ~P U. ran A } ) ) ) )
39 34 38 mpbird 
 |-  ( ( F : A -1-1-> B /\ A e. V /\ B e. W ) -> G : B -1-1-onto-> ran G )
40 ssun1 
 |-  A C_ ( A u. ( ( B \ ran F ) X. { ~P U. ran A } ) )
41 40 37 sseqtrrid 
 |-  ( ( F : A -1-1-> B /\ A e. V /\ B e. W ) -> A C_ ran G )
42 ssid 
 |-  ran F C_ ran F
43 cores 
 |-  ( ran F C_ ran F -> ( ( G |` ran F ) o. F ) = ( G o. F ) )
44 42 43 ax-mp 
 |-  ( ( G |` ran F ) o. F ) = ( G o. F )
45 dmres 
 |-  dom ( `' ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) |` ran F ) = ( ran F i^i dom `' ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) )
46 f1ocnv 
 |-  ( ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) : ( ( B \ ran F ) X. { ~P U. ran A } ) -1-1-onto-> ( B \ ran F ) -> `' ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) : ( B \ ran F ) -1-1-onto-> ( ( B \ ran F ) X. { ~P U. ran A } ) )
47 f1odm 
 |-  ( `' ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) : ( B \ ran F ) -1-1-onto-> ( ( B \ ran F ) X. { ~P U. ran A } ) -> dom `' ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) = ( B \ ran F ) )
48 11 46 47 3syl 
 |-  ( ( F : A -1-1-> B /\ A e. V /\ B e. W ) -> dom `' ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) = ( B \ ran F ) )
49 48 ineq2d 
 |-  ( ( F : A -1-1-> B /\ A e. V /\ B e. W ) -> ( ran F i^i dom `' ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) ) = ( ran F i^i ( B \ ran F ) ) )
50 49 17 eqtrdi 
 |-  ( ( F : A -1-1-> B /\ A e. V /\ B e. W ) -> ( ran F i^i dom `' ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) ) = (/) )
51 45 50 eqtrid 
 |-  ( ( F : A -1-1-> B /\ A e. V /\ B e. W ) -> dom ( `' ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) |` ran F ) = (/) )
52 relres 
 |-  Rel ( `' ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) |` ran F )
53 reldm0 
 |-  ( Rel ( `' ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) |` ran F ) -> ( ( `' ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) |` ran F ) = (/) <-> dom ( `' ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) |` ran F ) = (/) ) )
54 52 53 ax-mp 
 |-  ( ( `' ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) |` ran F ) = (/) <-> dom ( `' ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) |` ran F ) = (/) )
55 51 54 sylibr 
 |-  ( ( F : A -1-1-> B /\ A e. V /\ B e. W ) -> ( `' ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) |` ran F ) = (/) )
56 55 uneq2d 
 |-  ( ( F : A -1-1-> B /\ A e. V /\ B e. W ) -> ( `' F u. ( `' ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) |` ran F ) ) = ( `' F u. (/) ) )
57 cnvun 
 |-  `' ( F u. ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) ) = ( `' F u. `' ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) )
58 1 57 eqtri 
 |-  G = ( `' F u. `' ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) )
59 58 reseq1i 
 |-  ( G |` ran F ) = ( ( `' F u. `' ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) ) |` ran F )
60 resundir 
 |-  ( ( `' F u. `' ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) ) |` ran F ) = ( ( `' F |` ran F ) u. ( `' ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) |` ran F ) )
61 df-rn 
 |-  ran F = dom `' F
62 61 reseq2i 
 |-  ( `' F |` ran F ) = ( `' F |` dom `' F )
63 relcnv 
 |-  Rel `' F
64 resdm 
 |-  ( Rel `' F -> ( `' F |` dom `' F ) = `' F )
65 63 64 ax-mp 
 |-  ( `' F |` dom `' F ) = `' F
66 62 65 eqtri 
 |-  ( `' F |` ran F ) = `' F
67 66 uneq1i 
 |-  ( ( `' F |` ran F ) u. ( `' ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) |` ran F ) ) = ( `' F u. ( `' ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) |` ran F ) )
68 59 60 67 3eqtrri 
 |-  ( `' F u. ( `' ( 1st |` ( ( B \ ran F ) X. { ~P U. ran A } ) ) |` ran F ) ) = ( G |` ran F )
69 un0 
 |-  ( `' F u. (/) ) = `' F
70 56 68 69 3eqtr3g 
 |-  ( ( F : A -1-1-> B /\ A e. V /\ B e. W ) -> ( G |` ran F ) = `' F )
71 70 coeq1d 
 |-  ( ( F : A -1-1-> B /\ A e. V /\ B e. W ) -> ( ( G |` ran F ) o. F ) = ( `' F o. F ) )
72 f1cocnv1 
 |-  ( F : A -1-1-> B -> ( `' F o. F ) = ( _I |` A ) )
73 72 3ad2ant1 
 |-  ( ( F : A -1-1-> B /\ A e. V /\ B e. W ) -> ( `' F o. F ) = ( _I |` A ) )
74 71 73 eqtrd 
 |-  ( ( F : A -1-1-> B /\ A e. V /\ B e. W ) -> ( ( G |` ran F ) o. F ) = ( _I |` A ) )
75 44 74 eqtr3id 
 |-  ( ( F : A -1-1-> B /\ A e. V /\ B e. W ) -> ( G o. F ) = ( _I |` A ) )
76 39 41 75 3jca 
 |-  ( ( F : A -1-1-> B /\ A e. V /\ B e. W ) -> ( G : B -1-1-onto-> ran G /\ A C_ ran G /\ ( G o. F ) = ( _I |` A ) ) )