# Metamath Proof Explorer

## Theorem uspgrsprfo

Description: The mapping F is a function from the "simple pseudographs" with a fixed set of vertices V onto the subsets of the set of pairs over the set V . (Contributed by AV, 25-Nov-2021)

Ref Expression
Hypotheses uspgrsprf.p ${⊢}{P}=𝒫\mathrm{Pairs}\left({V}\right)$
uspgrsprf.g ${⊢}{G}=\left\{⟨{v},{e}⟩|\left({v}={V}\wedge \exists {q}\in \mathrm{USHGraph}\phantom{\rule{.4em}{0ex}}\left(\mathrm{Vtx}\left({q}\right)={v}\wedge \mathrm{Edg}\left({q}\right)={e}\right)\right)\right\}$
uspgrsprf.f ${⊢}{F}=\left({g}\in {G}⟼{2}^{nd}\left({g}\right)\right)$
Assertion uspgrsprfo ${⊢}{V}\in {W}\to {F}:{G}\underset{onto}{⟶}{P}$

### Proof

Step Hyp Ref Expression
1 uspgrsprf.p ${⊢}{P}=𝒫\mathrm{Pairs}\left({V}\right)$
2 uspgrsprf.g ${⊢}{G}=\left\{⟨{v},{e}⟩|\left({v}={V}\wedge \exists {q}\in \mathrm{USHGraph}\phantom{\rule{.4em}{0ex}}\left(\mathrm{Vtx}\left({q}\right)={v}\wedge \mathrm{Edg}\left({q}\right)={e}\right)\right)\right\}$
3 uspgrsprf.f ${⊢}{F}=\left({g}\in {G}⟼{2}^{nd}\left({g}\right)\right)$
4 1 2 3 uspgrsprf ${⊢}{F}:{G}⟶{P}$
5 4 a1i ${⊢}{V}\in {W}\to {F}:{G}⟶{P}$
6 1 eleq2i ${⊢}{a}\in {P}↔{a}\in 𝒫\mathrm{Pairs}\left({V}\right)$
7 velpw ${⊢}{a}\in 𝒫\mathrm{Pairs}\left({V}\right)↔{a}\subseteq \mathrm{Pairs}\left({V}\right)$
8 6 7 bitri ${⊢}{a}\in {P}↔{a}\subseteq \mathrm{Pairs}\left({V}\right)$
9 eqidd ${⊢}\left({a}\subseteq \mathrm{Pairs}\left({V}\right)\wedge {V}\in {W}\right)\to {V}={V}$
10 vex ${⊢}{a}\in \mathrm{V}$
11 10 a1i ${⊢}\left({a}\subseteq \mathrm{Pairs}\left({V}\right)\wedge {V}\in {W}\right)\to {a}\in \mathrm{V}$
12 f1oi ${⊢}\left({\mathrm{I}↾}_{{a}}\right):{a}\underset{1-1 onto}{⟶}{a}$
13 12 a1i ${⊢}\left({a}\subseteq \mathrm{Pairs}\left({V}\right)\wedge {V}\in {W}\right)\to \left({\mathrm{I}↾}_{{a}}\right):{a}\underset{1-1 onto}{⟶}{a}$
14 dmresi ${⊢}\mathrm{dom}\left({\mathrm{I}↾}_{{a}}\right)={a}$
15 f1oeq2 ${⊢}\mathrm{dom}\left({\mathrm{I}↾}_{{a}}\right)={a}\to \left(\left({\mathrm{I}↾}_{{a}}\right):\mathrm{dom}\left({\mathrm{I}↾}_{{a}}\right)\underset{1-1 onto}{⟶}{a}↔\left({\mathrm{I}↾}_{{a}}\right):{a}\underset{1-1 onto}{⟶}{a}\right)$
16 14 15 ax-mp ${⊢}\left({\mathrm{I}↾}_{{a}}\right):\mathrm{dom}\left({\mathrm{I}↾}_{{a}}\right)\underset{1-1 onto}{⟶}{a}↔\left({\mathrm{I}↾}_{{a}}\right):{a}\underset{1-1 onto}{⟶}{a}$
17 13 16 sylibr ${⊢}\left({a}\subseteq \mathrm{Pairs}\left({V}\right)\wedge {V}\in {W}\right)\to \left({\mathrm{I}↾}_{{a}}\right):\mathrm{dom}\left({\mathrm{I}↾}_{{a}}\right)\underset{1-1 onto}{⟶}{a}$
18 sprvalpwle2 ${⊢}{V}\in {W}\to \mathrm{Pairs}\left({V}\right)=\left\{{p}\in \left(𝒫{V}\setminus \left\{\varnothing \right\}\right)|\left|{p}\right|\le 2\right\}$
19 18 sseq2d ${⊢}{V}\in {W}\to \left({a}\subseteq \mathrm{Pairs}\left({V}\right)↔{a}\subseteq \left\{{p}\in \left(𝒫{V}\setminus \left\{\varnothing \right\}\right)|\left|{p}\right|\le 2\right\}\right)$
20 19 biimpac ${⊢}\left({a}\subseteq \mathrm{Pairs}\left({V}\right)\wedge {V}\in {W}\right)\to {a}\subseteq \left\{{p}\in \left(𝒫{V}\setminus \left\{\varnothing \right\}\right)|\left|{p}\right|\le 2\right\}$
21 17 20 jca ${⊢}\left({a}\subseteq \mathrm{Pairs}\left({V}\right)\wedge {V}\in {W}\right)\to \left(\left({\mathrm{I}↾}_{{a}}\right):\mathrm{dom}\left({\mathrm{I}↾}_{{a}}\right)\underset{1-1 onto}{⟶}{a}\wedge {a}\subseteq \left\{{p}\in \left(𝒫{V}\setminus \left\{\varnothing \right\}\right)|\left|{p}\right|\le 2\right\}\right)$
22 f1oeq3 ${⊢}{f}={a}\to \left(\left({\mathrm{I}↾}_{{a}}\right):\mathrm{dom}\left({\mathrm{I}↾}_{{a}}\right)\underset{1-1 onto}{⟶}{f}↔\left({\mathrm{I}↾}_{{a}}\right):\mathrm{dom}\left({\mathrm{I}↾}_{{a}}\right)\underset{1-1 onto}{⟶}{a}\right)$
23 sseq1 ${⊢}{f}={a}\to \left({f}\subseteq \left\{{p}\in \left(𝒫{V}\setminus \left\{\varnothing \right\}\right)|\left|{p}\right|\le 2\right\}↔{a}\subseteq \left\{{p}\in \left(𝒫{V}\setminus \left\{\varnothing \right\}\right)|\left|{p}\right|\le 2\right\}\right)$
24 22 23 anbi12d ${⊢}{f}={a}\to \left(\left(\left({\mathrm{I}↾}_{{a}}\right):\mathrm{dom}\left({\mathrm{I}↾}_{{a}}\right)\underset{1-1 onto}{⟶}{f}\wedge {f}\subseteq \left\{{p}\in \left(𝒫{V}\setminus \left\{\varnothing \right\}\right)|\left|{p}\right|\le 2\right\}\right)↔\left(\left({\mathrm{I}↾}_{{a}}\right):\mathrm{dom}\left({\mathrm{I}↾}_{{a}}\right)\underset{1-1 onto}{⟶}{a}\wedge {a}\subseteq \left\{{p}\in \left(𝒫{V}\setminus \left\{\varnothing \right\}\right)|\left|{p}\right|\le 2\right\}\right)\right)$
25 11 21 24 elabd ${⊢}\left({a}\subseteq \mathrm{Pairs}\left({V}\right)\wedge {V}\in {W}\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\left(\left({\mathrm{I}↾}_{{a}}\right):\mathrm{dom}\left({\mathrm{I}↾}_{{a}}\right)\underset{1-1 onto}{⟶}{f}\wedge {f}\subseteq \left\{{p}\in \left(𝒫{V}\setminus \left\{\varnothing \right\}\right)|\left|{p}\right|\le 2\right\}\right)$
26 resiexg ${⊢}{a}\in \mathrm{V}\to {\mathrm{I}↾}_{{a}}\in \mathrm{V}$
27 10 26 ax-mp ${⊢}{\mathrm{I}↾}_{{a}}\in \mathrm{V}$
28 27 f11o ${⊢}\left({\mathrm{I}↾}_{{a}}\right):\mathrm{dom}\left({\mathrm{I}↾}_{{a}}\right)\underset{1-1}{⟶}\left\{{p}\in \left(𝒫{V}\setminus \left\{\varnothing \right\}\right)|\left|{p}\right|\le 2\right\}↔\exists {f}\phantom{\rule{.4em}{0ex}}\left(\left({\mathrm{I}↾}_{{a}}\right):\mathrm{dom}\left({\mathrm{I}↾}_{{a}}\right)\underset{1-1 onto}{⟶}{f}\wedge {f}\subseteq \left\{{p}\in \left(𝒫{V}\setminus \left\{\varnothing \right\}\right)|\left|{p}\right|\le 2\right\}\right)$
29 25 28 sylibr ${⊢}\left({a}\subseteq \mathrm{Pairs}\left({V}\right)\wedge {V}\in {W}\right)\to \left({\mathrm{I}↾}_{{a}}\right):\mathrm{dom}\left({\mathrm{I}↾}_{{a}}\right)\underset{1-1}{⟶}\left\{{p}\in \left(𝒫{V}\setminus \left\{\varnothing \right\}\right)|\left|{p}\right|\le 2\right\}$
30 10 a1i ${⊢}{a}\subseteq \mathrm{Pairs}\left({V}\right)\to {a}\in \mathrm{V}$
31 30 resiexd ${⊢}{a}\subseteq \mathrm{Pairs}\left({V}\right)\to {\mathrm{I}↾}_{{a}}\in \mathrm{V}$
32 31 anim2i ${⊢}\left({V}\in {W}\wedge {a}\subseteq \mathrm{Pairs}\left({V}\right)\right)\to \left({V}\in {W}\wedge {\mathrm{I}↾}_{{a}}\in \mathrm{V}\right)$
33 32 ancoms ${⊢}\left({a}\subseteq \mathrm{Pairs}\left({V}\right)\wedge {V}\in {W}\right)\to \left({V}\in {W}\wedge {\mathrm{I}↾}_{{a}}\in \mathrm{V}\right)$
34 isuspgrop ${⊢}\left({V}\in {W}\wedge {\mathrm{I}↾}_{{a}}\in \mathrm{V}\right)\to \left(⟨{V},{\mathrm{I}↾}_{{a}}⟩\in \mathrm{USHGraph}↔\left({\mathrm{I}↾}_{{a}}\right):\mathrm{dom}\left({\mathrm{I}↾}_{{a}}\right)\underset{1-1}{⟶}\left\{{p}\in \left(𝒫{V}\setminus \left\{\varnothing \right\}\right)|\left|{p}\right|\le 2\right\}\right)$
35 33 34 syl ${⊢}\left({a}\subseteq \mathrm{Pairs}\left({V}\right)\wedge {V}\in {W}\right)\to \left(⟨{V},{\mathrm{I}↾}_{{a}}⟩\in \mathrm{USHGraph}↔\left({\mathrm{I}↾}_{{a}}\right):\mathrm{dom}\left({\mathrm{I}↾}_{{a}}\right)\underset{1-1}{⟶}\left\{{p}\in \left(𝒫{V}\setminus \left\{\varnothing \right\}\right)|\left|{p}\right|\le 2\right\}\right)$
36 29 35 mpbird ${⊢}\left({a}\subseteq \mathrm{Pairs}\left({V}\right)\wedge {V}\in {W}\right)\to ⟨{V},{\mathrm{I}↾}_{{a}}⟩\in \mathrm{USHGraph}$
37 fveqeq2 ${⊢}{q}=⟨{V},{\mathrm{I}↾}_{{a}}⟩\to \left(\mathrm{Vtx}\left({q}\right)={V}↔\mathrm{Vtx}\left(⟨{V},{\mathrm{I}↾}_{{a}}⟩\right)={V}\right)$
38 fveqeq2 ${⊢}{q}=⟨{V},{\mathrm{I}↾}_{{a}}⟩\to \left(\mathrm{Edg}\left({q}\right)={a}↔\mathrm{Edg}\left(⟨{V},{\mathrm{I}↾}_{{a}}⟩\right)={a}\right)$
39 37 38 anbi12d ${⊢}{q}=⟨{V},{\mathrm{I}↾}_{{a}}⟩\to \left(\left(\mathrm{Vtx}\left({q}\right)={V}\wedge \mathrm{Edg}\left({q}\right)={a}\right)↔\left(\mathrm{Vtx}\left(⟨{V},{\mathrm{I}↾}_{{a}}⟩\right)={V}\wedge \mathrm{Edg}\left(⟨{V},{\mathrm{I}↾}_{{a}}⟩\right)={a}\right)\right)$
40 39 adantl ${⊢}\left(\left({a}\subseteq \mathrm{Pairs}\left({V}\right)\wedge {V}\in {W}\right)\wedge {q}=⟨{V},{\mathrm{I}↾}_{{a}}⟩\right)\to \left(\left(\mathrm{Vtx}\left({q}\right)={V}\wedge \mathrm{Edg}\left({q}\right)={a}\right)↔\left(\mathrm{Vtx}\left(⟨{V},{\mathrm{I}↾}_{{a}}⟩\right)={V}\wedge \mathrm{Edg}\left(⟨{V},{\mathrm{I}↾}_{{a}}⟩\right)={a}\right)\right)$
41 opvtxfv ${⊢}\left({V}\in {W}\wedge {\mathrm{I}↾}_{{a}}\in \mathrm{V}\right)\to \mathrm{Vtx}\left(⟨{V},{\mathrm{I}↾}_{{a}}⟩\right)={V}$
42 32 41 syl ${⊢}\left({V}\in {W}\wedge {a}\subseteq \mathrm{Pairs}\left({V}\right)\right)\to \mathrm{Vtx}\left(⟨{V},{\mathrm{I}↾}_{{a}}⟩\right)={V}$
43 edgopval ${⊢}\left({V}\in {W}\wedge {\mathrm{I}↾}_{{a}}\in \mathrm{V}\right)\to \mathrm{Edg}\left(⟨{V},{\mathrm{I}↾}_{{a}}⟩\right)=\mathrm{ran}\left({\mathrm{I}↾}_{{a}}\right)$
44 32 43 syl ${⊢}\left({V}\in {W}\wedge {a}\subseteq \mathrm{Pairs}\left({V}\right)\right)\to \mathrm{Edg}\left(⟨{V},{\mathrm{I}↾}_{{a}}⟩\right)=\mathrm{ran}\left({\mathrm{I}↾}_{{a}}\right)$
45 rnresi ${⊢}\mathrm{ran}\left({\mathrm{I}↾}_{{a}}\right)={a}$
46 44 45 syl6eq ${⊢}\left({V}\in {W}\wedge {a}\subseteq \mathrm{Pairs}\left({V}\right)\right)\to \mathrm{Edg}\left(⟨{V},{\mathrm{I}↾}_{{a}}⟩\right)={a}$
47 42 46 jca ${⊢}\left({V}\in {W}\wedge {a}\subseteq \mathrm{Pairs}\left({V}\right)\right)\to \left(\mathrm{Vtx}\left(⟨{V},{\mathrm{I}↾}_{{a}}⟩\right)={V}\wedge \mathrm{Edg}\left(⟨{V},{\mathrm{I}↾}_{{a}}⟩\right)={a}\right)$
48 47 ancoms ${⊢}\left({a}\subseteq \mathrm{Pairs}\left({V}\right)\wedge {V}\in {W}\right)\to \left(\mathrm{Vtx}\left(⟨{V},{\mathrm{I}↾}_{{a}}⟩\right)={V}\wedge \mathrm{Edg}\left(⟨{V},{\mathrm{I}↾}_{{a}}⟩\right)={a}\right)$
49 36 40 48 rspcedvd ${⊢}\left({a}\subseteq \mathrm{Pairs}\left({V}\right)\wedge {V}\in {W}\right)\to \exists {q}\in \mathrm{USHGraph}\phantom{\rule{.4em}{0ex}}\left(\mathrm{Vtx}\left({q}\right)={V}\wedge \mathrm{Edg}\left({q}\right)={a}\right)$
50 9 49 jca ${⊢}\left({a}\subseteq \mathrm{Pairs}\left({V}\right)\wedge {V}\in {W}\right)\to \left({V}={V}\wedge \exists {q}\in \mathrm{USHGraph}\phantom{\rule{.4em}{0ex}}\left(\mathrm{Vtx}\left({q}\right)={V}\wedge \mathrm{Edg}\left({q}\right)={a}\right)\right)$
51 2 eleq2i ${⊢}⟨{V},{a}⟩\in {G}↔⟨{V},{a}⟩\in \left\{⟨{v},{e}⟩|\left({v}={V}\wedge \exists {q}\in \mathrm{USHGraph}\phantom{\rule{.4em}{0ex}}\left(\mathrm{Vtx}\left({q}\right)={v}\wedge \mathrm{Edg}\left({q}\right)={e}\right)\right)\right\}$
52 30 anim1i ${⊢}\left({a}\subseteq \mathrm{Pairs}\left({V}\right)\wedge {V}\in {W}\right)\to \left({a}\in \mathrm{V}\wedge {V}\in {W}\right)$
53 52 ancomd ${⊢}\left({a}\subseteq \mathrm{Pairs}\left({V}\right)\wedge {V}\in {W}\right)\to \left({V}\in {W}\wedge {a}\in \mathrm{V}\right)$
54 eqeq1 ${⊢}{v}={V}\to \left({v}={V}↔{V}={V}\right)$
55 54 adantr ${⊢}\left({v}={V}\wedge {e}={a}\right)\to \left({v}={V}↔{V}={V}\right)$
56 eqeq2 ${⊢}{v}={V}\to \left(\mathrm{Vtx}\left({q}\right)={v}↔\mathrm{Vtx}\left({q}\right)={V}\right)$
57 eqeq2 ${⊢}{e}={a}\to \left(\mathrm{Edg}\left({q}\right)={e}↔\mathrm{Edg}\left({q}\right)={a}\right)$
58 56 57 bi2anan9 ${⊢}\left({v}={V}\wedge {e}={a}\right)\to \left(\left(\mathrm{Vtx}\left({q}\right)={v}\wedge \mathrm{Edg}\left({q}\right)={e}\right)↔\left(\mathrm{Vtx}\left({q}\right)={V}\wedge \mathrm{Edg}\left({q}\right)={a}\right)\right)$
59 58 rexbidv ${⊢}\left({v}={V}\wedge {e}={a}\right)\to \left(\exists {q}\in \mathrm{USHGraph}\phantom{\rule{.4em}{0ex}}\left(\mathrm{Vtx}\left({q}\right)={v}\wedge \mathrm{Edg}\left({q}\right)={e}\right)↔\exists {q}\in \mathrm{USHGraph}\phantom{\rule{.4em}{0ex}}\left(\mathrm{Vtx}\left({q}\right)={V}\wedge \mathrm{Edg}\left({q}\right)={a}\right)\right)$
60 55 59 anbi12d ${⊢}\left({v}={V}\wedge {e}={a}\right)\to \left(\left({v}={V}\wedge \exists {q}\in \mathrm{USHGraph}\phantom{\rule{.4em}{0ex}}\left(\mathrm{Vtx}\left({q}\right)={v}\wedge \mathrm{Edg}\left({q}\right)={e}\right)\right)↔\left({V}={V}\wedge \exists {q}\in \mathrm{USHGraph}\phantom{\rule{.4em}{0ex}}\left(\mathrm{Vtx}\left({q}\right)={V}\wedge \mathrm{Edg}\left({q}\right)={a}\right)\right)\right)$
61 60 opelopabga ${⊢}\left({V}\in {W}\wedge {a}\in \mathrm{V}\right)\to \left(⟨{V},{a}⟩\in \left\{⟨{v},{e}⟩|\left({v}={V}\wedge \exists {q}\in \mathrm{USHGraph}\phantom{\rule{.4em}{0ex}}\left(\mathrm{Vtx}\left({q}\right)={v}\wedge \mathrm{Edg}\left({q}\right)={e}\right)\right)\right\}↔\left({V}={V}\wedge \exists {q}\in \mathrm{USHGraph}\phantom{\rule{.4em}{0ex}}\left(\mathrm{Vtx}\left({q}\right)={V}\wedge \mathrm{Edg}\left({q}\right)={a}\right)\right)\right)$
62 53 61 syl ${⊢}\left({a}\subseteq \mathrm{Pairs}\left({V}\right)\wedge {V}\in {W}\right)\to \left(⟨{V},{a}⟩\in \left\{⟨{v},{e}⟩|\left({v}={V}\wedge \exists {q}\in \mathrm{USHGraph}\phantom{\rule{.4em}{0ex}}\left(\mathrm{Vtx}\left({q}\right)={v}\wedge \mathrm{Edg}\left({q}\right)={e}\right)\right)\right\}↔\left({V}={V}\wedge \exists {q}\in \mathrm{USHGraph}\phantom{\rule{.4em}{0ex}}\left(\mathrm{Vtx}\left({q}\right)={V}\wedge \mathrm{Edg}\left({q}\right)={a}\right)\right)\right)$
63 51 62 syl5bb ${⊢}\left({a}\subseteq \mathrm{Pairs}\left({V}\right)\wedge {V}\in {W}\right)\to \left(⟨{V},{a}⟩\in {G}↔\left({V}={V}\wedge \exists {q}\in \mathrm{USHGraph}\phantom{\rule{.4em}{0ex}}\left(\mathrm{Vtx}\left({q}\right)={V}\wedge \mathrm{Edg}\left({q}\right)={a}\right)\right)\right)$
64 50 63 mpbird ${⊢}\left({a}\subseteq \mathrm{Pairs}\left({V}\right)\wedge {V}\in {W}\right)\to ⟨{V},{a}⟩\in {G}$
65 fveq2 ${⊢}{b}=⟨{V},{a}⟩\to {2}^{nd}\left({b}\right)={2}^{nd}\left(⟨{V},{a}⟩\right)$
66 65 eqeq2d ${⊢}{b}=⟨{V},{a}⟩\to \left({a}={2}^{nd}\left({b}\right)↔{a}={2}^{nd}\left(⟨{V},{a}⟩\right)\right)$
67 66 adantl ${⊢}\left(\left({a}\subseteq \mathrm{Pairs}\left({V}\right)\wedge {V}\in {W}\right)\wedge {b}=⟨{V},{a}⟩\right)\to \left({a}={2}^{nd}\left({b}\right)↔{a}={2}^{nd}\left(⟨{V},{a}⟩\right)\right)$
68 op2ndg ${⊢}\left({V}\in {W}\wedge {a}\in \mathrm{V}\right)\to {2}^{nd}\left(⟨{V},{a}⟩\right)={a}$
69 68 elvd ${⊢}{V}\in {W}\to {2}^{nd}\left(⟨{V},{a}⟩\right)={a}$
70 69 adantl ${⊢}\left({a}\subseteq \mathrm{Pairs}\left({V}\right)\wedge {V}\in {W}\right)\to {2}^{nd}\left(⟨{V},{a}⟩\right)={a}$
71 70 eqcomd ${⊢}\left({a}\subseteq \mathrm{Pairs}\left({V}\right)\wedge {V}\in {W}\right)\to {a}={2}^{nd}\left(⟨{V},{a}⟩\right)$
72 64 67 71 rspcedvd ${⊢}\left({a}\subseteq \mathrm{Pairs}\left({V}\right)\wedge {V}\in {W}\right)\to \exists {b}\in {G}\phantom{\rule{.4em}{0ex}}{a}={2}^{nd}\left({b}\right)$
73 72 ex ${⊢}{a}\subseteq \mathrm{Pairs}\left({V}\right)\to \left({V}\in {W}\to \exists {b}\in {G}\phantom{\rule{.4em}{0ex}}{a}={2}^{nd}\left({b}\right)\right)$
74 8 73 sylbi ${⊢}{a}\in {P}\to \left({V}\in {W}\to \exists {b}\in {G}\phantom{\rule{.4em}{0ex}}{a}={2}^{nd}\left({b}\right)\right)$
75 74 impcom ${⊢}\left({V}\in {W}\wedge {a}\in {P}\right)\to \exists {b}\in {G}\phantom{\rule{.4em}{0ex}}{a}={2}^{nd}\left({b}\right)$
76 1 2 3 uspgrsprfv ${⊢}{b}\in {G}\to {F}\left({b}\right)={2}^{nd}\left({b}\right)$
77 76 adantl ${⊢}\left(\left({V}\in {W}\wedge {a}\in {P}\right)\wedge {b}\in {G}\right)\to {F}\left({b}\right)={2}^{nd}\left({b}\right)$
78 77 eqeq2d ${⊢}\left(\left({V}\in {W}\wedge {a}\in {P}\right)\wedge {b}\in {G}\right)\to \left({a}={F}\left({b}\right)↔{a}={2}^{nd}\left({b}\right)\right)$
79 78 rexbidva ${⊢}\left({V}\in {W}\wedge {a}\in {P}\right)\to \left(\exists {b}\in {G}\phantom{\rule{.4em}{0ex}}{a}={F}\left({b}\right)↔\exists {b}\in {G}\phantom{\rule{.4em}{0ex}}{a}={2}^{nd}\left({b}\right)\right)$
80 75 79 mpbird ${⊢}\left({V}\in {W}\wedge {a}\in {P}\right)\to \exists {b}\in {G}\phantom{\rule{.4em}{0ex}}{a}={F}\left({b}\right)$
81 80 ralrimiva ${⊢}{V}\in {W}\to \forall {a}\in {P}\phantom{\rule{.4em}{0ex}}\exists {b}\in {G}\phantom{\rule{.4em}{0ex}}{a}={F}\left({b}\right)$
82 dffo3 ${⊢}{F}:{G}\underset{onto}{⟶}{P}↔\left({F}:{G}⟶{P}\wedge \forall {a}\in {P}\phantom{\rule{.4em}{0ex}}\exists {b}\in {G}\phantom{\rule{.4em}{0ex}}{a}={F}\left({b}\right)\right)$
83 5 81 82 sylanbrc ${⊢}{V}\in {W}\to {F}:{G}\underset{onto}{⟶}{P}$