Step | Hyp | Ref
| Expression |
1 | | diffi 8192 |
. . . . . . 7
|
2 | 1 | adantr 481 |
. . . . . 6
|
3 | 2 | 3ad2ant2 1083 |
. . . . 5
UPGraph
|
4 | | dmfi 8244 |
. . . . . . . . 9
|
5 | | rabfi 8185 |
. . . . . . . . 9
|
6 | 4, 5 | syl 17 |
. . . . . . . 8
|
7 | 6 | adantl 482 |
. . . . . . 7
|
8 | 7 | 3ad2ant2 1083 |
. . . . . 6
UPGraph
|
9 | 8 | adantr 481 |
. . . . 5
UPGraph
|
10 | | notnotb 304 |
. . . . . . . . . . . . . 14
|
11 | | notnotb 304 |
. . . . . . . . . . . . . . . . 17
|
12 | | upgruhgr 25997 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
UPGraph UHGraph |
13 | | edglnl.e |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
iEdg |
14 | 13 | uhgrfun 25961 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
UHGraph
|
15 | 12, 14 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
UPGraph
|
16 | 13 | iedgedg 25943 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
Edg |
17 | 15, 16 | sylan 488 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
UPGraph
Edg |
18 | | edglnl.v |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
Vtx |
19 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
Edg Edg |
20 | 18, 19 | upgredg 26032 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
UPGraph
Edg
|
21 | 17, 20 | syldan 487 |
. . . . . . . . . . . . . . . . . . . . . . . 24
UPGraph
|
22 | 21 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . 23
UPGraph
|
23 | 22 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . . . . . 22
UPGraph
|
24 | 23 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
UPGraph
|
25 | 24 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
UPGraph
|
26 | 25 | imp 445 |
. . . . . . . . . . . . . . . . . . 19
UPGraph
|
27 | | eldifsni 4320 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
28 | | eldifsni 4320 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
29 | | 3elpr2eq 4435 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
30 | 29 | expcom 451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
31 | 30 | 3expd 1284 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
32 | 31 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
33 | 32 | 3imp 1256 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
34 | 33 | con3d 148 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
35 | 34 | 3exp 1264 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
36 | 35 | com24 95 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
37 | 36 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
38 | | eleq2 2690 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
39 | | eleq2 2690 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
40 | | eleq2 2690 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
41 | 40 | notbid 308 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
42 | 39, 41 | imbi12d 334 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
43 | 38, 42 | imbi12d 334 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
44 | 37, 43 | syl5ibrcom 237 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
45 | 44 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
46 | 45 | rexlimdvva 3038 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
47 | 46 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
48 | 27, 28, 47 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . . 22
|
49 | 48 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
UPGraph
|
50 | 49 | imp 445 |
. . . . . . . . . . . . . . . . . . . 20
UPGraph
|
51 | 50 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
UPGraph
|
52 | 26, 51 | mpd 15 |
. . . . . . . . . . . . . . . . . 18
UPGraph
|
53 | 52 | imp 445 |
. . . . . . . . . . . . . . . . 17
UPGraph
|
54 | 11, 53 | syl5bir 233 |
. . . . . . . . . . . . . . . 16
UPGraph
|
55 | 54 | orrd 393 |
. . . . . . . . . . . . . . 15
UPGraph
|
56 | 55 | ex 450 |
. . . . . . . . . . . . . 14
UPGraph
|
57 | 10, 56 | syl5bir 233 |
. . . . . . . . . . . . 13
UPGraph
|
58 | 57 | orrd 393 |
. . . . . . . . . . . 12
UPGraph
|
59 | | anandi 871 |
. . . . . . . . . . . . . . 15
|
60 | 59 | bicomi 214 |
. . . . . . . . . . . . . 14
|
61 | 60 | notbii 310 |
. . . . . . . . . . . . 13
|
62 | | ianor 509 |
. . . . . . . . . . . . 13
|
63 | | ianor 509 |
. . . . . . . . . . . . . 14
|
64 | 63 | orbi2i 541 |
. . . . . . . . . . . . 13
|
65 | 61, 62, 64 | 3bitri 286 |
. . . . . . . . . . . 12
|
66 | 58, 65 | sylibr 224 |
. . . . . . . . . . 11
UPGraph
|
67 | 66 | ralrimiva 2966 |
. . . . . . . . . 10
UPGraph
|
68 | | inrab 3899 |
. . . . . . . . . . . 12
|
69 | 68 | eqeq1i 2627 |
. . . . . . . . . . 11
|
70 | | rabeq0 3957 |
. . . . . . . . . . 11
|
71 | 69, 70 | bitri 264 |
. . . . . . . . . 10
|
72 | 67, 71 | sylibr 224 |
. . . . . . . . 9
UPGraph
|
73 | 72 | ex 450 |
. . . . . . . 8
UPGraph
|
74 | 73 | orrd 393 |
. . . . . . 7
UPGraph
|
75 | 74 | ralrimivva 2971 |
. . . . . 6
UPGraph
|
76 | | eleq1w 2684 |
. . . . . . . . 9
|
77 | 76 | anbi2d 740 |
. . . . . . . 8
|
78 | 77 | rabbidv 3189 |
. . . . . . 7
|
79 | 78 | disjor 4634 |
. . . . . 6
Disj
|
80 | 75, 79 | sylibr 224 |
. . . . 5
UPGraph
Disj |
81 | 3, 9, 80 | hashiun 14554 |
. . . 4
UPGraph
|
82 | 81 | eqcomd 2628 |
. . 3
UPGraph
|
83 | 82 | oveq1d 6665 |
. 2
UPGraph
|
84 | 9 | ralrimiva 2966 |
. . . 4
UPGraph
|
85 | | iunfi 8254 |
. . . 4
|
86 | 3, 84, 85 | syl2anc 693 |
. . 3
UPGraph
|
87 | | rabfi 8185 |
. . . . . 6
|
88 | 4, 87 | syl 17 |
. . . . 5
|
89 | 88 | adantl 482 |
. . . 4
|
90 | 89 | 3ad2ant2 1083 |
. . 3
UPGraph
|
91 | | fveq2 6191 |
. . . . . . . 8
|
92 | 91 | eqeq1d 2624 |
. . . . . . 7
|
93 | 92 | elrab 3363 |
. . . . . 6
|
94 | | eldifn 3733 |
. . . . . . . . . . . . . . 15
|
95 | | eleq2 2690 |
. . . . . . . . . . . . . . . 16
|
96 | 95 | notbid 308 |
. . . . . . . . . . . . . . 15
|
97 | 94, 96 | syl5ibr 236 |
. . . . . . . . . . . . . 14
|
98 | 97 | adantl 482 |
. . . . . . . . . . . . 13
|
99 | 98 | adantl 482 |
. . . . . . . . . . . 12
UPGraph
|
100 | 99 | imp 445 |
. . . . . . . . . . 11
UPGraph
|
101 | 100 | intnand 962 |
. . . . . . . . . 10
UPGraph
|
102 | 101 | intnand 962 |
. . . . . . . . 9
UPGraph
|
103 | 102 | ralrimiva 2966 |
. . . . . . . 8
UPGraph
|
104 | | eliun 4524 |
. . . . . . . . . 10
|
105 | 104 | notbii 310 |
. . . . . . . . 9
|
106 | | ralnex 2992 |
. . . . . . . . 9
|
107 | 91 | eleq2d 2687 |
. . . . . . . . . . . . 13
|
108 | 91 | eleq2d 2687 |
. . . . . . . . . . . . 13
|
109 | 107, 108 | anbi12d 747 |
. . . . . . . . . . . 12
|
110 | 109 | elrab 3363 |
. . . . . . . . . . 11
|
111 | 110 | notbii 310 |
. . . . . . . . . 10
|
112 | 111 | ralbii 2980 |
. . . . . . . . 9
|
113 | 105, 106,
112 | 3bitr2i 288 |
. . . . . . . 8
|
114 | 103, 113 | sylibr 224 |
. . . . . . 7
UPGraph
|
115 | 114 | ex 450 |
. . . . . 6
UPGraph
|
116 | 93, 115 | syl5bi 232 |
. . . . 5
UPGraph
|
117 | 116 | ralrimiv 2965 |
. . . 4
UPGraph
|
118 | | disjr 4018 |
. . . 4
|
119 | 117, 118 | sylibr 224 |
. . 3
UPGraph
|
120 | | hashun 13171 |
. . 3
|
121 | 86, 90, 119, 120 | syl3anc 1326 |
. 2
UPGraph
|
122 | 18, 13 | edglnl 26038 |
. . . 4
UPGraph
|
123 | 122 | 3adant2 1080 |
. . 3
UPGraph
|
124 | 123 | fveq2d 6195 |
. 2
UPGraph
|
125 | 83, 121, 124 | 3eqtr2d 2662 |
1
UPGraph
|