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