Step | Hyp | Ref
| Expression |
1 | | cusisusgra 25987 |
. . 3
⊢ (𝑉 ComplUSGrph 𝐸 → 𝑉 USGrph 𝐸) |
2 | | nbusgra 25957 |
. . . . . . 7
⊢ (𝑉 USGrph 𝐸 → (〈𝑉, 𝐸〉 Neighbors 𝑁) = {𝑛 ∈ 𝑉 ∣ {𝑁, 𝑛} ∈ ran 𝐸}) |
3 | 2 | adantr 480 |
. . . . . 6
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ComplUSGrph 𝐸) → (〈𝑉, 𝐸〉 Neighbors 𝑁) = {𝑛 ∈ 𝑉 ∣ {𝑁, 𝑛} ∈ ran 𝐸}) |
4 | 3 | adantr 480 |
. . . . 5
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ComplUSGrph 𝐸) ∧ 𝑁 ∈ 𝑉) → (〈𝑉, 𝐸〉 Neighbors 𝑁) = {𝑛 ∈ 𝑉 ∣ {𝑁, 𝑛} ∈ ran 𝐸}) |
5 | | usgrav 25867 |
. . . . . . . . . 10
⊢ (𝑉 USGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
6 | | iscusgra 25985 |
. . . . . . . . . 10
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑉 ComplUSGrph 𝐸 ↔ (𝑉 USGrph 𝐸 ∧ ∀𝑥 ∈ 𝑉 ∀𝑘 ∈ (𝑉 ∖ {𝑥}){𝑘, 𝑥} ∈ ran 𝐸))) |
7 | 5, 6 | syl 17 |
. . . . . . . . 9
⊢ (𝑉 USGrph 𝐸 → (𝑉 ComplUSGrph 𝐸 ↔ (𝑉 USGrph 𝐸 ∧ ∀𝑥 ∈ 𝑉 ∀𝑘 ∈ (𝑉 ∖ {𝑥}){𝑘, 𝑥} ∈ ran 𝐸))) |
8 | 7 | biimpa 500 |
. . . . . . . 8
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ComplUSGrph 𝐸) → (𝑉 USGrph 𝐸 ∧ ∀𝑥 ∈ 𝑉 ∀𝑘 ∈ (𝑉 ∖ {𝑥}){𝑘, 𝑥} ∈ ran 𝐸)) |
9 | | df-ral 2901 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
𝑉 ∀𝑘 ∈ (𝑉 ∖ {𝑥}){𝑘, 𝑥} ∈ ran 𝐸 ↔ ∀𝑥(𝑥 ∈ 𝑉 → ∀𝑘 ∈ (𝑉 ∖ {𝑥}){𝑘, 𝑥} ∈ ran 𝐸)) |
10 | | preq2 4213 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑥 → {𝑁, 𝑛} = {𝑁, 𝑥}) |
11 | 10 | eleq1d 2672 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑥 → ({𝑁, 𝑛} ∈ ran 𝐸 ↔ {𝑁, 𝑥} ∈ ran 𝐸)) |
12 | 11 | elrab 3331 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ {𝑛 ∈ 𝑉 ∣ {𝑁, 𝑛} ∈ ran 𝐸} ↔ (𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸)) |
13 | | pm2.24 120 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ 𝑉 → (¬ 𝑥 ∈ 𝑉 → 𝑥 ∈ (𝑉 ∖ {𝑁}))) |
14 | 13 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) → (¬ 𝑥 ∈ 𝑉 → 𝑥 ∈ (𝑉 ∖ {𝑁}))) |
15 | 14 | com12 32 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
𝑥 ∈ 𝑉 → ((𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) → 𝑥 ∈ (𝑉 ∖ {𝑁}))) |
16 | | eldif 3550 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ (𝑉 ∖ {𝑁}) ↔ (𝑥 ∈ 𝑉 ∧ ¬ 𝑥 ∈ {𝑁})) |
17 | | pm2.24 120 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ 𝑉 → (¬ 𝑥 ∈ 𝑉 → (𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸))) |
18 | 17 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ 𝑉 ∧ ¬ 𝑥 ∈ {𝑁}) → (¬ 𝑥 ∈ 𝑉 → (𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸))) |
19 | 16, 18 | sylbi 206 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (𝑉 ∖ {𝑁}) → (¬ 𝑥 ∈ 𝑉 → (𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸))) |
20 | 19 | com12 32 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
𝑥 ∈ 𝑉 → (𝑥 ∈ (𝑉 ∖ {𝑁}) → (𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸))) |
21 | 15, 20 | impbid 201 |
. . . . . . . . . . . . . . . 16
⊢ (¬
𝑥 ∈ 𝑉 → ((𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ↔ 𝑥 ∈ (𝑉 ∖ {𝑁}))) |
22 | 21 | a1d 25 |
. . . . . . . . . . . . . . 15
⊢ (¬
𝑥 ∈ 𝑉 → ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → ((𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ↔ 𝑥 ∈ (𝑉 ∖ {𝑁})))) |
23 | | usgraedgrn 25910 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑉 USGrph 𝐸 ∧ {𝑁, 𝑥} ∈ ran 𝐸) → 𝑁 ≠ 𝑥) |
24 | | elsni 4142 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 ∈ {𝑁} → 𝑥 = 𝑁) |
25 | | eqcom 2617 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 = 𝑥 ↔ 𝑥 = 𝑁) |
26 | 24, 25 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 ∈ {𝑁} → 𝑁 = 𝑥) |
27 | 26 | necon3ai 2807 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ≠ 𝑥 → ¬ 𝑥 ∈ {𝑁}) |
28 | 23, 27 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑉 USGrph 𝐸 ∧ {𝑁, 𝑥} ∈ ran 𝐸) → ¬ 𝑥 ∈ {𝑁}) |
29 | 28 | ex 449 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑉 USGrph 𝐸 → ({𝑁, 𝑥} ∈ ran 𝐸 → ¬ 𝑥 ∈ {𝑁})) |
30 | 29 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((∀𝑘 ∈
(𝑉 ∖ {𝑥}){𝑘, 𝑥} ∈ ran 𝐸 ∧ (𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉)) → ({𝑁, 𝑥} ∈ ran 𝐸 → ¬ 𝑥 ∈ {𝑁})) |
31 | 30 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((∀𝑘 ∈
(𝑉 ∖ {𝑥}){𝑘, 𝑥} ∈ ran 𝐸 ∧ (𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉)) ∧ 𝑥 ∈ 𝑉) → ({𝑁, 𝑥} ∈ ran 𝐸 → ¬ 𝑥 ∈ {𝑁})) |
32 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((¬
𝑥 ∈ {𝑁} ∧ 𝑁 ∈ 𝑉) → 𝑁 ∈ 𝑉) |
33 | | elsng 4139 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑁 ∈ 𝑉 → (𝑁 ∈ {𝑥} ↔ 𝑁 = 𝑥)) |
34 | | velsn 4141 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑥 ∈ {𝑁} ↔ 𝑥 = 𝑁) |
35 | 25, 34 | sylbb2 227 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑁 = 𝑥 → 𝑥 ∈ {𝑁}) |
36 | 33, 35 | syl6bi 242 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑁 ∈ 𝑉 → (𝑁 ∈ {𝑥} → 𝑥 ∈ {𝑁})) |
37 | 36 | con3d 147 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑁 ∈ 𝑉 → (¬ 𝑥 ∈ {𝑁} → ¬ 𝑁 ∈ {𝑥})) |
38 | 37 | impcom 445 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((¬
𝑥 ∈ {𝑁} ∧ 𝑁 ∈ 𝑉) → ¬ 𝑁 ∈ {𝑥}) |
39 | 32, 38 | eldifd 3551 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((¬
𝑥 ∈ {𝑁} ∧ 𝑁 ∈ 𝑉) → 𝑁 ∈ (𝑉 ∖ {𝑥})) |
40 | | preq1 4212 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑘 = 𝑁 → {𝑘, 𝑥} = {𝑁, 𝑥}) |
41 | 40 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑘 = 𝑁 → ({𝑘, 𝑥} ∈ ran 𝐸 ↔ {𝑁, 𝑥} ∈ ran 𝐸)) |
42 | 41 | rspcva 3280 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑁 ∈ (𝑉 ∖ {𝑥}) ∧ ∀𝑘 ∈ (𝑉 ∖ {𝑥}){𝑘, 𝑥} ∈ ran 𝐸) → {𝑁, 𝑥} ∈ ran 𝐸) |
43 | 42 | 2a1d 26 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑁 ∈ (𝑉 ∖ {𝑥}) ∧ ∀𝑘 ∈ (𝑉 ∖ {𝑥}){𝑘, 𝑥} ∈ ran 𝐸) → (𝑥 ∈ 𝑉 → (𝑉 USGrph 𝐸 → {𝑁, 𝑥} ∈ ran 𝐸))) |
44 | 43 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈ (𝑉 ∖ {𝑥}) → (∀𝑘 ∈ (𝑉 ∖ {𝑥}){𝑘, 𝑥} ∈ ran 𝐸 → (𝑥 ∈ 𝑉 → (𝑉 USGrph 𝐸 → {𝑁, 𝑥} ∈ ran 𝐸)))) |
45 | 44 | com24 93 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ (𝑉 ∖ {𝑥}) → (𝑉 USGrph 𝐸 → (𝑥 ∈ 𝑉 → (∀𝑘 ∈ (𝑉 ∖ {𝑥}){𝑘, 𝑥} ∈ ran 𝐸 → {𝑁, 𝑥} ∈ ran 𝐸)))) |
46 | 39, 45 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((¬
𝑥 ∈ {𝑁} ∧ 𝑁 ∈ 𝑉) → (𝑉 USGrph 𝐸 → (𝑥 ∈ 𝑉 → (∀𝑘 ∈ (𝑉 ∖ {𝑥}){𝑘, 𝑥} ∈ ran 𝐸 → {𝑁, 𝑥} ∈ ran 𝐸)))) |
47 | 46 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (¬
𝑥 ∈ {𝑁} → (𝑁 ∈ 𝑉 → (𝑉 USGrph 𝐸 → (𝑥 ∈ 𝑉 → (∀𝑘 ∈ (𝑉 ∖ {𝑥}){𝑘, 𝑥} ∈ ran 𝐸 → {𝑁, 𝑥} ∈ ran 𝐸))))) |
48 | 47 | com13 86 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑉 USGrph 𝐸 → (𝑁 ∈ 𝑉 → (¬ 𝑥 ∈ {𝑁} → (𝑥 ∈ 𝑉 → (∀𝑘 ∈ (𝑉 ∖ {𝑥}){𝑘, 𝑥} ∈ ran 𝐸 → {𝑁, 𝑥} ∈ ran 𝐸))))) |
49 | 48 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → (¬ 𝑥 ∈ {𝑁} → (𝑥 ∈ 𝑉 → (∀𝑘 ∈ (𝑉 ∖ {𝑥}){𝑘, 𝑥} ∈ ran 𝐸 → {𝑁, 𝑥} ∈ ran 𝐸)))) |
50 | 49 | com12 32 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (¬
𝑥 ∈ {𝑁} → ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → (𝑥 ∈ 𝑉 → (∀𝑘 ∈ (𝑉 ∖ {𝑥}){𝑘, 𝑥} ∈ ran 𝐸 → {𝑁, 𝑥} ∈ ran 𝐸)))) |
51 | 50 | com14 94 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∀𝑘 ∈
(𝑉 ∖ {𝑥}){𝑘, 𝑥} ∈ ran 𝐸 → ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → (𝑥 ∈ 𝑉 → (¬ 𝑥 ∈ {𝑁} → {𝑁, 𝑥} ∈ ran 𝐸)))) |
52 | 51 | imp31 447 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((∀𝑘 ∈
(𝑉 ∖ {𝑥}){𝑘, 𝑥} ∈ ran 𝐸 ∧ (𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉)) ∧ 𝑥 ∈ 𝑉) → (¬ 𝑥 ∈ {𝑁} → {𝑁, 𝑥} ∈ ran 𝐸)) |
53 | 31, 52 | impbid 201 |
. . . . . . . . . . . . . . . . . 18
⊢
(((∀𝑘 ∈
(𝑉 ∖ {𝑥}){𝑘, 𝑥} ∈ ran 𝐸 ∧ (𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉)) ∧ 𝑥 ∈ 𝑉) → ({𝑁, 𝑥} ∈ ran 𝐸 ↔ ¬ 𝑥 ∈ {𝑁})) |
54 | 53 | pm5.32da 671 |
. . . . . . . . . . . . . . . . 17
⊢
((∀𝑘 ∈
(𝑉 ∖ {𝑥}){𝑘, 𝑥} ∈ ran 𝐸 ∧ (𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉)) → ((𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ↔ (𝑥 ∈ 𝑉 ∧ ¬ 𝑥 ∈ {𝑁}))) |
55 | 54, 16 | syl6bbr 277 |
. . . . . . . . . . . . . . . 16
⊢
((∀𝑘 ∈
(𝑉 ∖ {𝑥}){𝑘, 𝑥} ∈ ran 𝐸 ∧ (𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉)) → ((𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ↔ 𝑥 ∈ (𝑉 ∖ {𝑁}))) |
56 | 55 | ex 449 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑘 ∈
(𝑉 ∖ {𝑥}){𝑘, 𝑥} ∈ ran 𝐸 → ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → ((𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ↔ 𝑥 ∈ (𝑉 ∖ {𝑁})))) |
57 | 22, 56 | ja 172 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝑉 → ∀𝑘 ∈ (𝑉 ∖ {𝑥}){𝑘, 𝑥} ∈ ran 𝐸) → ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → ((𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ↔ 𝑥 ∈ (𝑉 ∖ {𝑁})))) |
58 | 57 | impcom 445 |
. . . . . . . . . . . . 13
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) ∧ (𝑥 ∈ 𝑉 → ∀𝑘 ∈ (𝑉 ∖ {𝑥}){𝑘, 𝑥} ∈ ran 𝐸)) → ((𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ↔ 𝑥 ∈ (𝑉 ∖ {𝑁}))) |
59 | 12, 58 | syl5bb 271 |
. . . . . . . . . . . 12
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) ∧ (𝑥 ∈ 𝑉 → ∀𝑘 ∈ (𝑉 ∖ {𝑥}){𝑘, 𝑥} ∈ ran 𝐸)) → (𝑥 ∈ {𝑛 ∈ 𝑉 ∣ {𝑁, 𝑛} ∈ ran 𝐸} ↔ 𝑥 ∈ (𝑉 ∖ {𝑁}))) |
60 | 59 | ex 449 |
. . . . . . . . . . 11
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → ((𝑥 ∈ 𝑉 → ∀𝑘 ∈ (𝑉 ∖ {𝑥}){𝑘, 𝑥} ∈ ran 𝐸) → (𝑥 ∈ {𝑛 ∈ 𝑉 ∣ {𝑁, 𝑛} ∈ ran 𝐸} ↔ 𝑥 ∈ (𝑉 ∖ {𝑁})))) |
61 | 60 | alimdv 1832 |
. . . . . . . . . 10
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → (∀𝑥(𝑥 ∈ 𝑉 → ∀𝑘 ∈ (𝑉 ∖ {𝑥}){𝑘, 𝑥} ∈ ran 𝐸) → ∀𝑥(𝑥 ∈ {𝑛 ∈ 𝑉 ∣ {𝑁, 𝑛} ∈ ran 𝐸} ↔ 𝑥 ∈ (𝑉 ∖ {𝑁})))) |
62 | 9, 61 | syl5bi 231 |
. . . . . . . . 9
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → (∀𝑥 ∈ 𝑉 ∀𝑘 ∈ (𝑉 ∖ {𝑥}){𝑘, 𝑥} ∈ ran 𝐸 → ∀𝑥(𝑥 ∈ {𝑛 ∈ 𝑉 ∣ {𝑁, 𝑛} ∈ ran 𝐸} ↔ 𝑥 ∈ (𝑉 ∖ {𝑁})))) |
63 | 62 | impancom 455 |
. . . . . . . 8
⊢ ((𝑉 USGrph 𝐸 ∧ ∀𝑥 ∈ 𝑉 ∀𝑘 ∈ (𝑉 ∖ {𝑥}){𝑘, 𝑥} ∈ ran 𝐸) → (𝑁 ∈ 𝑉 → ∀𝑥(𝑥 ∈ {𝑛 ∈ 𝑉 ∣ {𝑁, 𝑛} ∈ ran 𝐸} ↔ 𝑥 ∈ (𝑉 ∖ {𝑁})))) |
64 | 8, 63 | syl 17 |
. . . . . . 7
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ComplUSGrph 𝐸) → (𝑁 ∈ 𝑉 → ∀𝑥(𝑥 ∈ {𝑛 ∈ 𝑉 ∣ {𝑁, 𝑛} ∈ ran 𝐸} ↔ 𝑥 ∈ (𝑉 ∖ {𝑁})))) |
65 | 64 | imp 444 |
. . . . . 6
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ComplUSGrph 𝐸) ∧ 𝑁 ∈ 𝑉) → ∀𝑥(𝑥 ∈ {𝑛 ∈ 𝑉 ∣ {𝑁, 𝑛} ∈ ran 𝐸} ↔ 𝑥 ∈ (𝑉 ∖ {𝑁}))) |
66 | | dfcleq 2604 |
. . . . . 6
⊢ ({𝑛 ∈ 𝑉 ∣ {𝑁, 𝑛} ∈ ran 𝐸} = (𝑉 ∖ {𝑁}) ↔ ∀𝑥(𝑥 ∈ {𝑛 ∈ 𝑉 ∣ {𝑁, 𝑛} ∈ ran 𝐸} ↔ 𝑥 ∈ (𝑉 ∖ {𝑁}))) |
67 | 65, 66 | sylibr 223 |
. . . . 5
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ComplUSGrph 𝐸) ∧ 𝑁 ∈ 𝑉) → {𝑛 ∈ 𝑉 ∣ {𝑁, 𝑛} ∈ ran 𝐸} = (𝑉 ∖ {𝑁})) |
68 | 4, 67 | eqtrd 2644 |
. . . 4
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ComplUSGrph 𝐸) ∧ 𝑁 ∈ 𝑉) → (〈𝑉, 𝐸〉 Neighbors 𝑁) = (𝑉 ∖ {𝑁})) |
69 | 68 | ex 449 |
. . 3
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ComplUSGrph 𝐸) → (𝑁 ∈ 𝑉 → (〈𝑉, 𝐸〉 Neighbors 𝑁) = (𝑉 ∖ {𝑁}))) |
70 | 1, 69 | mpancom 700 |
. 2
⊢ (𝑉 ComplUSGrph 𝐸 → (𝑁 ∈ 𝑉 → (〈𝑉, 𝐸〉 Neighbors 𝑁) = (𝑉 ∖ {𝑁}))) |
71 | 70 | imp 444 |
1
⊢ ((𝑉 ComplUSGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → (〈𝑉, 𝐸〉 Neighbors 𝑁) = (𝑉 ∖ {𝑁})) |