| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | uspgrsprf.p | . . 3
⊢ 𝑃 = 𝒫 (Pairs‘𝑉) | 
| 2 |  | uspgrsprf.g | . . 3
⊢ 𝐺 = {〈𝑣, 𝑒〉 ∣ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))} | 
| 3 |  | uspgrsprf.f | . . 3
⊢ 𝐹 = (𝑔 ∈ 𝐺 ↦ (2nd ‘𝑔)) | 
| 4 | 1, 2, 3 | uspgrsprf 48062 | . 2
⊢ 𝐹:𝐺⟶𝑃 | 
| 5 | 1, 2, 3 | uspgrsprfv 48061 | . . . . 5
⊢ (𝑎 ∈ 𝐺 → (𝐹‘𝑎) = (2nd ‘𝑎)) | 
| 6 | 1, 2, 3 | uspgrsprfv 48061 | . . . . 5
⊢ (𝑏 ∈ 𝐺 → (𝐹‘𝑏) = (2nd ‘𝑏)) | 
| 7 | 5, 6 | eqeqan12d 2751 | . . . 4
⊢ ((𝑎 ∈ 𝐺 ∧ 𝑏 ∈ 𝐺) → ((𝐹‘𝑎) = (𝐹‘𝑏) ↔ (2nd ‘𝑎) = (2nd ‘𝑏))) | 
| 8 | 2 | eleq2i 2833 | . . . . . 6
⊢ (𝑎 ∈ 𝐺 ↔ 𝑎 ∈ {〈𝑣, 𝑒〉 ∣ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))}) | 
| 9 |  | elopab 5532 | . . . . . 6
⊢ (𝑎 ∈ {〈𝑣, 𝑒〉 ∣ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))} ↔ ∃𝑣∃𝑒(𝑎 = 〈𝑣, 𝑒〉 ∧ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒)))) | 
| 10 |  | opeq12 4875 | . . . . . . . . 9
⊢ ((𝑣 = 𝑤 ∧ 𝑒 = 𝑓) → 〈𝑣, 𝑒〉 = 〈𝑤, 𝑓〉) | 
| 11 | 10 | eqeq2d 2748 | . . . . . . . 8
⊢ ((𝑣 = 𝑤 ∧ 𝑒 = 𝑓) → (𝑎 = 〈𝑣, 𝑒〉 ↔ 𝑎 = 〈𝑤, 𝑓〉)) | 
| 12 |  | eqeq1 2741 | . . . . . . . . . 10
⊢ (𝑣 = 𝑤 → (𝑣 = 𝑉 ↔ 𝑤 = 𝑉)) | 
| 13 | 12 | adantr 480 | . . . . . . . . 9
⊢ ((𝑣 = 𝑤 ∧ 𝑒 = 𝑓) → (𝑣 = 𝑉 ↔ 𝑤 = 𝑉)) | 
| 14 |  | eqeq2 2749 | . . . . . . . . . . 11
⊢ (𝑣 = 𝑤 → ((Vtx‘𝑞) = 𝑣 ↔ (Vtx‘𝑞) = 𝑤)) | 
| 15 |  | eqeq2 2749 | . . . . . . . . . . 11
⊢ (𝑒 = 𝑓 → ((Edg‘𝑞) = 𝑒 ↔ (Edg‘𝑞) = 𝑓)) | 
| 16 | 14, 15 | bi2anan9 638 | . . . . . . . . . 10
⊢ ((𝑣 = 𝑤 ∧ 𝑒 = 𝑓) → (((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒) ↔ ((Vtx‘𝑞) = 𝑤 ∧ (Edg‘𝑞) = 𝑓))) | 
| 17 | 16 | rexbidv 3179 | . . . . . . . . 9
⊢ ((𝑣 = 𝑤 ∧ 𝑒 = 𝑓) → (∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒) ↔ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑤 ∧ (Edg‘𝑞) = 𝑓))) | 
| 18 | 13, 17 | anbi12d 632 | . . . . . . . 8
⊢ ((𝑣 = 𝑤 ∧ 𝑒 = 𝑓) → ((𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒)) ↔ (𝑤 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑤 ∧ (Edg‘𝑞) = 𝑓)))) | 
| 19 | 11, 18 | anbi12d 632 | . . . . . . 7
⊢ ((𝑣 = 𝑤 ∧ 𝑒 = 𝑓) → ((𝑎 = 〈𝑣, 𝑒〉 ∧ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))) ↔ (𝑎 = 〈𝑤, 𝑓〉 ∧ (𝑤 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑤 ∧ (Edg‘𝑞) = 𝑓))))) | 
| 20 | 19 | cbvex2vw 2040 | . . . . . 6
⊢
(∃𝑣∃𝑒(𝑎 = 〈𝑣, 𝑒〉 ∧ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))) ↔ ∃𝑤∃𝑓(𝑎 = 〈𝑤, 𝑓〉 ∧ (𝑤 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑤 ∧ (Edg‘𝑞) = 𝑓)))) | 
| 21 | 8, 9, 20 | 3bitri 297 | . . . . 5
⊢ (𝑎 ∈ 𝐺 ↔ ∃𝑤∃𝑓(𝑎 = 〈𝑤, 𝑓〉 ∧ (𝑤 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑤 ∧ (Edg‘𝑞) = 𝑓)))) | 
| 22 | 2 | eleq2i 2833 | . . . . . 6
⊢ (𝑏 ∈ 𝐺 ↔ 𝑏 ∈ {〈𝑣, 𝑒〉 ∣ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))}) | 
| 23 |  | elopab 5532 | . . . . . 6
⊢ (𝑏 ∈ {〈𝑣, 𝑒〉 ∣ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))} ↔ ∃𝑣∃𝑒(𝑏 = 〈𝑣, 𝑒〉 ∧ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒)))) | 
| 24 | 22, 23 | bitri 275 | . . . . 5
⊢ (𝑏 ∈ 𝐺 ↔ ∃𝑣∃𝑒(𝑏 = 〈𝑣, 𝑒〉 ∧ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒)))) | 
| 25 |  | eqeq2 2749 | . . . . . . . . . . . . . . . 16
⊢ (𝑤 = 𝑉 → (𝑣 = 𝑤 ↔ 𝑣 = 𝑉)) | 
| 26 |  | opeq12 4875 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑤 = 𝑣 ∧ 𝑓 = 𝑒) → 〈𝑤, 𝑓〉 = 〈𝑣, 𝑒〉) | 
| 27 | 26 | ex 412 | . . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 𝑣 → (𝑓 = 𝑒 → 〈𝑤, 𝑓〉 = 〈𝑣, 𝑒〉)) | 
| 28 | 27 | equcoms 2019 | . . . . . . . . . . . . . . . 16
⊢ (𝑣 = 𝑤 → (𝑓 = 𝑒 → 〈𝑤, 𝑓〉 = 〈𝑣, 𝑒〉)) | 
| 29 | 25, 28 | biimtrrdi 254 | . . . . . . . . . . . . . . 15
⊢ (𝑤 = 𝑉 → (𝑣 = 𝑉 → (𝑓 = 𝑒 → 〈𝑤, 𝑓〉 = 〈𝑣, 𝑒〉))) | 
| 30 | 29 | ad2antrl 728 | . . . . . . . . . . . . . 14
⊢ ((𝑎 = 〈𝑤, 𝑓〉 ∧ (𝑤 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑤 ∧ (Edg‘𝑞) = 𝑓))) → (𝑣 = 𝑉 → (𝑓 = 𝑒 → 〈𝑤, 𝑓〉 = 〈𝑣, 𝑒〉))) | 
| 31 | 30 | com12 32 | . . . . . . . . . . . . 13
⊢ (𝑣 = 𝑉 → ((𝑎 = 〈𝑤, 𝑓〉 ∧ (𝑤 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑤 ∧ (Edg‘𝑞) = 𝑓))) → (𝑓 = 𝑒 → 〈𝑤, 𝑓〉 = 〈𝑣, 𝑒〉))) | 
| 32 | 31 | ad2antrl 728 | . . . . . . . . . . . 12
⊢ ((𝑏 = 〈𝑣, 𝑒〉 ∧ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))) → ((𝑎 = 〈𝑤, 𝑓〉 ∧ (𝑤 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑤 ∧ (Edg‘𝑞) = 𝑓))) → (𝑓 = 𝑒 → 〈𝑤, 𝑓〉 = 〈𝑣, 𝑒〉))) | 
| 33 | 32 | imp 406 | . . . . . . . . . . 11
⊢ (((𝑏 = 〈𝑣, 𝑒〉 ∧ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))) ∧ (𝑎 = 〈𝑤, 𝑓〉 ∧ (𝑤 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑤 ∧ (Edg‘𝑞) = 𝑓)))) → (𝑓 = 𝑒 → 〈𝑤, 𝑓〉 = 〈𝑣, 𝑒〉)) | 
| 34 |  | vex 3484 | . . . . . . . . . . . . . 14
⊢ 𝑤 ∈ V | 
| 35 |  | vex 3484 | . . . . . . . . . . . . . 14
⊢ 𝑓 ∈ V | 
| 36 | 34, 35 | op2ndd 8025 | . . . . . . . . . . . . 13
⊢ (𝑎 = 〈𝑤, 𝑓〉 → (2nd ‘𝑎) = 𝑓) | 
| 37 | 36 | ad2antrl 728 | . . . . . . . . . . . 12
⊢ (((𝑏 = 〈𝑣, 𝑒〉 ∧ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))) ∧ (𝑎 = 〈𝑤, 𝑓〉 ∧ (𝑤 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑤 ∧ (Edg‘𝑞) = 𝑓)))) → (2nd ‘𝑎) = 𝑓) | 
| 38 |  | vex 3484 | . . . . . . . . . . . . . . 15
⊢ 𝑣 ∈ V | 
| 39 |  | vex 3484 | . . . . . . . . . . . . . . 15
⊢ 𝑒 ∈ V | 
| 40 | 38, 39 | op2ndd 8025 | . . . . . . . . . . . . . 14
⊢ (𝑏 = 〈𝑣, 𝑒〉 → (2nd ‘𝑏) = 𝑒) | 
| 41 | 40 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝑏 = 〈𝑣, 𝑒〉 ∧ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))) → (2nd ‘𝑏) = 𝑒) | 
| 42 | 41 | adantr 480 | . . . . . . . . . . . 12
⊢ (((𝑏 = 〈𝑣, 𝑒〉 ∧ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))) ∧ (𝑎 = 〈𝑤, 𝑓〉 ∧ (𝑤 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑤 ∧ (Edg‘𝑞) = 𝑓)))) → (2nd ‘𝑏) = 𝑒) | 
| 43 | 37, 42 | eqeq12d 2753 | . . . . . . . . . . 11
⊢ (((𝑏 = 〈𝑣, 𝑒〉 ∧ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))) ∧ (𝑎 = 〈𝑤, 𝑓〉 ∧ (𝑤 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑤 ∧ (Edg‘𝑞) = 𝑓)))) → ((2nd ‘𝑎) = (2nd ‘𝑏) ↔ 𝑓 = 𝑒)) | 
| 44 |  | eqeq12 2754 | . . . . . . . . . . . . . . . 16
⊢ ((𝑎 = 〈𝑤, 𝑓〉 ∧ 𝑏 = 〈𝑣, 𝑒〉) → (𝑎 = 𝑏 ↔ 〈𝑤, 𝑓〉 = 〈𝑣, 𝑒〉)) | 
| 45 | 44 | ex 412 | . . . . . . . . . . . . . . 15
⊢ (𝑎 = 〈𝑤, 𝑓〉 → (𝑏 = 〈𝑣, 𝑒〉 → (𝑎 = 𝑏 ↔ 〈𝑤, 𝑓〉 = 〈𝑣, 𝑒〉))) | 
| 46 | 45 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝑎 = 〈𝑤, 𝑓〉 ∧ (𝑤 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑤 ∧ (Edg‘𝑞) = 𝑓))) → (𝑏 = 〈𝑣, 𝑒〉 → (𝑎 = 𝑏 ↔ 〈𝑤, 𝑓〉 = 〈𝑣, 𝑒〉))) | 
| 47 | 46 | com12 32 | . . . . . . . . . . . . 13
⊢ (𝑏 = 〈𝑣, 𝑒〉 → ((𝑎 = 〈𝑤, 𝑓〉 ∧ (𝑤 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑤 ∧ (Edg‘𝑞) = 𝑓))) → (𝑎 = 𝑏 ↔ 〈𝑤, 𝑓〉 = 〈𝑣, 𝑒〉))) | 
| 48 | 47 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝑏 = 〈𝑣, 𝑒〉 ∧ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))) → ((𝑎 = 〈𝑤, 𝑓〉 ∧ (𝑤 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑤 ∧ (Edg‘𝑞) = 𝑓))) → (𝑎 = 𝑏 ↔ 〈𝑤, 𝑓〉 = 〈𝑣, 𝑒〉))) | 
| 49 | 48 | imp 406 | . . . . . . . . . . 11
⊢ (((𝑏 = 〈𝑣, 𝑒〉 ∧ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))) ∧ (𝑎 = 〈𝑤, 𝑓〉 ∧ (𝑤 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑤 ∧ (Edg‘𝑞) = 𝑓)))) → (𝑎 = 𝑏 ↔ 〈𝑤, 𝑓〉 = 〈𝑣, 𝑒〉)) | 
| 50 | 33, 43, 49 | 3imtr4d 294 | . . . . . . . . . 10
⊢ (((𝑏 = 〈𝑣, 𝑒〉 ∧ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))) ∧ (𝑎 = 〈𝑤, 𝑓〉 ∧ (𝑤 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑤 ∧ (Edg‘𝑞) = 𝑓)))) → ((2nd ‘𝑎) = (2nd ‘𝑏) → 𝑎 = 𝑏)) | 
| 51 | 50 | ex 412 | . . . . . . . . 9
⊢ ((𝑏 = 〈𝑣, 𝑒〉 ∧ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))) → ((𝑎 = 〈𝑤, 𝑓〉 ∧ (𝑤 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑤 ∧ (Edg‘𝑞) = 𝑓))) → ((2nd ‘𝑎) = (2nd ‘𝑏) → 𝑎 = 𝑏))) | 
| 52 | 51 | exlimivv 1932 | . . . . . . . 8
⊢
(∃𝑣∃𝑒(𝑏 = 〈𝑣, 𝑒〉 ∧ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))) → ((𝑎 = 〈𝑤, 𝑓〉 ∧ (𝑤 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑤 ∧ (Edg‘𝑞) = 𝑓))) → ((2nd ‘𝑎) = (2nd ‘𝑏) → 𝑎 = 𝑏))) | 
| 53 | 52 | com12 32 | . . . . . . 7
⊢ ((𝑎 = 〈𝑤, 𝑓〉 ∧ (𝑤 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑤 ∧ (Edg‘𝑞) = 𝑓))) → (∃𝑣∃𝑒(𝑏 = 〈𝑣, 𝑒〉 ∧ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))) → ((2nd ‘𝑎) = (2nd ‘𝑏) → 𝑎 = 𝑏))) | 
| 54 | 53 | exlimivv 1932 | . . . . . 6
⊢
(∃𝑤∃𝑓(𝑎 = 〈𝑤, 𝑓〉 ∧ (𝑤 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑤 ∧ (Edg‘𝑞) = 𝑓))) → (∃𝑣∃𝑒(𝑏 = 〈𝑣, 𝑒〉 ∧ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))) → ((2nd ‘𝑎) = (2nd ‘𝑏) → 𝑎 = 𝑏))) | 
| 55 | 54 | imp 406 | . . . . 5
⊢
((∃𝑤∃𝑓(𝑎 = 〈𝑤, 𝑓〉 ∧ (𝑤 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑤 ∧ (Edg‘𝑞) = 𝑓))) ∧ ∃𝑣∃𝑒(𝑏 = 〈𝑣, 𝑒〉 ∧ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒)))) → ((2nd ‘𝑎) = (2nd ‘𝑏) → 𝑎 = 𝑏)) | 
| 56 | 21, 24, 55 | syl2anb 598 | . . . 4
⊢ ((𝑎 ∈ 𝐺 ∧ 𝑏 ∈ 𝐺) → ((2nd ‘𝑎) = (2nd ‘𝑏) → 𝑎 = 𝑏)) | 
| 57 | 7, 56 | sylbid 240 | . . 3
⊢ ((𝑎 ∈ 𝐺 ∧ 𝑏 ∈ 𝐺) → ((𝐹‘𝑎) = (𝐹‘𝑏) → 𝑎 = 𝑏)) | 
| 58 | 57 | rgen2 3199 | . 2
⊢
∀𝑎 ∈
𝐺 ∀𝑏 ∈ 𝐺 ((𝐹‘𝑎) = (𝐹‘𝑏) → 𝑎 = 𝑏) | 
| 59 |  | dff13 7275 | . 2
⊢ (𝐹:𝐺–1-1→𝑃 ↔ (𝐹:𝐺⟶𝑃 ∧ ∀𝑎 ∈ 𝐺 ∀𝑏 ∈ 𝐺 ((𝐹‘𝑎) = (𝐹‘𝑏) → 𝑎 = 𝑏))) | 
| 60 | 4, 58, 59 | mpbir2an 711 | 1
⊢ 𝐹:𝐺–1-1→𝑃 |