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 | | subgruhgrfun 26174 |
. . . . . . . . 9
UHGraph
SubGraph
iEdg |
8 | 7 | ancoms 469 |
. . . . . . . 8
SubGraph
UHGraph
iEdg |
9 | 8 | adantl 482 |
. . . . . . 7
Vtx
Vtx
iEdg
iEdg
Edg
Vtx
SubGraph UHGraph iEdg |
10 | | funfn 5918 |
. . . . . . 7
iEdg iEdg iEdg |
11 | 9, 10 | sylib 208 |
. . . . . 6
Vtx
Vtx
iEdg
iEdg
Edg
Vtx
SubGraph UHGraph iEdg iEdg |
12 | | simplrr 801 |
. . . . . . . . 9
Vtx Vtx iEdg iEdg Edg Vtx SubGraph
UHGraph
iEdg
UHGraph |
13 | | simplrl 800 |
. . . . . . . . 9
Vtx Vtx iEdg iEdg Edg Vtx SubGraph
UHGraph
iEdg SubGraph |
14 | | simpr 477 |
. . . . . . . . 9
Vtx Vtx iEdg iEdg Edg Vtx SubGraph
UHGraph
iEdg
iEdg |
15 | 1, 3, 12, 13, 14 | subgruhgredgd 26176 |
. . . . . . . 8
Vtx Vtx iEdg iEdg Edg Vtx SubGraph
UHGraph
iEdg iEdg Vtx |
16 | 15 | ralrimiva 2966 |
. . . . . . 7
Vtx
Vtx
iEdg
iEdg
Edg
Vtx
SubGraph UHGraph iEdgiEdg Vtx |
17 | | fnfvrnss 6390 |
. . . . . . 7
iEdg iEdg
iEdgiEdg Vtx
iEdg
Vtx |
18 | 11, 16, 17 | syl2anc 693 |
. . . . . 6
Vtx
Vtx
iEdg
iEdg
Edg
Vtx
SubGraph UHGraph iEdg Vtx
|
19 | | df-f 5892 |
. . . . . 6
iEdg iEdgVtx
iEdg iEdg iEdg Vtx
|
20 | 11, 18, 19 | sylanbrc 698 |
. . . . 5
Vtx
Vtx
iEdg
iEdg
Edg
Vtx
SubGraph UHGraph iEdg iEdgVtx
|
21 | | subgrv 26162 |
. . . . . . . 8
SubGraph
|
22 | 1, 3 | isuhgr 25955 |
. . . . . . . . 9
UHGraph iEdg iEdgVtx |
23 | 22 | adantr 481 |
. . . . . . . 8
UHGraph
iEdg iEdgVtx |
24 | 21, 23 | syl 17 |
. . . . . . 7
SubGraph UHGraph iEdg iEdgVtx
|
25 | 24 | adantr 481 |
. . . . . 6
SubGraph
UHGraph UHGraph iEdg iEdgVtx
|
26 | 25 | adantl 482 |
. . . . 5
Vtx
Vtx
iEdg
iEdg
Edg
Vtx
SubGraph UHGraph
UHGraph iEdg iEdgVtx |
27 | 20, 26 | mpbird 247 |
. . . 4
Vtx
Vtx
iEdg
iEdg
Edg
Vtx
SubGraph UHGraph UHGraph |
28 | 27 | ex 450 |
. . 3
Vtx Vtx iEdg iEdg Edg Vtx SubGraph
UHGraph UHGraph |
29 | 6, 28 | syl 17 |
. 2
SubGraph SubGraph UHGraph UHGraph
|
30 | 29 | anabsi8 861 |
1
UHGraph
SubGraph UHGraph |