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→ 𝑃