Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . . 4
Vtx Vtx |
2 | | eqid 2622 |
. . . 4
Vtx Vtx |
3 | | eqid 2622 |
. . . 4
iEdg iEdg |
4 | | eqid 2622 |
. . . 4
iEdg iEdg |
5 | | eqid 2622 |
. . . 4
Edg Edg |
6 | 1, 2, 3, 4, 5 | subgrprop2 26166 |
. . 3
SubGraph Vtx Vtx iEdg iEdg Edg Vtx |
7 | | usgruhgr 26078 |
. . . . . . . . . . 11
USGraph UHGraph |
8 | | subgruhgrfun 26174 |
. . . . . . . . . . 11
UHGraph
SubGraph
iEdg |
9 | 7, 8 | sylan 488 |
. . . . . . . . . 10
USGraph
SubGraph
iEdg |
10 | 9 | ancoms 469 |
. . . . . . . . 9
SubGraph
USGraph
iEdg |
11 | | funfn 5918 |
. . . . . . . . 9
iEdg iEdg iEdg |
12 | 10, 11 | sylib 208 |
. . . . . . . 8
SubGraph
USGraph iEdg iEdg |
13 | 12 | adantl 482 |
. . . . . . 7
Vtx
Vtx
iEdg
iEdg
Edg
Vtx
SubGraph USGraph iEdg iEdg |
14 | | simplrl 800 |
. . . . . . . . . 10
Vtx Vtx iEdg iEdg Edg Vtx SubGraph
USGraph
iEdg SubGraph |
15 | | usgrumgr 26074 |
. . . . . . . . . . . . 13
USGraph UMGraph |
16 | 15 | adantl 482 |
. . . . . . . . . . . 12
SubGraph
USGraph UMGraph |
17 | 16 | adantl 482 |
. . . . . . . . . . 11
Vtx
Vtx
iEdg
iEdg
Edg
Vtx
SubGraph USGraph UMGraph |
18 | 17 | adantr 481 |
. . . . . . . . . 10
Vtx Vtx iEdg iEdg Edg Vtx SubGraph
USGraph
iEdg
UMGraph |
19 | | simpr 477 |
. . . . . . . . . 10
Vtx Vtx iEdg iEdg Edg Vtx SubGraph
USGraph
iEdg
iEdg |
20 | 1, 3 | subumgredg2 26177 |
. . . . . . . . . 10
SubGraph
UMGraph
iEdg iEdg Vtx |
21 | 14, 18, 19, 20 | syl3anc 1326 |
. . . . . . . . 9
Vtx Vtx iEdg iEdg Edg Vtx SubGraph
USGraph
iEdg iEdg Vtx |
22 | 21 | ralrimiva 2966 |
. . . . . . . 8
Vtx
Vtx
iEdg
iEdg
Edg
Vtx
SubGraph USGraph iEdgiEdg Vtx |
23 | | fnfvrnss 6390 |
. . . . . . . 8
iEdg iEdg
iEdgiEdg Vtx
iEdg
Vtx |
24 | 13, 22, 23 | syl2anc 693 |
. . . . . . 7
Vtx
Vtx
iEdg
iEdg
Edg
Vtx
SubGraph USGraph iEdg Vtx |
25 | | df-f 5892 |
. . . . . . 7
iEdg iEdg Vtx
iEdg iEdg iEdg Vtx |
26 | 13, 24, 25 | sylanbrc 698 |
. . . . . 6
Vtx
Vtx
iEdg
iEdg
Edg
Vtx
SubGraph USGraph iEdg iEdg Vtx |
27 | | simp2 1062 |
. . . . . . . . 9
Vtx Vtx iEdg iEdg Edg Vtx iEdg iEdg |
28 | 2, 4 | usgrfs 26052 |
. . . . . . . . . . 11
USGraph iEdg iEdg Vtx |
29 | | df-f1 5893 |
. . . . . . . . . . . 12
iEdg iEdg Vtx
iEdg iEdg Vtx iEdg |
30 | | ffun 6048 |
. . . . . . . . . . . . 13
iEdg iEdg Vtx iEdg |
31 | 30 | anim1i 592 |
. . . . . . . . . . . 12
iEdg iEdg Vtx iEdg iEdg iEdg |
32 | 29, 31 | sylbi 207 |
. . . . . . . . . . 11
iEdg iEdg Vtx iEdg
iEdg |
33 | 28, 32 | syl 17 |
. . . . . . . . . 10
USGraph iEdg iEdg |
34 | 33 | adantl 482 |
. . . . . . . . 9
SubGraph
USGraph iEdg iEdg |
35 | 27, 34 | anim12ci 591 |
. . . . . . . 8
Vtx
Vtx
iEdg
iEdg
Edg
Vtx
SubGraph USGraph
iEdg
iEdg iEdg iEdg |
36 | | df-3an 1039 |
. . . . . . . 8
iEdg
iEdg iEdg iEdg
iEdg iEdg iEdg iEdg |
37 | 35, 36 | sylibr 224 |
. . . . . . 7
Vtx
Vtx
iEdg
iEdg
Edg
Vtx
SubGraph USGraph iEdg iEdg iEdg iEdg |
38 | | f1ssf1 6168 |
. . . . . . 7
iEdg
iEdg iEdg iEdg iEdg |
39 | 37, 38 | syl 17 |
. . . . . 6
Vtx
Vtx
iEdg
iEdg
Edg
Vtx
SubGraph USGraph iEdg |
40 | | df-f1 5893 |
. . . . . 6
iEdg iEdg Vtx
iEdg iEdg Vtx iEdg |
41 | 26, 39, 40 | sylanbrc 698 |
. . . . 5
Vtx
Vtx
iEdg
iEdg
Edg
Vtx
SubGraph USGraph iEdg iEdg Vtx |
42 | | subgrv 26162 |
. . . . . . . 8
SubGraph
|
43 | 1, 3 | isusgrs 26051 |
. . . . . . . . 9
USGraph iEdg iEdg Vtx |
44 | 43 | adantr 481 |
. . . . . . . 8
USGraph
iEdg iEdg Vtx |
45 | 42, 44 | syl 17 |
. . . . . . 7
SubGraph USGraph iEdg iEdg Vtx |
46 | 45 | adantr 481 |
. . . . . 6
SubGraph
USGraph USGraph iEdg iEdg Vtx |
47 | 46 | adantl 482 |
. . . . 5
Vtx
Vtx
iEdg
iEdg
Edg
Vtx
SubGraph USGraph
USGraph iEdg iEdg Vtx |
48 | 41, 47 | mpbird 247 |
. . . 4
Vtx
Vtx
iEdg
iEdg
Edg
Vtx
SubGraph USGraph USGraph |
49 | 48 | ex 450 |
. . 3
Vtx Vtx iEdg iEdg Edg Vtx SubGraph
USGraph USGraph |
50 | 6, 49 | syl 17 |
. 2
SubGraph SubGraph USGraph USGraph
|
51 | 50 | anabsi8 861 |
1
USGraph
SubGraph USGraph |