Proof of Theorem subgruhgredgd
Step | Hyp | Ref
| Expression |
1 | | subgruhgredgd.s |
. . 3
SubGraph |
2 | | subgruhgredgd.v |
. . . 4
Vtx |
3 | | eqid 2622 |
. . . 4
Vtx Vtx |
4 | | subgruhgredgd.i |
. . . 4
iEdg |
5 | | eqid 2622 |
. . . 4
iEdg iEdg |
6 | | eqid 2622 |
. . . 4
Edg Edg |
7 | 2, 3, 4, 5, 6 | subgrprop2 26166 |
. . 3
SubGraph Vtx iEdg
Edg
|
8 | 1, 7 | syl 17 |
. 2
Vtx iEdg Edg |
9 | | simpr3 1069 |
. . . 4
Vtx
iEdg Edg Edg |
10 | | subgruhgredgd.g |
. . . . . . . . 9
UHGraph
|
11 | | subgruhgrfun 26174 |
. . . . . . . . 9
UHGraph
SubGraph
iEdg |
12 | 10, 1, 11 | syl2anc 693 |
. . . . . . . 8
iEdg |
13 | | subgruhgredgd.x |
. . . . . . . . 9
|
14 | 4 | dmeqi 5325 |
. . . . . . . . 9
iEdg |
15 | 13, 14 | syl6eleq 2711 |
. . . . . . . 8
iEdg |
16 | 12, 15 | jca 554 |
. . . . . . 7
iEdg iEdg |
17 | 16 | adantr 481 |
. . . . . 6
Vtx
iEdg Edg
iEdg
iEdg |
18 | 4 | fveq1i 6192 |
. . . . . . 7
iEdg |
19 | | fvelrn 6352 |
. . . . . . 7
iEdg
iEdg
iEdg iEdg |
20 | 18, 19 | syl5eqel 2705 |
. . . . . 6
iEdg
iEdg
iEdg |
21 | 17, 20 | syl 17 |
. . . . 5
Vtx
iEdg Edg iEdg |
22 | | edgval 25941 |
. . . . 5
Edg iEdg |
23 | 21, 22 | syl6eleqr 2712 |
. . . 4
Vtx
iEdg Edg Edg |
24 | 9, 23 | sseldd 3604 |
. . 3
Vtx
iEdg Edg |
25 | 5 | uhgrfun 25961 |
. . . . . . 7
UHGraph
iEdg |
26 | 10, 25 | syl 17 |
. . . . . 6
iEdg |
27 | 26 | adantr 481 |
. . . . 5
Vtx
iEdg Edg iEdg |
28 | | simpr2 1068 |
. . . . 5
Vtx
iEdg Edg iEdg |
29 | 13 | adantr 481 |
. . . . 5
Vtx
iEdg Edg
|
30 | | funssfv 6209 |
. . . . . 6
iEdg
iEdg iEdg |
31 | 30 | eqcomd 2628 |
. . . . 5
iEdg
iEdg iEdg |
32 | 27, 28, 29, 31 | syl3anc 1326 |
. . . 4
Vtx
iEdg Edg iEdg |
33 | 10 | adantr 481 |
. . . . 5
Vtx
iEdg Edg
UHGraph |
34 | | funfn 5918 |
. . . . . . 7
iEdg iEdg iEdg |
35 | 26, 34 | sylib 208 |
. . . . . 6
iEdg iEdg |
36 | 35 | adantr 481 |
. . . . 5
Vtx
iEdg Edg iEdg iEdg |
37 | | subgreldmiedg 26175 |
. . . . . . 7
SubGraph
iEdg
iEdg |
38 | 1, 15, 37 | syl2anc 693 |
. . . . . 6
iEdg |
39 | 38 | adantr 481 |
. . . . 5
Vtx
iEdg Edg
iEdg |
40 | 5 | uhgrn0 25962 |
. . . . 5
UHGraph
iEdg iEdg
iEdg iEdg |
41 | 33, 36, 39, 40 | syl3anc 1326 |
. . . 4
Vtx
iEdg Edg iEdg |
42 | 32, 41 | eqnetrd 2861 |
. . 3
Vtx
iEdg Edg |
43 | | eldifsn 4317 |
. . 3
|
44 | 24, 42, 43 | sylanbrc 698 |
. 2
Vtx
iEdg Edg |
45 | 8, 44 | mpdan 702 |
1
|