# 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}={\left({F}\cup \left({{1}^{st}↾}_{\left(\left({B}\setminus \mathrm{ran}{F}\right)×\left\{𝒫\bigcup \mathrm{ran}{A}\right\}\right)}\right)\right)}^{-1}$
Assertion domss2 ${⊢}\left({F}:{A}\underset{1-1}{⟶}{B}\wedge {A}\in {V}\wedge {B}\in {W}\right)\to \left({G}:{B}\underset{1-1 onto}{⟶}\mathrm{ran}{G}\wedge {A}\subseteq \mathrm{ran}{G}\wedge {G}\circ {F}={\mathrm{I}↾}_{{A}}\right)$

### Proof

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