Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . . . . 6
Vtx Vtx |
2 | | eqid 2622 |
. . . . . 6
Edg Edg |
3 | 1, 2 | iscplgredg 26313 |
. . . . 5
ComplGraph ComplGraph
Vtx Vtx
Edg |
4 | | edgval 25941 |
. . . . . . 7
Edg iEdg |
5 | 4 | a1i 11 |
. . . . . 6
ComplGraph Edg iEdg |
6 | | simpl 473 |
. . . . . . . . . . . 12
Vtx Vtx iEdg iEdg
Vtx Vtx |
7 | 6 | adantl 482 |
. . . . . . . . . . 11
Edg iEdg
Vtx Vtx iEdg iEdg Vtx Vtx |
8 | 6 | difeq1d 3727 |
. . . . . . . . . . . . 13
Vtx Vtx iEdg iEdg
Vtx Vtx
|
9 | 8 | adantl 482 |
. . . . . . . . . . . 12
Edg iEdg
Vtx Vtx iEdg iEdg Vtx Vtx |
10 | | edgval 25941 |
. . . . . . . . . . . . . . . 16
Edg iEdg |
11 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
Vtx Vtx iEdg iEdg
iEdg iEdg |
12 | 11 | rneqd 5353 |
. . . . . . . . . . . . . . . 16
Vtx Vtx iEdg iEdg
iEdg iEdg |
13 | 10, 12 | syl5eq 2668 |
. . . . . . . . . . . . . . 15
Vtx Vtx iEdg iEdg
Edg iEdg |
14 | 13 | adantl 482 |
. . . . . . . . . . . . . 14
Edg iEdg
Vtx Vtx iEdg iEdg Edg iEdg |
15 | | simpl 473 |
. . . . . . . . . . . . . 14
Edg iEdg
Vtx Vtx iEdg iEdg Edg iEdg |
16 | 14, 15 | eqtr4d 2659 |
. . . . . . . . . . . . 13
Edg iEdg
Vtx Vtx iEdg iEdg Edg Edg |
17 | 16 | rexeqdv 3145 |
. . . . . . . . . . . 12
Edg iEdg
Vtx Vtx iEdg iEdg
Edg Edg |
18 | 9, 17 | raleqbidv 3152 |
. . . . . . . . . . 11
Edg iEdg
Vtx Vtx iEdg iEdg
Vtx Edg Vtx Edg |
19 | 7, 18 | raleqbidv 3152 |
. . . . . . . . . 10
Edg iEdg
Vtx Vtx iEdg iEdg
Vtx Vtx
Edg
Vtx
Vtx Edg |
20 | 19 | biimpar 502 |
. . . . . . . . 9
Edg iEdg Vtx Vtx iEdg iEdg
Vtx Vtx
Edg
Vtx Vtx
Edg |
21 | | vex 3203 |
. . . . . . . . . 10
|
22 | | eqid 2622 |
. . . . . . . . . . 11
Vtx Vtx |
23 | | eqid 2622 |
. . . . . . . . . . 11
Edg Edg |
24 | 22, 23 | iscplgredg 26313 |
. . . . . . . . . 10
ComplGraph Vtx
Vtx Edg |
25 | 21, 24 | ax-mp 5 |
. . . . . . . . 9
ComplGraph Vtx
Vtx Edg |
26 | 20, 25 | sylibr 224 |
. . . . . . . 8
Edg iEdg Vtx Vtx iEdg iEdg
Vtx Vtx
Edg
ComplGraph |
27 | 26 | expcom 451 |
. . . . . . 7
Vtx Vtx
Edg Edg iEdg Vtx Vtx iEdg iEdg ComplGraph |
28 | 27 | expd 452 |
. . . . . 6
Vtx Vtx
Edg Edg iEdg
Vtx Vtx iEdg iEdg
ComplGraph |
29 | 5, 28 | syl5com 31 |
. . . . 5
ComplGraph Vtx
Vtx Edg
Vtx Vtx iEdg iEdg
ComplGraph |
30 | 3, 29 | sylbid 230 |
. . . 4
ComplGraph ComplGraph Vtx Vtx iEdg iEdg
ComplGraph |
31 | 30 | pm2.43i 52 |
. . 3
ComplGraph Vtx Vtx iEdg iEdg
ComplGraph |
32 | 31 | alrimiv 1855 |
. 2
ComplGraph Vtx Vtx iEdg iEdg
ComplGraph |
33 | | fvexd 6203 |
. 2
ComplGraph Vtx |
34 | | fvexd 6203 |
. 2
ComplGraph iEdg |
35 | 32, 33, 34 | gropeld 25925 |
1
ComplGraph Vtx iEdg ComplGraph |