Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . . . 5
Vtx Vtx |
2 | | ushgredgedgloop.i |
. . . . 5
iEdg |
3 | 1, 2 | ushgrf 25958 |
. . . 4
USHGraph Vtx |
4 | 3 | adantr 481 |
. . 3
USHGraph
Vtx |
5 | | ssrab2 3687 |
. . 3
|
6 | | f1ores 6151 |
. . 3
Vtx |
7 | 4, 5, 6 | sylancl 694 |
. 2
USHGraph
|
8 | | ushgredgedgloop.f |
. . . . 5
|
9 | | ushgredgedgloop.a |
. . . . . . 7
|
10 | 9 | a1i 11 |
. . . . . 6
USHGraph
|
11 | | eqidd 2623 |
. . . . . 6
USHGraph |
12 | 10, 11 | mpteq12dva 4732 |
. . . . 5
USHGraph
|
13 | 8, 12 | syl5eq 2668 |
. . . 4
USHGraph
|
14 | | f1f 6101 |
. . . . . . 7
Vtx
Vtx |
15 | 3, 14 | syl 17 |
. . . . . 6
USHGraph Vtx |
16 | 5 | a1i 11 |
. . . . . 6
USHGraph |
17 | 15, 16 | feqresmpt 6250 |
. . . . 5
USHGraph
|
18 | 17 | adantr 481 |
. . . 4
USHGraph
|
19 | 13, 18 | eqtr4d 2659 |
. . 3
USHGraph
|
20 | | ushgruhgr 25964 |
. . . . . . . 8
USHGraph UHGraph |
21 | | eqid 2622 |
. . . . . . . . 9
iEdg iEdg |
22 | 21 | uhgrfun 25961 |
. . . . . . . 8
UHGraph
iEdg |
23 | 20, 22 | syl 17 |
. . . . . . 7
USHGraph
iEdg |
24 | 2 | funeqi 5909 |
. . . . . . 7
iEdg |
25 | 23, 24 | sylibr 224 |
. . . . . 6
USHGraph
|
26 | 25 | adantr 481 |
. . . . 5
USHGraph
|
27 | | dfimafn 6245 |
. . . . 5
|
28 | 26, 5, 27 | sylancl 694 |
. . . 4
USHGraph
|
29 | | fveq2 6191 |
. . . . . . . . . . 11
|
30 | 29 | eqeq1d 2624 |
. . . . . . . . . 10
|
31 | 30 | elrab 3363 |
. . . . . . . . 9
|
32 | | simpl 473 |
. . . . . . . . . . . . . . 15
|
33 | | fvelrn 6352 |
. . . . . . . . . . . . . . . 16
|
34 | 2 | eqcomi 2631 |
. . . . . . . . . . . . . . . . 17
iEdg |
35 | 34 | rneqi 5352 |
. . . . . . . . . . . . . . . 16
iEdg |
36 | 33, 35 | syl6eleqr 2712 |
. . . . . . . . . . . . . . 15
iEdg |
37 | 26, 32, 36 | syl2an 494 |
. . . . . . . . . . . . . 14
USHGraph iEdg |
38 | 37 | 3adant3 1081 |
. . . . . . . . . . . . 13
USHGraph iEdg |
39 | | eleq1 2689 |
. . . . . . . . . . . . . . 15
iEdg
iEdg |
40 | 39 | eqcoms 2630 |
. . . . . . . . . . . . . 14
iEdg
iEdg |
41 | 40 | 3ad2ant3 1084 |
. . . . . . . . . . . . 13
USHGraph iEdg
iEdg |
42 | 38, 41 | mpbird 247 |
. . . . . . . . . . . 12
USHGraph iEdg |
43 | | ushgredgedgloop.e |
. . . . . . . . . . . . . . . 16
Edg |
44 | | edgval 25941 |
. . . . . . . . . . . . . . . . 17
Edg iEdg |
45 | 44 | a1i 11 |
. . . . . . . . . . . . . . . 16
USHGraph Edg iEdg |
46 | 43, 45 | syl5eq 2668 |
. . . . . . . . . . . . . . 15
USHGraph iEdg |
47 | 46 | eleq2d 2687 |
. . . . . . . . . . . . . 14
USHGraph iEdg |
48 | 47 | adantr 481 |
. . . . . . . . . . . . 13
USHGraph
iEdg |
49 | 48 | 3ad2ant1 1082 |
. . . . . . . . . . . 12
USHGraph iEdg |
50 | 42, 49 | mpbird 247 |
. . . . . . . . . . 11
USHGraph |
51 | | eqeq1 2626 |
. . . . . . . . . . . . . . 15
|
52 | 51 | biimpcd 239 |
. . . . . . . . . . . . . 14
|
53 | 52 | adantl 482 |
. . . . . . . . . . . . 13
|
54 | 53 | a1i 11 |
. . . . . . . . . . . 12
USHGraph
|
55 | 54 | 3imp 1256 |
. . . . . . . . . . 11
USHGraph |
56 | 50, 55 | jca 554 |
. . . . . . . . . 10
USHGraph
|
57 | 56 | 3exp 1264 |
. . . . . . . . 9
USHGraph
|
58 | 31, 57 | syl5bi 232 |
. . . . . . . 8
USHGraph
|
59 | 58 | rexlimdv 3030 |
. . . . . . 7
USHGraph
|
60 | | funfn 5918 |
. . . . . . . . . . . . . 14
iEdg iEdg iEdg |
61 | 60 | biimpi 206 |
. . . . . . . . . . . . 13
iEdg iEdg iEdg |
62 | 23, 61 | syl 17 |
. . . . . . . . . . . 12
USHGraph iEdg iEdg |
63 | | fvelrnb 6243 |
. . . . . . . . . . . 12
iEdg iEdg iEdg
iEdgiEdg |
64 | 62, 63 | syl 17 |
. . . . . . . . . . 11
USHGraph iEdg iEdgiEdg |
65 | 34 | dmeqi 5325 |
. . . . . . . . . . . . . . . . . . . . . 22
iEdg |
66 | 65 | eleq2i 2693 |
. . . . . . . . . . . . . . . . . . . . 21
iEdg
|
67 | 66 | biimpi 206 |
. . . . . . . . . . . . . . . . . . . 20
iEdg |
68 | 67 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
iEdg iEdg
|
69 | 68 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
USHGraph iEdg iEdg |
70 | 34 | fveq1i 6192 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
iEdg |
71 | 70 | eqeq2i 2634 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
iEdg |
72 | 71 | biimpi 206 |
. . . . . . . . . . . . . . . . . . . . . . . 24
iEdg
|
73 | 72 | eqcoms 2630 |
. . . . . . . . . . . . . . . . . . . . . . 23
iEdg |
74 | 73 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . . . . 22
iEdg
|
75 | 74 | biimpcd 239 |
. . . . . . . . . . . . . . . . . . . . 21
iEdg |
76 | 75 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
USHGraph
iEdg |
77 | 76 | adantld 483 |
. . . . . . . . . . . . . . . . . . 19
USHGraph
iEdg iEdg
|
78 | 77 | imp 445 |
. . . . . . . . . . . . . . . . . 18
USHGraph iEdg iEdg |
79 | 69, 78 | jca 554 |
. . . . . . . . . . . . . . . . 17
USHGraph iEdg iEdg |
80 | 79, 31 | sylibr 224 |
. . . . . . . . . . . . . . . 16
USHGraph iEdg iEdg |
81 | 70 | eqeq1i 2627 |
. . . . . . . . . . . . . . . . . . 19
iEdg |
82 | 81 | biimpi 206 |
. . . . . . . . . . . . . . . . . 18
iEdg |
83 | 82 | adantl 482 |
. . . . . . . . . . . . . . . . 17
iEdg iEdg
|
84 | 83 | adantl 482 |
. . . . . . . . . . . . . . . 16
USHGraph iEdg iEdg |
85 | 80, 84 | jca 554 |
. . . . . . . . . . . . . . 15
USHGraph iEdg iEdg
|
86 | 85 | ex 450 |
. . . . . . . . . . . . . 14
USHGraph
iEdg iEdg
|
87 | 86 | reximdv2 3014 |
. . . . . . . . . . . . 13
USHGraph
iEdgiEdg
|
88 | 87 | ex 450 |
. . . . . . . . . . . 12
USHGraph iEdgiEdg |
89 | 88 | com23 86 |
. . . . . . . . . . 11
USHGraph iEdgiEdg
|
90 | 64, 89 | sylbid 230 |
. . . . . . . . . 10
USHGraph iEdg
|
91 | 47, 90 | sylbid 230 |
. . . . . . . . 9
USHGraph
|
92 | 91 | impd 447 |
. . . . . . . 8
USHGraph |
93 | 92 | adantr 481 |
. . . . . . 7
USHGraph
|
94 | 59, 93 | impbid 202 |
. . . . . 6
USHGraph
|
95 | | vex 3203 |
. . . . . . 7
|
96 | | eqeq2 2633 |
. . . . . . . 8
|
97 | 96 | rexbidv 3052 |
. . . . . . 7
|
98 | 95, 97 | elab 3350 |
. . . . . 6
|
99 | | eqeq1 2626 |
. . . . . . 7
|
100 | | ushgredgedgloop.b |
. . . . . . 7
|
101 | 99, 100 | elrab2 3366 |
. . . . . 6
|
102 | 94, 98, 101 | 3bitr4g 303 |
. . . . 5
USHGraph
|
103 | 102 | eqrdv 2620 |
. . . 4
USHGraph
|
104 | 28, 103 | eqtr2d 2657 |
. . 3
USHGraph
|
105 | 19, 10, 104 | f1oeq123d 6133 |
. 2
USHGraph
|
106 | 7, 105 | mpbird 247 |
1
USHGraph
|