Step | Hyp | Ref
| Expression |
1 | | iunrab 4567 |
. . . 4
|
2 | 1 | a1i 11 |
. . 3
UPGraph
|
3 | 2 | uneq1d 3766 |
. 2
UPGraph
|
4 | | unrab 3898 |
. . 3
|
5 | | simpl 473 |
. . . . . . . 8
|
6 | 5 | rexlimivw 3029 |
. . . . . . 7
|
7 | 6 | a1i 11 |
. . . . . 6
UPGraph |
8 | | snidg 4206 |
. . . . . . . 8
|
9 | 8 | ad2antlr 763 |
. . . . . . 7
UPGraph
|
10 | | eleq2 2690 |
. . . . . . 7
|
11 | 9, 10 | syl5ibrcom 237 |
. . . . . 6
UPGraph
|
12 | 7, 11 | jaod 395 |
. . . . 5
UPGraph |
13 | | upgruhgr 25997 |
. . . . . . . . 9
UPGraph UHGraph |
14 | | edglnl.e |
. . . . . . . . . 10
iEdg |
15 | 14 | uhgrfun 25961 |
. . . . . . . . 9
UHGraph
|
16 | 13, 15 | syl 17 |
. . . . . . . 8
UPGraph
|
17 | 16 | adantr 481 |
. . . . . . 7
UPGraph
|
18 | 14 | iedgedg 25943 |
. . . . . . 7
Edg |
19 | 17, 18 | sylan 488 |
. . . . . 6
UPGraph Edg |
20 | | edglnl.v |
. . . . . . . . . 10
Vtx |
21 | | eqid 2622 |
. . . . . . . . . 10
Edg Edg |
22 | 20, 21 | upgredg 26032 |
. . . . . . . . 9
UPGraph
Edg
|
23 | 22 | ex 450 |
. . . . . . . 8
UPGraph Edg
|
24 | 23 | ad2antrr 762 |
. . . . . . 7
UPGraph Edg
|
25 | | dfsn2 4190 |
. . . . . . . . . . . . . . . . . . . . . 22
|
26 | 25 | eqcomi 2631 |
. . . . . . . . . . . . . . . . . . . . 21
|
27 | | elsni 4194 |
. . . . . . . . . . . . . . . . . . . . . 22
|
28 | | sneq 4187 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
29 | 28 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . . 22
|
30 | 27, 29 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
|
31 | 26, 30 | syl5eq 2668 |
. . . . . . . . . . . . . . . . . . . 20
|
32 | 31, 26 | eleq2s 2719 |
. . . . . . . . . . . . . . . . . . 19
|
33 | | preq2 4269 |
. . . . . . . . . . . . . . . . . . . . 21
|
34 | 33 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . . 20
|
35 | 33 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . . 20
|
36 | 34, 35 | imbi12d 334 |
. . . . . . . . . . . . . . . . . . 19
|
37 | 32, 36 | mpbiri 248 |
. . . . . . . . . . . . . . . . . 18
|
38 | 37 | imp 445 |
. . . . . . . . . . . . . . . . 17
|
39 | 38 | olcd 408 |
. . . . . . . . . . . . . . . 16
|
40 | 39 | expcom 451 |
. . . . . . . . . . . . . . 15
|
41 | 40 | 3ad2ant3 1084 |
. . . . . . . . . . . . . 14
|
42 | 41 | com12 32 |
. . . . . . . . . . . . 13
|
43 | | simpr3 1069 |
. . . . . . . . . . . . . . . 16
|
44 | | simpl 473 |
. . . . . . . . . . . . . . . . . 18
|
45 | 44 | necomd 2849 |
. . . . . . . . . . . . . . . . 17
|
46 | | simpr2 1068 |
. . . . . . . . . . . . . . . . 17
|
47 | | prproe 4434 |
. . . . . . . . . . . . . . . . 17
|
48 | 43, 45, 46, 47 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
|
49 | | r19.42v 3092 |
. . . . . . . . . . . . . . . 16
|
50 | 43, 48, 49 | sylanbrc 698 |
. . . . . . . . . . . . . . 15
|
51 | 50 | orcd 407 |
. . . . . . . . . . . . . 14
|
52 | 51 | ex 450 |
. . . . . . . . . . . . 13
|
53 | 42, 52 | pm2.61ine 2877 |
. . . . . . . . . . . 12
|
54 | 53 | 3exp 1264 |
. . . . . . . . . . 11
|
55 | 54 | ad2antlr 763 |
. . . . . . . . . 10
UPGraph
|
56 | 55 | imp 445 |
. . . . . . . . 9
UPGraph
|
57 | | eleq2 2690 |
. . . . . . . . . 10
|
58 | | eleq2 2690 |
. . . . . . . . . . . . 13
|
59 | 57, 58 | anbi12d 747 |
. . . . . . . . . . . 12
|
60 | 59 | rexbidv 3052 |
. . . . . . . . . . 11
|
61 | | eqeq1 2626 |
. . . . . . . . . . 11
|
62 | 60, 61 | orbi12d 746 |
. . . . . . . . . 10
|
63 | 57, 62 | imbi12d 334 |
. . . . . . . . 9
|
64 | 56, 63 | syl5ibrcom 237 |
. . . . . . . 8
UPGraph
|
65 | 64 | rexlimdvva 3038 |
. . . . . . 7
UPGraph |
66 | 24, 65 | syld 47 |
. . . . . 6
UPGraph Edg |
67 | 19, 66 | mpd 15 |
. . . . 5
UPGraph |
68 | 12, 67 | impbid 202 |
. . . 4
UPGraph |
69 | 68 | rabbidva 3188 |
. . 3
UPGraph
|
70 | 4, 69 | syl5eq 2668 |
. 2
UPGraph
|
71 | 3, 70 | eqtrd 2656 |
1
UPGraph
|