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 1 st B ran F × 𝒫 ran A -1
Assertion domss2 F : A 1-1 B A V B W G : B 1-1 onto ran G A ran G G F = I A

Proof

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