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