Metamath Proof Explorer


Theorem uspgrsprf1

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

Ref Expression
Hypotheses uspgrsprf.p 𝑃 = 𝒫 ( Pairs ‘ 𝑉 )
uspgrsprf.g 𝐺 = { ⟨ 𝑣 , 𝑒 ⟩ ∣ ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) }
uspgrsprf.f 𝐹 = ( 𝑔𝐺 ↦ ( 2nd𝑔 ) )
Assertion uspgrsprf1 𝐹 : 𝐺1-1𝑃

Proof

Step Hyp Ref Expression
1 uspgrsprf.p 𝑃 = 𝒫 ( Pairs ‘ 𝑉 )
2 uspgrsprf.g 𝐺 = { ⟨ 𝑣 , 𝑒 ⟩ ∣ ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) }
3 uspgrsprf.f 𝐹 = ( 𝑔𝐺 ↦ ( 2nd𝑔 ) )
4 1 2 3 uspgrsprf 𝐹 : 𝐺𝑃
5 1 2 3 uspgrsprfv ( 𝑎𝐺 → ( 𝐹𝑎 ) = ( 2nd𝑎 ) )
6 1 2 3 uspgrsprfv ( 𝑏𝐺 → ( 𝐹𝑏 ) = ( 2nd𝑏 ) )
7 5 6 eqeqan12d ( ( 𝑎𝐺𝑏𝐺 ) → ( ( 𝐹𝑎 ) = ( 𝐹𝑏 ) ↔ ( 2nd𝑎 ) = ( 2nd𝑏 ) ) )
8 2 eleq2i ( 𝑎𝐺𝑎 ∈ { ⟨ 𝑣 , 𝑒 ⟩ ∣ ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) } )
9 elopab ( 𝑎 ∈ { ⟨ 𝑣 , 𝑒 ⟩ ∣ ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) } ↔ ∃ 𝑣𝑒 ( 𝑎 = ⟨ 𝑣 , 𝑒 ⟩ ∧ ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) ) )
10 opeq12 ( ( 𝑣 = 𝑤𝑒 = 𝑓 ) → ⟨ 𝑣 , 𝑒 ⟩ = ⟨ 𝑤 , 𝑓 ⟩ )
11 10 eqeq2d ( ( 𝑣 = 𝑤𝑒 = 𝑓 ) → ( 𝑎 = ⟨ 𝑣 , 𝑒 ⟩ ↔ 𝑎 = ⟨ 𝑤 , 𝑓 ⟩ ) )
12 eqeq1 ( 𝑣 = 𝑤 → ( 𝑣 = 𝑉𝑤 = 𝑉 ) )
13 12 adantr ( ( 𝑣 = 𝑤𝑒 = 𝑓 ) → ( 𝑣 = 𝑉𝑤 = 𝑉 ) )
14 eqeq2 ( 𝑣 = 𝑤 → ( ( Vtx ‘ 𝑞 ) = 𝑣 ↔ ( Vtx ‘ 𝑞 ) = 𝑤 ) )
15 eqeq2 ( 𝑒 = 𝑓 → ( ( Edg ‘ 𝑞 ) = 𝑒 ↔ ( Edg ‘ 𝑞 ) = 𝑓 ) )
16 14 15 bi2anan9 ( ( 𝑣 = 𝑤𝑒 = 𝑓 ) → ( ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ↔ ( ( Vtx ‘ 𝑞 ) = 𝑤 ∧ ( Edg ‘ 𝑞 ) = 𝑓 ) ) )
17 16 rexbidv ( ( 𝑣 = 𝑤𝑒 = 𝑓 ) → ( ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ↔ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑤 ∧ ( Edg ‘ 𝑞 ) = 𝑓 ) ) )
18 13 17 anbi12d ( ( 𝑣 = 𝑤𝑒 = 𝑓 ) → ( ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) ↔ ( 𝑤 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑤 ∧ ( Edg ‘ 𝑞 ) = 𝑓 ) ) ) )
19 11 18 anbi12d ( ( 𝑣 = 𝑤𝑒 = 𝑓 ) → ( ( 𝑎 = ⟨ 𝑣 , 𝑒 ⟩ ∧ ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) ) ↔ ( 𝑎 = ⟨ 𝑤 , 𝑓 ⟩ ∧ ( 𝑤 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑤 ∧ ( Edg ‘ 𝑞 ) = 𝑓 ) ) ) ) )
20 19 cbvex2vw ( ∃ 𝑣𝑒 ( 𝑎 = ⟨ 𝑣 , 𝑒 ⟩ ∧ ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) ) ↔ ∃ 𝑤𝑓 ( 𝑎 = ⟨ 𝑤 , 𝑓 ⟩ ∧ ( 𝑤 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑤 ∧ ( Edg ‘ 𝑞 ) = 𝑓 ) ) ) )
21 8 9 20 3bitri ( 𝑎𝐺 ↔ ∃ 𝑤𝑓 ( 𝑎 = ⟨ 𝑤 , 𝑓 ⟩ ∧ ( 𝑤 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑤 ∧ ( Edg ‘ 𝑞 ) = 𝑓 ) ) ) )
22 2 eleq2i ( 𝑏𝐺𝑏 ∈ { ⟨ 𝑣 , 𝑒 ⟩ ∣ ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) } )
23 elopab ( 𝑏 ∈ { ⟨ 𝑣 , 𝑒 ⟩ ∣ ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) } ↔ ∃ 𝑣𝑒 ( 𝑏 = ⟨ 𝑣 , 𝑒 ⟩ ∧ ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) ) )
24 22 23 bitri ( 𝑏𝐺 ↔ ∃ 𝑣𝑒 ( 𝑏 = ⟨ 𝑣 , 𝑒 ⟩ ∧ ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) ) )
25 eqeq2 ( 𝑤 = 𝑉 → ( 𝑣 = 𝑤𝑣 = 𝑉 ) )
26 opeq12 ( ( 𝑤 = 𝑣𝑓 = 𝑒 ) → ⟨ 𝑤 , 𝑓 ⟩ = ⟨ 𝑣 , 𝑒 ⟩ )
27 26 ex ( 𝑤 = 𝑣 → ( 𝑓 = 𝑒 → ⟨ 𝑤 , 𝑓 ⟩ = ⟨ 𝑣 , 𝑒 ⟩ ) )
28 27 equcoms ( 𝑣 = 𝑤 → ( 𝑓 = 𝑒 → ⟨ 𝑤 , 𝑓 ⟩ = ⟨ 𝑣 , 𝑒 ⟩ ) )
29 25 28 syl6bir ( 𝑤 = 𝑉 → ( 𝑣 = 𝑉 → ( 𝑓 = 𝑒 → ⟨ 𝑤 , 𝑓 ⟩ = ⟨ 𝑣 , 𝑒 ⟩ ) ) )
30 29 ad2antrl ( ( 𝑎 = ⟨ 𝑤 , 𝑓 ⟩ ∧ ( 𝑤 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑤 ∧ ( Edg ‘ 𝑞 ) = 𝑓 ) ) ) → ( 𝑣 = 𝑉 → ( 𝑓 = 𝑒 → ⟨ 𝑤 , 𝑓 ⟩ = ⟨ 𝑣 , 𝑒 ⟩ ) ) )
31 30 com12 ( 𝑣 = 𝑉 → ( ( 𝑎 = ⟨ 𝑤 , 𝑓 ⟩ ∧ ( 𝑤 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑤 ∧ ( Edg ‘ 𝑞 ) = 𝑓 ) ) ) → ( 𝑓 = 𝑒 → ⟨ 𝑤 , 𝑓 ⟩ = ⟨ 𝑣 , 𝑒 ⟩ ) ) )
32 31 ad2antrl ( ( 𝑏 = ⟨ 𝑣 , 𝑒 ⟩ ∧ ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) ) → ( ( 𝑎 = ⟨ 𝑤 , 𝑓 ⟩ ∧ ( 𝑤 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑤 ∧ ( Edg ‘ 𝑞 ) = 𝑓 ) ) ) → ( 𝑓 = 𝑒 → ⟨ 𝑤 , 𝑓 ⟩ = ⟨ 𝑣 , 𝑒 ⟩ ) ) )
33 32 imp ( ( ( 𝑏 = ⟨ 𝑣 , 𝑒 ⟩ ∧ ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) ) ∧ ( 𝑎 = ⟨ 𝑤 , 𝑓 ⟩ ∧ ( 𝑤 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑤 ∧ ( Edg ‘ 𝑞 ) = 𝑓 ) ) ) ) → ( 𝑓 = 𝑒 → ⟨ 𝑤 , 𝑓 ⟩ = ⟨ 𝑣 , 𝑒 ⟩ ) )
34 vex 𝑤 ∈ V
35 vex 𝑓 ∈ V
36 34 35 op2ndd ( 𝑎 = ⟨ 𝑤 , 𝑓 ⟩ → ( 2nd𝑎 ) = 𝑓 )
37 36 ad2antrl ( ( ( 𝑏 = ⟨ 𝑣 , 𝑒 ⟩ ∧ ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) ) ∧ ( 𝑎 = ⟨ 𝑤 , 𝑓 ⟩ ∧ ( 𝑤 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑤 ∧ ( Edg ‘ 𝑞 ) = 𝑓 ) ) ) ) → ( 2nd𝑎 ) = 𝑓 )
38 vex 𝑣 ∈ V
39 vex 𝑒 ∈ V
40 38 39 op2ndd ( 𝑏 = ⟨ 𝑣 , 𝑒 ⟩ → ( 2nd𝑏 ) = 𝑒 )
41 40 adantr ( ( 𝑏 = ⟨ 𝑣 , 𝑒 ⟩ ∧ ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) ) → ( 2nd𝑏 ) = 𝑒 )
42 41 adantr ( ( ( 𝑏 = ⟨ 𝑣 , 𝑒 ⟩ ∧ ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) ) ∧ ( 𝑎 = ⟨ 𝑤 , 𝑓 ⟩ ∧ ( 𝑤 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑤 ∧ ( Edg ‘ 𝑞 ) = 𝑓 ) ) ) ) → ( 2nd𝑏 ) = 𝑒 )
43 37 42 eqeq12d ( ( ( 𝑏 = ⟨ 𝑣 , 𝑒 ⟩ ∧ ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) ) ∧ ( 𝑎 = ⟨ 𝑤 , 𝑓 ⟩ ∧ ( 𝑤 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑤 ∧ ( Edg ‘ 𝑞 ) = 𝑓 ) ) ) ) → ( ( 2nd𝑎 ) = ( 2nd𝑏 ) ↔ 𝑓 = 𝑒 ) )
44 eqeq12 ( ( 𝑎 = ⟨ 𝑤 , 𝑓 ⟩ ∧ 𝑏 = ⟨ 𝑣 , 𝑒 ⟩ ) → ( 𝑎 = 𝑏 ↔ ⟨ 𝑤 , 𝑓 ⟩ = ⟨ 𝑣 , 𝑒 ⟩ ) )
45 44 ex ( 𝑎 = ⟨ 𝑤 , 𝑓 ⟩ → ( 𝑏 = ⟨ 𝑣 , 𝑒 ⟩ → ( 𝑎 = 𝑏 ↔ ⟨ 𝑤 , 𝑓 ⟩ = ⟨ 𝑣 , 𝑒 ⟩ ) ) )
46 45 adantr ( ( 𝑎 = ⟨ 𝑤 , 𝑓 ⟩ ∧ ( 𝑤 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑤 ∧ ( Edg ‘ 𝑞 ) = 𝑓 ) ) ) → ( 𝑏 = ⟨ 𝑣 , 𝑒 ⟩ → ( 𝑎 = 𝑏 ↔ ⟨ 𝑤 , 𝑓 ⟩ = ⟨ 𝑣 , 𝑒 ⟩ ) ) )
47 46 com12 ( 𝑏 = ⟨ 𝑣 , 𝑒 ⟩ → ( ( 𝑎 = ⟨ 𝑤 , 𝑓 ⟩ ∧ ( 𝑤 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑤 ∧ ( Edg ‘ 𝑞 ) = 𝑓 ) ) ) → ( 𝑎 = 𝑏 ↔ ⟨ 𝑤 , 𝑓 ⟩ = ⟨ 𝑣 , 𝑒 ⟩ ) ) )
48 47 adantr ( ( 𝑏 = ⟨ 𝑣 , 𝑒 ⟩ ∧ ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) ) → ( ( 𝑎 = ⟨ 𝑤 , 𝑓 ⟩ ∧ ( 𝑤 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑤 ∧ ( Edg ‘ 𝑞 ) = 𝑓 ) ) ) → ( 𝑎 = 𝑏 ↔ ⟨ 𝑤 , 𝑓 ⟩ = ⟨ 𝑣 , 𝑒 ⟩ ) ) )
49 48 imp ( ( ( 𝑏 = ⟨ 𝑣 , 𝑒 ⟩ ∧ ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) ) ∧ ( 𝑎 = ⟨ 𝑤 , 𝑓 ⟩ ∧ ( 𝑤 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑤 ∧ ( Edg ‘ 𝑞 ) = 𝑓 ) ) ) ) → ( 𝑎 = 𝑏 ↔ ⟨ 𝑤 , 𝑓 ⟩ = ⟨ 𝑣 , 𝑒 ⟩ ) )
50 33 43 49 3imtr4d ( ( ( 𝑏 = ⟨ 𝑣 , 𝑒 ⟩ ∧ ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) ) ∧ ( 𝑎 = ⟨ 𝑤 , 𝑓 ⟩ ∧ ( 𝑤 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑤 ∧ ( Edg ‘ 𝑞 ) = 𝑓 ) ) ) ) → ( ( 2nd𝑎 ) = ( 2nd𝑏 ) → 𝑎 = 𝑏 ) )
51 50 ex ( ( 𝑏 = ⟨ 𝑣 , 𝑒 ⟩ ∧ ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) ) → ( ( 𝑎 = ⟨ 𝑤 , 𝑓 ⟩ ∧ ( 𝑤 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑤 ∧ ( Edg ‘ 𝑞 ) = 𝑓 ) ) ) → ( ( 2nd𝑎 ) = ( 2nd𝑏 ) → 𝑎 = 𝑏 ) ) )
52 51 exlimivv ( ∃ 𝑣𝑒 ( 𝑏 = ⟨ 𝑣 , 𝑒 ⟩ ∧ ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) ) → ( ( 𝑎 = ⟨ 𝑤 , 𝑓 ⟩ ∧ ( 𝑤 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑤 ∧ ( Edg ‘ 𝑞 ) = 𝑓 ) ) ) → ( ( 2nd𝑎 ) = ( 2nd𝑏 ) → 𝑎 = 𝑏 ) ) )
53 52 com12 ( ( 𝑎 = ⟨ 𝑤 , 𝑓 ⟩ ∧ ( 𝑤 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑤 ∧ ( Edg ‘ 𝑞 ) = 𝑓 ) ) ) → ( ∃ 𝑣𝑒 ( 𝑏 = ⟨ 𝑣 , 𝑒 ⟩ ∧ ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) ) → ( ( 2nd𝑎 ) = ( 2nd𝑏 ) → 𝑎 = 𝑏 ) ) )
54 53 exlimivv ( ∃ 𝑤𝑓 ( 𝑎 = ⟨ 𝑤 , 𝑓 ⟩ ∧ ( 𝑤 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑤 ∧ ( Edg ‘ 𝑞 ) = 𝑓 ) ) ) → ( ∃ 𝑣𝑒 ( 𝑏 = ⟨ 𝑣 , 𝑒 ⟩ ∧ ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) ) → ( ( 2nd𝑎 ) = ( 2nd𝑏 ) → 𝑎 = 𝑏 ) ) )
55 54 imp ( ( ∃ 𝑤𝑓 ( 𝑎 = ⟨ 𝑤 , 𝑓 ⟩ ∧ ( 𝑤 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑤 ∧ ( Edg ‘ 𝑞 ) = 𝑓 ) ) ) ∧ ∃ 𝑣𝑒 ( 𝑏 = ⟨ 𝑣 , 𝑒 ⟩ ∧ ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) ) ) → ( ( 2nd𝑎 ) = ( 2nd𝑏 ) → 𝑎 = 𝑏 ) )
56 21 24 55 syl2anb ( ( 𝑎𝐺𝑏𝐺 ) → ( ( 2nd𝑎 ) = ( 2nd𝑏 ) → 𝑎 = 𝑏 ) )
57 7 56 sylbid ( ( 𝑎𝐺𝑏𝐺 ) → ( ( 𝐹𝑎 ) = ( 𝐹𝑏 ) → 𝑎 = 𝑏 ) )
58 57 rgen2 𝑎𝐺𝑏𝐺 ( ( 𝐹𝑎 ) = ( 𝐹𝑏 ) → 𝑎 = 𝑏 )
59 dff13 ( 𝐹 : 𝐺1-1𝑃 ↔ ( 𝐹 : 𝐺𝑃 ∧ ∀ 𝑎𝐺𝑏𝐺 ( ( 𝐹𝑎 ) = ( 𝐹𝑏 ) → 𝑎 = 𝑏 ) ) )
60 4 58 59 mpbir2an 𝐹 : 𝐺1-1𝑃