Step | Hyp | Ref
| Expression |
1 | | usgrav 25867 |
. . . 4
⊢ (𝑉 USGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
2 | | uvtxel 26017 |
. . . 4
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑁 ∈ (𝑉 UnivVertex 𝐸) ↔ (𝑁 ∈ 𝑉 ∧ ∀𝑣 ∈ (𝑉 ∖ {𝑁}){𝑣, 𝑁} ∈ ran 𝐸))) |
3 | 1, 2 | syl 17 |
. . 3
⊢ (𝑉 USGrph 𝐸 → (𝑁 ∈ (𝑉 UnivVertex 𝐸) ↔ (𝑁 ∈ 𝑉 ∧ ∀𝑣 ∈ (𝑉 ∖ {𝑁}){𝑣, 𝑁} ∈ ran 𝐸))) |
4 | | nbusgra 25957 |
. . . . . 6
⊢ (𝑉 USGrph 𝐸 → (〈𝑉, 𝐸〉 Neighbors 𝑁) = {𝑛 ∈ 𝑉 ∣ {𝑁, 𝑛} ∈ ran 𝐸}) |
5 | 4 | adantr 480 |
. . . . 5
⊢ ((𝑉 USGrph 𝐸 ∧ (𝑁 ∈ 𝑉 ∧ ∀𝑣 ∈ (𝑉 ∖ {𝑁}){𝑣, 𝑁} ∈ ran 𝐸)) → (〈𝑉, 𝐸〉 Neighbors 𝑁) = {𝑛 ∈ 𝑉 ∣ {𝑁, 𝑛} ∈ ran 𝐸}) |
6 | | preq2 4213 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑥 → {𝑁, 𝑛} = {𝑁, 𝑥}) |
7 | 6 | eleq1d 2672 |
. . . . . . . . 9
⊢ (𝑛 = 𝑥 → ({𝑁, 𝑛} ∈ ran 𝐸 ↔ {𝑁, 𝑥} ∈ ran 𝐸)) |
8 | 7 | elrab 3331 |
. . . . . . . 8
⊢ (𝑥 ∈ {𝑛 ∈ 𝑉 ∣ {𝑁, 𝑛} ∈ ran 𝐸} ↔ (𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸)) |
9 | | usgraedgrn 25910 |
. . . . . . . . . . . . . 14
⊢ ((𝑉 USGrph 𝐸 ∧ {𝑁, 𝑥} ∈ ran 𝐸) → 𝑁 ≠ 𝑥) |
10 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ≠ 𝑥 ∧ 𝑥 ∈ 𝑉) → 𝑥 ∈ 𝑉) |
11 | | elsni 4142 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ {𝑁} → 𝑥 = 𝑁) |
12 | 11 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ {𝑁} → 𝑁 = 𝑥) |
13 | 12 | necon3ai 2807 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ≠ 𝑥 → ¬ 𝑥 ∈ {𝑁}) |
14 | 13 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ≠ 𝑥 ∧ 𝑥 ∈ 𝑉) → ¬ 𝑥 ∈ {𝑁}) |
15 | 10, 14 | eldifd 3551 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ≠ 𝑥 ∧ 𝑥 ∈ 𝑉) → 𝑥 ∈ (𝑉 ∖ {𝑁})) |
16 | 15 | ex 449 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ≠ 𝑥 → (𝑥 ∈ 𝑉 → 𝑥 ∈ (𝑉 ∖ {𝑁}))) |
17 | 9, 16 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑉 USGrph 𝐸 ∧ {𝑁, 𝑥} ∈ ran 𝐸) → (𝑥 ∈ 𝑉 → 𝑥 ∈ (𝑉 ∖ {𝑁}))) |
18 | 17 | ex 449 |
. . . . . . . . . . . 12
⊢ (𝑉 USGrph 𝐸 → ({𝑁, 𝑥} ∈ ran 𝐸 → (𝑥 ∈ 𝑉 → 𝑥 ∈ (𝑉 ∖ {𝑁})))) |
19 | 18 | com13 86 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝑉 → ({𝑁, 𝑥} ∈ ran 𝐸 → (𝑉 USGrph 𝐸 → 𝑥 ∈ (𝑉 ∖ {𝑁})))) |
20 | 19 | imp 444 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) → (𝑉 USGrph 𝐸 → 𝑥 ∈ (𝑉 ∖ {𝑁}))) |
21 | 20 | com12 32 |
. . . . . . . . 9
⊢ (𝑉 USGrph 𝐸 → ((𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) → 𝑥 ∈ (𝑉 ∖ {𝑁}))) |
22 | 21 | adantr 480 |
. . . . . . . 8
⊢ ((𝑉 USGrph 𝐸 ∧ (𝑁 ∈ 𝑉 ∧ ∀𝑣 ∈ (𝑉 ∖ {𝑁}){𝑣, 𝑁} ∈ ran 𝐸)) → ((𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) → 𝑥 ∈ (𝑉 ∖ {𝑁}))) |
23 | 8, 22 | syl5bi 231 |
. . . . . . 7
⊢ ((𝑉 USGrph 𝐸 ∧ (𝑁 ∈ 𝑉 ∧ ∀𝑣 ∈ (𝑉 ∖ {𝑁}){𝑣, 𝑁} ∈ ran 𝐸)) → (𝑥 ∈ {𝑛 ∈ 𝑉 ∣ {𝑁, 𝑛} ∈ ran 𝐸} → 𝑥 ∈ (𝑉 ∖ {𝑁}))) |
24 | | eldifi 3694 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝑉 ∖ {𝑁}) → 𝑥 ∈ 𝑉) |
25 | 24 | adantl 481 |
. . . . . . . . 9
⊢ (((𝑉 USGrph 𝐸 ∧ (𝑁 ∈ 𝑉 ∧ ∀𝑣 ∈ (𝑉 ∖ {𝑁}){𝑣, 𝑁} ∈ ran 𝐸)) ∧ 𝑥 ∈ (𝑉 ∖ {𝑁})) → 𝑥 ∈ 𝑉) |
26 | | preq1 4212 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 = 𝑥 → {𝑣, 𝑁} = {𝑥, 𝑁}) |
27 | 26 | eleq1d 2672 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 = 𝑥 → ({𝑣, 𝑁} ∈ ran 𝐸 ↔ {𝑥, 𝑁} ∈ ran 𝐸)) |
28 | 27 | rspcva 3280 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (𝑉 ∖ {𝑁}) ∧ ∀𝑣 ∈ (𝑉 ∖ {𝑁}){𝑣, 𝑁} ∈ ran 𝐸) → {𝑥, 𝑁} ∈ ran 𝐸) |
29 | | prcom 4211 |
. . . . . . . . . . . . . . . . . 18
⊢ {𝑥, 𝑁} = {𝑁, 𝑥} |
30 | 29 | eleq1i 2679 |
. . . . . . . . . . . . . . . . 17
⊢ ({𝑥, 𝑁} ∈ ran 𝐸 ↔ {𝑁, 𝑥} ∈ ran 𝐸) |
31 | 30 | biimpi 205 |
. . . . . . . . . . . . . . . 16
⊢ ({𝑥, 𝑁} ∈ ran 𝐸 → {𝑁, 𝑥} ∈ ran 𝐸) |
32 | 31 | 2a1d 26 |
. . . . . . . . . . . . . . 15
⊢ ({𝑥, 𝑁} ∈ ran 𝐸 → (𝑉 USGrph 𝐸 → (𝑁 ∈ 𝑉 → {𝑁, 𝑥} ∈ ran 𝐸))) |
33 | 28, 32 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (𝑉 ∖ {𝑁}) ∧ ∀𝑣 ∈ (𝑉 ∖ {𝑁}){𝑣, 𝑁} ∈ ran 𝐸) → (𝑉 USGrph 𝐸 → (𝑁 ∈ 𝑉 → {𝑁, 𝑥} ∈ ran 𝐸))) |
34 | 33 | ex 449 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝑉 ∖ {𝑁}) → (∀𝑣 ∈ (𝑉 ∖ {𝑁}){𝑣, 𝑁} ∈ ran 𝐸 → (𝑉 USGrph 𝐸 → (𝑁 ∈ 𝑉 → {𝑁, 𝑥} ∈ ran 𝐸)))) |
35 | 34 | com14 94 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ 𝑉 → (∀𝑣 ∈ (𝑉 ∖ {𝑁}){𝑣, 𝑁} ∈ ran 𝐸 → (𝑉 USGrph 𝐸 → (𝑥 ∈ (𝑉 ∖ {𝑁}) → {𝑁, 𝑥} ∈ ran 𝐸)))) |
36 | 35 | imp 444 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ 𝑉 ∧ ∀𝑣 ∈ (𝑉 ∖ {𝑁}){𝑣, 𝑁} ∈ ran 𝐸) → (𝑉 USGrph 𝐸 → (𝑥 ∈ (𝑉 ∖ {𝑁}) → {𝑁, 𝑥} ∈ ran 𝐸))) |
37 | 36 | impcom 445 |
. . . . . . . . . 10
⊢ ((𝑉 USGrph 𝐸 ∧ (𝑁 ∈ 𝑉 ∧ ∀𝑣 ∈ (𝑉 ∖ {𝑁}){𝑣, 𝑁} ∈ ran 𝐸)) → (𝑥 ∈ (𝑉 ∖ {𝑁}) → {𝑁, 𝑥} ∈ ran 𝐸)) |
38 | 37 | imp 444 |
. . . . . . . . 9
⊢ (((𝑉 USGrph 𝐸 ∧ (𝑁 ∈ 𝑉 ∧ ∀𝑣 ∈ (𝑉 ∖ {𝑁}){𝑣, 𝑁} ∈ ran 𝐸)) ∧ 𝑥 ∈ (𝑉 ∖ {𝑁})) → {𝑁, 𝑥} ∈ ran 𝐸) |
39 | 25, 38, 8 | sylanbrc 695 |
. . . . . . . 8
⊢ (((𝑉 USGrph 𝐸 ∧ (𝑁 ∈ 𝑉 ∧ ∀𝑣 ∈ (𝑉 ∖ {𝑁}){𝑣, 𝑁} ∈ ran 𝐸)) ∧ 𝑥 ∈ (𝑉 ∖ {𝑁})) → 𝑥 ∈ {𝑛 ∈ 𝑉 ∣ {𝑁, 𝑛} ∈ ran 𝐸}) |
40 | 39 | ex 449 |
. . . . . . 7
⊢ ((𝑉 USGrph 𝐸 ∧ (𝑁 ∈ 𝑉 ∧ ∀𝑣 ∈ (𝑉 ∖ {𝑁}){𝑣, 𝑁} ∈ ran 𝐸)) → (𝑥 ∈ (𝑉 ∖ {𝑁}) → 𝑥 ∈ {𝑛 ∈ 𝑉 ∣ {𝑁, 𝑛} ∈ ran 𝐸})) |
41 | 23, 40 | impbid 201 |
. . . . . 6
⊢ ((𝑉 USGrph 𝐸 ∧ (𝑁 ∈ 𝑉 ∧ ∀𝑣 ∈ (𝑉 ∖ {𝑁}){𝑣, 𝑁} ∈ ran 𝐸)) → (𝑥 ∈ {𝑛 ∈ 𝑉 ∣ {𝑁, 𝑛} ∈ ran 𝐸} ↔ 𝑥 ∈ (𝑉 ∖ {𝑁}))) |
42 | 41 | eqrdv 2608 |
. . . . 5
⊢ ((𝑉 USGrph 𝐸 ∧ (𝑁 ∈ 𝑉 ∧ ∀𝑣 ∈ (𝑉 ∖ {𝑁}){𝑣, 𝑁} ∈ ran 𝐸)) → {𝑛 ∈ 𝑉 ∣ {𝑁, 𝑛} ∈ ran 𝐸} = (𝑉 ∖ {𝑁})) |
43 | 5, 42 | eqtrd 2644 |
. . . 4
⊢ ((𝑉 USGrph 𝐸 ∧ (𝑁 ∈ 𝑉 ∧ ∀𝑣 ∈ (𝑉 ∖ {𝑁}){𝑣, 𝑁} ∈ ran 𝐸)) → (〈𝑉, 𝐸〉 Neighbors 𝑁) = (𝑉 ∖ {𝑁})) |
44 | 43 | ex 449 |
. . 3
⊢ (𝑉 USGrph 𝐸 → ((𝑁 ∈ 𝑉 ∧ ∀𝑣 ∈ (𝑉 ∖ {𝑁}){𝑣, 𝑁} ∈ ran 𝐸) → (〈𝑉, 𝐸〉 Neighbors 𝑁) = (𝑉 ∖ {𝑁}))) |
45 | 3, 44 | sylbid 229 |
. 2
⊢ (𝑉 USGrph 𝐸 → (𝑁 ∈ (𝑉 UnivVertex 𝐸) → (〈𝑉, 𝐸〉 Neighbors 𝑁) = (𝑉 ∖ {𝑁}))) |
46 | 45 | imp 444 |
1
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ (𝑉 UnivVertex 𝐸)) → (〈𝑉, 𝐸〉 Neighbors 𝑁) = (𝑉 ∖ {𝑁})) |