Step | Hyp | Ref
| Expression |
1 | | nbusgra 25957 |
. . . 4
⊢ (𝑉 USGrph 𝐸 → (〈𝑉, 𝐸〉 Neighbors 𝑁) = {𝑛 ∈ 𝑉 ∣ {𝑁, 𝑛} ∈ ran 𝐸}) |
2 | 1 | adantr 480 |
. . 3
⊢ ((𝑉 USGrph 𝐸 ∧ ∀𝑥 ∈ ran 𝐸 𝑁 ∉ 𝑥) → (〈𝑉, 𝐸〉 Neighbors 𝑁) = {𝑛 ∈ 𝑉 ∣ {𝑁, 𝑛} ∈ ran 𝐸}) |
3 | | neleq2 2889 |
. . . . . . . . . 10
⊢ (𝑥 = {𝑁, 𝑛} → (𝑁 ∉ 𝑥 ↔ 𝑁 ∉ {𝑁, 𝑛})) |
4 | 3 | rspcv 3278 |
. . . . . . . . 9
⊢ ({𝑁, 𝑛} ∈ ran 𝐸 → (∀𝑥 ∈ ran 𝐸 𝑁 ∉ 𝑥 → 𝑁 ∉ {𝑁, 𝑛})) |
5 | | df-nel 2783 |
. . . . . . . . . 10
⊢ (𝑁 ∉ {𝑁, 𝑛} ↔ ¬ 𝑁 ∈ {𝑁, 𝑛}) |
6 | | elprg 4144 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ 𝑉 → (𝑁 ∈ {𝑁, 𝑛} ↔ (𝑁 = 𝑁 ∨ 𝑁 = 𝑛))) |
7 | 6 | notbid 307 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ 𝑉 → (¬ 𝑁 ∈ {𝑁, 𝑛} ↔ ¬ (𝑁 = 𝑁 ∨ 𝑁 = 𝑛))) |
8 | | ioran 510 |
. . . . . . . . . . . . 13
⊢ (¬
(𝑁 = 𝑁 ∨ 𝑁 = 𝑛) ↔ (¬ 𝑁 = 𝑁 ∧ ¬ 𝑁 = 𝑛)) |
9 | 7, 8 | syl6bb 275 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ 𝑉 → (¬ 𝑁 ∈ {𝑁, 𝑛} ↔ (¬ 𝑁 = 𝑁 ∧ ¬ 𝑁 = 𝑛))) |
10 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢ 𝑁 = 𝑁 |
11 | 10 | pm2.24i 145 |
. . . . . . . . . . . . 13
⊢ (¬
𝑁 = 𝑁 → (¬ 𝑁 = 𝑛 → (𝑉 USGrph 𝐸 → (𝑛 ∈ 𝑉 → ¬ {𝑁, 𝑛} ∈ ran 𝐸)))) |
12 | 11 | imp 444 |
. . . . . . . . . . . 12
⊢ ((¬
𝑁 = 𝑁 ∧ ¬ 𝑁 = 𝑛) → (𝑉 USGrph 𝐸 → (𝑛 ∈ 𝑉 → ¬ {𝑁, 𝑛} ∈ ran 𝐸))) |
13 | 9, 12 | syl6bi 242 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ 𝑉 → (¬ 𝑁 ∈ {𝑁, 𝑛} → (𝑉 USGrph 𝐸 → (𝑛 ∈ 𝑉 → ¬ {𝑁, 𝑛} ∈ ran 𝐸)))) |
14 | | usgraedgrnv 25906 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑉 USGrph 𝐸 ∧ {𝑁, 𝑛} ∈ ran 𝐸) → (𝑁 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉)) |
15 | 14 | simpld 474 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑉 USGrph 𝐸 ∧ {𝑁, 𝑛} ∈ ran 𝐸) → 𝑁 ∈ 𝑉) |
16 | 15 | ex 449 |
. . . . . . . . . . . . . . 15
⊢ (𝑉 USGrph 𝐸 → ({𝑁, 𝑛} ∈ ran 𝐸 → 𝑁 ∈ 𝑉)) |
17 | 16 | con3d 147 |
. . . . . . . . . . . . . 14
⊢ (𝑉 USGrph 𝐸 → (¬ 𝑁 ∈ 𝑉 → ¬ {𝑁, 𝑛} ∈ ran 𝐸)) |
18 | 17 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ 𝑉 → (𝑉 USGrph 𝐸 → (¬ 𝑁 ∈ 𝑉 → ¬ {𝑁, 𝑛} ∈ ran 𝐸))) |
19 | 18 | com13 86 |
. . . . . . . . . . . 12
⊢ (¬
𝑁 ∈ 𝑉 → (𝑉 USGrph 𝐸 → (𝑛 ∈ 𝑉 → ¬ {𝑁, 𝑛} ∈ ran 𝐸))) |
20 | 19 | a1d 25 |
. . . . . . . . . . 11
⊢ (¬
𝑁 ∈ 𝑉 → (¬ 𝑁 ∈ {𝑁, 𝑛} → (𝑉 USGrph 𝐸 → (𝑛 ∈ 𝑉 → ¬ {𝑁, 𝑛} ∈ ran 𝐸)))) |
21 | 13, 20 | pm2.61i 175 |
. . . . . . . . . 10
⊢ (¬
𝑁 ∈ {𝑁, 𝑛} → (𝑉 USGrph 𝐸 → (𝑛 ∈ 𝑉 → ¬ {𝑁, 𝑛} ∈ ran 𝐸))) |
22 | 5, 21 | sylbi 206 |
. . . . . . . . 9
⊢ (𝑁 ∉ {𝑁, 𝑛} → (𝑉 USGrph 𝐸 → (𝑛 ∈ 𝑉 → ¬ {𝑁, 𝑛} ∈ ran 𝐸))) |
23 | 4, 22 | syl6 34 |
. . . . . . . 8
⊢ ({𝑁, 𝑛} ∈ ran 𝐸 → (∀𝑥 ∈ ran 𝐸 𝑁 ∉ 𝑥 → (𝑉 USGrph 𝐸 → (𝑛 ∈ 𝑉 → ¬ {𝑁, 𝑛} ∈ ran 𝐸)))) |
24 | 23 | com13 86 |
. . . . . . 7
⊢ (𝑉 USGrph 𝐸 → (∀𝑥 ∈ ran 𝐸 𝑁 ∉ 𝑥 → ({𝑁, 𝑛} ∈ ran 𝐸 → (𝑛 ∈ 𝑉 → ¬ {𝑁, 𝑛} ∈ ran 𝐸)))) |
25 | 24 | imp 444 |
. . . . . 6
⊢ ((𝑉 USGrph 𝐸 ∧ ∀𝑥 ∈ ran 𝐸 𝑁 ∉ 𝑥) → ({𝑁, 𝑛} ∈ ran 𝐸 → (𝑛 ∈ 𝑉 → ¬ {𝑁, 𝑛} ∈ ran 𝐸))) |
26 | | ax-1 6 |
. . . . . 6
⊢ (¬
{𝑁, 𝑛} ∈ ran 𝐸 → (𝑛 ∈ 𝑉 → ¬ {𝑁, 𝑛} ∈ ran 𝐸)) |
27 | 25, 26 | pm2.61d1 170 |
. . . . 5
⊢ ((𝑉 USGrph 𝐸 ∧ ∀𝑥 ∈ ran 𝐸 𝑁 ∉ 𝑥) → (𝑛 ∈ 𝑉 → ¬ {𝑁, 𝑛} ∈ ran 𝐸)) |
28 | 27 | ralrimiv 2948 |
. . . 4
⊢ ((𝑉 USGrph 𝐸 ∧ ∀𝑥 ∈ ran 𝐸 𝑁 ∉ 𝑥) → ∀𝑛 ∈ 𝑉 ¬ {𝑁, 𝑛} ∈ ran 𝐸) |
29 | | rabeq0 3911 |
. . . 4
⊢ ({𝑛 ∈ 𝑉 ∣ {𝑁, 𝑛} ∈ ran 𝐸} = ∅ ↔ ∀𝑛 ∈ 𝑉 ¬ {𝑁, 𝑛} ∈ ran 𝐸) |
30 | 28, 29 | sylibr 223 |
. . 3
⊢ ((𝑉 USGrph 𝐸 ∧ ∀𝑥 ∈ ran 𝐸 𝑁 ∉ 𝑥) → {𝑛 ∈ 𝑉 ∣ {𝑁, 𝑛} ∈ ran 𝐸} = ∅) |
31 | 2, 30 | eqtrd 2644 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ ∀𝑥 ∈ ran 𝐸 𝑁 ∉ 𝑥) → (〈𝑉, 𝐸〉 Neighbors 𝑁) = ∅) |
32 | 31 | ex 449 |
1
⊢ (𝑉 USGrph 𝐸 → (∀𝑥 ∈ ran 𝐸 𝑁 ∉ 𝑥 → (〈𝑉, 𝐸〉 Neighbors 𝑁) = ∅)) |