Step | Hyp | Ref
| Expression |
1 | | df-uhgr 39159 |
. . 3
UHGraph   Vtx   ![]. ].](_drbrack.gif)  iEdg   ![]. ].](_drbrack.gif)            |
2 | 1 | eleq2i 2523 |
. 2
 UHGraph   Vtx   ![]. ].](_drbrack.gif)  iEdg   ![]. ].](_drbrack.gif)             |
3 | | fveq2 5870 |
. . . . 5
 iEdg  iEdg    |
4 | | isuhgr.e |
. . . . 5
iEdg   |
5 | 3, 4 | syl6eqr 2505 |
. . . 4
 iEdg    |
6 | 3 | dmeqd 5040 |
. . . . 5
 iEdg  iEdg    |
7 | 4 | eqcomi 2462 |
. . . . . 6
iEdg   |
8 | 7 | dmeqi 5039 |
. . . . 5
iEdg   |
9 | 6, 8 | syl6eq 2503 |
. . . 4
 iEdg    |
10 | | fveq2 5870 |
. . . . . . 7
 Vtx  Vtx    |
11 | | isuhgr.v |
. . . . . . 7
Vtx   |
12 | 10, 11 | syl6eqr 2505 |
. . . . . 6
 Vtx    |
13 | 12 | pweqd 3958 |
. . . . 5
  Vtx     |
14 | 13 | difeq1d 3552 |
. . . 4
   Vtx            |
15 | 5, 9, 14 | feq123d 5723 |
. . 3
  iEdg    iEdg      Vtx    
            |
16 | | fvex 5880 |
. . . . . 6
Vtx   |
17 | 16 | a1i 11 |
. . . . 5
 Vtx    |
18 | | fveq2 5870 |
. . . . 5
 Vtx  Vtx    |
19 | | fvex 5880 |
. . . . . . 7
iEdg   |
20 | 19 | a1i 11 |
. . . . . 6
 
Vtx   iEdg    |
21 | | fveq2 5870 |
. . . . . . 7
 iEdg  iEdg    |
22 | 21 | adantr 467 |
. . . . . 6
 
Vtx   iEdg  iEdg    |
23 | | simpr 463 |
. . . . . . 7
   Vtx   iEdg   iEdg    |
24 | 23 | dmeqd 5040 |
. . . . . . 7
   Vtx   iEdg  
iEdg    |
25 | | simpr 463 |
. . . . . . . . . 10
 
Vtx   Vtx    |
26 | 25 | pweqd 3958 |
. . . . . . . . 9
 
Vtx   
 Vtx    |
27 | 26 | difeq1d 3552 |
. . . . . . . 8
 
Vtx    
     Vtx       |
28 | 27 | adantr 467 |
. . . . . . 7
   Vtx   iEdg          Vtx       |
29 | 23, 24, 28 | feq123d 5723 |
. . . . . 6
   Vtx   iEdg            
iEdg    iEdg      Vtx        |
30 | 20, 22, 29 | sbcied2 3307 |
. . . . 5
 
Vtx     iEdg   ![]. ].](_drbrack.gif)          iEdg    iEdg      Vtx        |
31 | 17, 18, 30 | sbcied2 3307 |
. . . 4
   Vtx   ![]. ].](_drbrack.gif)  iEdg   ![]. ].](_drbrack.gif)         
iEdg    iEdg      Vtx        |
32 | 31 | cbvabv 2577 |
. . 3
  Vtx   ![]. ].](_drbrack.gif)  iEdg   ![]. ].](_drbrack.gif)           
iEdg    iEdg      Vtx 
     |
33 | 15, 32 | elab2g 3189 |
. 2
 
  Vtx   ![]. ].](_drbrack.gif)  iEdg   ![]. ].](_drbrack.gif)          
            |
34 | 2, 33 | syl5bb 261 |
1
 
UHGraph             |