Step | Hyp | Ref
| Expression |
1 | | uspgrsprf.p |
. . 3
Pairs |
2 | | uspgrsprf.g |
. . 3
USPGraph Vtx Edg |
3 | | uspgrsprf.f |
. . 3
|
4 | 1, 2, 3 | uspgrsprf 41754 |
. 2
|
5 | 1, 2, 3 | uspgrsprfv 41753 |
. . . . 5
|
6 | 1, 2, 3 | uspgrsprfv 41753 |
. . . . 5
|
7 | 5, 6 | eqeqan12d 2638 |
. . . 4
|
8 | 2 | eleq2i 2693 |
. . . . . 6
USPGraph Vtx Edg |
9 | | elopab 4983 |
. . . . . 6
USPGraph
Vtx Edg
USPGraph Vtx
Edg |
10 | | opeq12 4404 |
. . . . . . . . 9
|
11 | 10 | eqeq2d 2632 |
. . . . . . . 8
|
12 | | eqeq1 2626 |
. . . . . . . . . 10
|
13 | 12 | adantr 481 |
. . . . . . . . 9
|
14 | | eqeq2 2633 |
. . . . . . . . . . 11
Vtx
Vtx |
15 | | eqeq2 2633 |
. . . . . . . . . . 11
Edg
Edg |
16 | 14, 15 | bi2anan9 917 |
. . . . . . . . . 10
Vtx Edg Vtx Edg |
17 | 16 | rexbidv 3052 |
. . . . . . . . 9
USPGraph Vtx
Edg USPGraph Vtx Edg |
18 | 13, 17 | anbi12d 747 |
. . . . . . . 8
USPGraph Vtx Edg
USPGraph Vtx Edg |
19 | 11, 18 | anbi12d 747 |
. . . . . . 7
USPGraph Vtx
Edg
USPGraph Vtx Edg |
20 | 19 | cbvex2v 2287 |
. . . . . 6
USPGraph
Vtx Edg
USPGraph Vtx
Edg |
21 | 8, 9, 20 | 3bitri 286 |
. . . . 5
USPGraph Vtx
Edg |
22 | 2 | eleq2i 2693 |
. . . . . 6
USPGraph Vtx Edg |
23 | | elopab 4983 |
. . . . . 6
USPGraph
Vtx Edg
USPGraph Vtx
Edg |
24 | 22, 23 | bitri 264 |
. . . . 5
USPGraph Vtx
Edg |
25 | | eqeq2 2633 |
. . . . . . . . . . . . . . . 16
|
26 | | opeq12 4404 |
. . . . . . . . . . . . . . . . . 18
|
27 | 26 | ex 450 |
. . . . . . . . . . . . . . . . 17
|
28 | 27 | equcoms 1947 |
. . . . . . . . . . . . . . . 16
|
29 | 25, 28 | syl6bir 244 |
. . . . . . . . . . . . . . 15
|
30 | 29 | ad2antrl 764 |
. . . . . . . . . . . . . 14
USPGraph
Vtx Edg
|
31 | 30 | com12 32 |
. . . . . . . . . . . . 13
USPGraph
Vtx Edg |
32 | 31 | ad2antrl 764 |
. . . . . . . . . . . 12
USPGraph
Vtx Edg USPGraph
Vtx Edg |
33 | 32 | imp 445 |
. . . . . . . . . . 11
USPGraph
Vtx Edg USPGraph
Vtx Edg
|
34 | | vex 3203 |
. . . . . . . . . . . . . 14
|
35 | | vex 3203 |
. . . . . . . . . . . . . 14
|
36 | 34, 35 | op2ndd 7179 |
. . . . . . . . . . . . 13
|
37 | 36 | ad2antrl 764 |
. . . . . . . . . . . 12
USPGraph
Vtx Edg USPGraph
Vtx Edg |
38 | | vex 3203 |
. . . . . . . . . . . . . . 15
|
39 | | vex 3203 |
. . . . . . . . . . . . . . 15
|
40 | 38, 39 | op2ndd 7179 |
. . . . . . . . . . . . . 14
|
41 | 40 | adantr 481 |
. . . . . . . . . . . . 13
USPGraph
Vtx Edg |
42 | 41 | adantr 481 |
. . . . . . . . . . . 12
USPGraph
Vtx Edg USPGraph
Vtx Edg |
43 | 37, 42 | eqeq12d 2637 |
. . . . . . . . . . 11
USPGraph
Vtx Edg USPGraph
Vtx Edg
|
44 | | eqeq12 2635 |
. . . . . . . . . . . . . . . 16
|
45 | 44 | ex 450 |
. . . . . . . . . . . . . . 15
|
46 | 45 | adantr 481 |
. . . . . . . . . . . . . 14
USPGraph
Vtx Edg
|
47 | 46 | com12 32 |
. . . . . . . . . . . . 13
USPGraph Vtx Edg
|
48 | 47 | adantr 481 |
. . . . . . . . . . . 12
USPGraph
Vtx Edg USPGraph
Vtx Edg
|
49 | 48 | imp 445 |
. . . . . . . . . . 11
USPGraph
Vtx Edg USPGraph
Vtx Edg |
50 | 33, 43, 49 | 3imtr4d 283 |
. . . . . . . . . 10
USPGraph
Vtx Edg USPGraph
Vtx Edg |
51 | 50 | ex 450 |
. . . . . . . . 9
USPGraph
Vtx Edg USPGraph
Vtx Edg |
52 | 51 | exlimivv 1860 |
. . . . . . . 8
USPGraph
Vtx Edg USPGraph
Vtx Edg |
53 | 52 | com12 32 |
. . . . . . 7
USPGraph
Vtx Edg USPGraph
Vtx Edg |
54 | 53 | exlimivv 1860 |
. . . . . 6
USPGraph
Vtx Edg USPGraph
Vtx Edg |
55 | 54 | imp 445 |
. . . . 5
USPGraph
Vtx Edg USPGraph Vtx Edg
|
56 | 21, 24, 55 | syl2anb 496 |
. . . 4
|
57 | 7, 56 | sylbid 230 |
. . 3
|
58 | 57 | rgen2a 2977 |
. 2
|
59 | | dff13 6512 |
. 2
|
60 | 4, 58, 59 | mpbir2an 955 |
1
|