Proof of Theorem nbhashuvtx1
Step | Hyp | Ref
| Expression |
1 | | ax-1 6 |
. . 3
⊢ (𝑀 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑁) → ((𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑁) → 𝑀 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑁))) |
2 | 1 | 2a1d 26 |
. 2
⊢ (𝑀 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑁) → ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → ((#‘(〈𝑉, 𝐸〉 Neighbors 𝑁)) = ((#‘𝑉) − 1) → ((𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑁) → 𝑀 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑁))))) |
3 | | df-nel 2783 |
. . 3
⊢ (𝑀 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑁) ↔ ¬ 𝑀 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑁)) |
4 | | nbgrassvwo2 25967 |
. . . . . . 7
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑀 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑁)) → (〈𝑉, 𝐸〉 Neighbors 𝑁) ⊆ (𝑉 ∖ {𝑀, 𝑁})) |
5 | 4 | ex 449 |
. . . . . 6
⊢ (𝑉 USGrph 𝐸 → (𝑀 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑁) → (〈𝑉, 𝐸〉 Neighbors 𝑁) ⊆ (𝑉 ∖ {𝑀, 𝑁}))) |
6 | 5 | 3ad2ant1 1075 |
. . . . 5
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (𝑀 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑁) → (〈𝑉, 𝐸〉 Neighbors 𝑁) ⊆ (𝑉 ∖ {𝑀, 𝑁}))) |
7 | | difexg 4735 |
. . . . . . 7
⊢ (𝑉 ∈ Fin → (𝑉 ∖ {𝑀, 𝑁}) ∈ V) |
8 | 7 | 3ad2ant2 1076 |
. . . . . 6
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (𝑉 ∖ {𝑀, 𝑁}) ∈ V) |
9 | | hashss 13058 |
. . . . . . 7
⊢ (((𝑉 ∖ {𝑀, 𝑁}) ∈ V ∧ (〈𝑉, 𝐸〉 Neighbors 𝑁) ⊆ (𝑉 ∖ {𝑀, 𝑁})) → (#‘(〈𝑉, 𝐸〉 Neighbors 𝑁)) ≤ (#‘(𝑉 ∖ {𝑀, 𝑁}))) |
10 | 9 | ex 449 |
. . . . . 6
⊢ ((𝑉 ∖ {𝑀, 𝑁}) ∈ V → ((〈𝑉, 𝐸〉 Neighbors 𝑁) ⊆ (𝑉 ∖ {𝑀, 𝑁}) → (#‘(〈𝑉, 𝐸〉 Neighbors 𝑁)) ≤ (#‘(𝑉 ∖ {𝑀, 𝑁})))) |
11 | 8, 10 | syl 17 |
. . . . 5
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → ((〈𝑉, 𝐸〉 Neighbors 𝑁) ⊆ (𝑉 ∖ {𝑀, 𝑁}) → (#‘(〈𝑉, 𝐸〉 Neighbors 𝑁)) ≤ (#‘(𝑉 ∖ {𝑀, 𝑁})))) |
12 | | simpl2 1058 |
. . . . . . . . . . . 12
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑁)) → 𝑉 ∈ Fin) |
13 | | simpl 472 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑁) → 𝑀 ∈ 𝑉) |
14 | | simp3 1056 |
. . . . . . . . . . . . 13
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → 𝑁 ∈ 𝑉) |
15 | | prssi 4293 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) → {𝑀, 𝑁} ⊆ 𝑉) |
16 | 13, 14, 15 | syl2anr 494 |
. . . . . . . . . . . 12
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑁)) → {𝑀, 𝑁} ⊆ 𝑉) |
17 | | hashssdif 13061 |
. . . . . . . . . . . 12
⊢ ((𝑉 ∈ Fin ∧ {𝑀, 𝑁} ⊆ 𝑉) → (#‘(𝑉 ∖ {𝑀, 𝑁})) = ((#‘𝑉) − (#‘{𝑀, 𝑁}))) |
18 | 12, 16, 17 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑁)) → (#‘(𝑉 ∖ {𝑀, 𝑁})) = ((#‘𝑉) − (#‘{𝑀, 𝑁}))) |
19 | | simprr 792 |
. . . . . . . . . . . . 13
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑁)) → 𝑀 ≠ 𝑁) |
20 | | hashprgOLD 13044 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) → (𝑀 ≠ 𝑁 ↔ (#‘{𝑀, 𝑁}) = 2)) |
21 | 13, 14, 20 | syl2anr 494 |
. . . . . . . . . . . . 13
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑁)) → (𝑀 ≠ 𝑁 ↔ (#‘{𝑀, 𝑁}) = 2)) |
22 | 19, 21 | mpbid 221 |
. . . . . . . . . . . 12
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑁)) → (#‘{𝑀, 𝑁}) = 2) |
23 | 22 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑁)) → ((#‘𝑉) − (#‘{𝑀, 𝑁})) = ((#‘𝑉) − 2)) |
24 | 18, 23 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑁)) → (#‘(𝑉 ∖ {𝑀, 𝑁})) = ((#‘𝑉) − 2)) |
25 | 24 | breq2d 4595 |
. . . . . . . . 9
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑁)) → ((#‘(〈𝑉, 𝐸〉 Neighbors 𝑁)) ≤ (#‘(𝑉 ∖ {𝑀, 𝑁})) ↔ (#‘(〈𝑉, 𝐸〉 Neighbors 𝑁)) ≤ ((#‘𝑉) − 2))) |
26 | | nbhashnn0 26441 |
. . . . . . . . . . . . . 14
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (#‘(〈𝑉, 𝐸〉 Neighbors 𝑁)) ∈
ℕ0) |
27 | 26 | nn0zd 11356 |
. . . . . . . . . . . . 13
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (#‘(〈𝑉, 𝐸〉 Neighbors 𝑁)) ∈ ℤ) |
28 | | hashcl 13009 |
. . . . . . . . . . . . . . 15
⊢ (𝑉 ∈ Fin →
(#‘𝑉) ∈
ℕ0) |
29 | | nn0z 11277 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑉) ∈
ℕ0 → (#‘𝑉) ∈ ℤ) |
30 | | peano2zm 11297 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑉) ∈
ℤ → ((#‘𝑉)
− 1) ∈ ℤ) |
31 | 28, 29, 30 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (𝑉 ∈ Fin →
((#‘𝑉) − 1)
∈ ℤ) |
32 | 31 | 3ad2ant2 1076 |
. . . . . . . . . . . . 13
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → ((#‘𝑉) − 1) ∈
ℤ) |
33 | | zltlem1 11307 |
. . . . . . . . . . . . 13
⊢
(((#‘(〈𝑉,
𝐸〉 Neighbors 𝑁)) ∈ ℤ ∧
((#‘𝑉) − 1)
∈ ℤ) → ((#‘(〈𝑉, 𝐸〉 Neighbors 𝑁)) < ((#‘𝑉) − 1) ↔ (#‘(〈𝑉, 𝐸〉 Neighbors 𝑁)) ≤ (((#‘𝑉) − 1) − 1))) |
34 | 27, 32, 33 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → ((#‘(〈𝑉, 𝐸〉 Neighbors 𝑁)) < ((#‘𝑉) − 1) ↔ (#‘(〈𝑉, 𝐸〉 Neighbors 𝑁)) ≤ (((#‘𝑉) − 1) − 1))) |
35 | 28 | nn0cnd 11230 |
. . . . . . . . . . . . . . . 16
⊢ (𝑉 ∈ Fin →
(#‘𝑉) ∈
ℂ) |
36 | 35 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . 15
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (#‘𝑉) ∈ ℂ) |
37 | | 1cnd 9935 |
. . . . . . . . . . . . . . 15
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → 1 ∈ ℂ) |
38 | 36, 37, 37 | subsub4d 10302 |
. . . . . . . . . . . . . 14
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (((#‘𝑉) − 1) − 1) = ((#‘𝑉) − (1 +
1))) |
39 | | 1p1e2 11011 |
. . . . . . . . . . . . . . 15
⊢ (1 + 1) =
2 |
40 | 39 | oveq2i 6560 |
. . . . . . . . . . . . . 14
⊢
((#‘𝑉) −
(1 + 1)) = ((#‘𝑉)
− 2) |
41 | 38, 40 | syl6eq 2660 |
. . . . . . . . . . . . 13
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (((#‘𝑉) − 1) − 1) = ((#‘𝑉) − 2)) |
42 | 41 | breq2d 4595 |
. . . . . . . . . . . 12
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → ((#‘(〈𝑉, 𝐸〉 Neighbors 𝑁)) ≤ (((#‘𝑉) − 1) − 1) ↔
(#‘(〈𝑉, 𝐸〉 Neighbors 𝑁)) ≤ ((#‘𝑉) − 2))) |
43 | 34, 42 | bitrd 267 |
. . . . . . . . . . 11
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → ((#‘(〈𝑉, 𝐸〉 Neighbors 𝑁)) < ((#‘𝑉) − 1) ↔ (#‘(〈𝑉, 𝐸〉 Neighbors 𝑁)) ≤ ((#‘𝑉) − 2))) |
44 | 43 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑁)) → ((#‘(〈𝑉, 𝐸〉 Neighbors 𝑁)) < ((#‘𝑉) − 1) ↔ (#‘(〈𝑉, 𝐸〉 Neighbors 𝑁)) ≤ ((#‘𝑉) − 2))) |
45 | 26 | nn0red 11229 |
. . . . . . . . . . . . . . 15
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (#‘(〈𝑉, 𝐸〉 Neighbors 𝑁)) ∈ ℝ) |
46 | 45 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑁)) → (#‘(〈𝑉, 𝐸〉 Neighbors 𝑁)) ∈ ℝ) |
47 | 46 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑁)) ∧ (#‘(〈𝑉, 𝐸〉 Neighbors 𝑁)) < ((#‘𝑉) − 1)) → (#‘(〈𝑉, 𝐸〉 Neighbors 𝑁)) ∈ ℝ) |
48 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑁)) ∧ (#‘(〈𝑉, 𝐸〉 Neighbors 𝑁)) < ((#‘𝑉) − 1)) → (#‘(〈𝑉, 𝐸〉 Neighbors 𝑁)) < ((#‘𝑉) − 1)) |
49 | 47, 48 | ltned 10052 |
. . . . . . . . . . . 12
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑁)) ∧ (#‘(〈𝑉, 𝐸〉 Neighbors 𝑁)) < ((#‘𝑉) − 1)) → (#‘(〈𝑉, 𝐸〉 Neighbors 𝑁)) ≠ ((#‘𝑉) − 1)) |
50 | 49 | ex 449 |
. . . . . . . . . . 11
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑁)) → ((#‘(〈𝑉, 𝐸〉 Neighbors 𝑁)) < ((#‘𝑉) − 1) → (#‘(〈𝑉, 𝐸〉 Neighbors 𝑁)) ≠ ((#‘𝑉) − 1))) |
51 | | eqneqall 2793 |
. . . . . . . . . . . 12
⊢
((#‘(〈𝑉,
𝐸〉 Neighbors 𝑁)) = ((#‘𝑉) − 1) → ((#‘(〈𝑉, 𝐸〉 Neighbors 𝑁)) ≠ ((#‘𝑉) − 1) → 𝑀 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑁))) |
52 | 51 | com12 32 |
. . . . . . . . . . 11
⊢
((#‘(〈𝑉,
𝐸〉 Neighbors 𝑁)) ≠ ((#‘𝑉) − 1) →
((#‘(〈𝑉, 𝐸〉 Neighbors 𝑁)) = ((#‘𝑉) − 1) → 𝑀 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑁))) |
53 | 50, 52 | syl6 34 |
. . . . . . . . . 10
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑁)) → ((#‘(〈𝑉, 𝐸〉 Neighbors 𝑁)) < ((#‘𝑉) − 1) → ((#‘(〈𝑉, 𝐸〉 Neighbors 𝑁)) = ((#‘𝑉) − 1) → 𝑀 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑁)))) |
54 | 44, 53 | sylbird 249 |
. . . . . . . . 9
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑁)) → ((#‘(〈𝑉, 𝐸〉 Neighbors 𝑁)) ≤ ((#‘𝑉) − 2) → ((#‘(〈𝑉, 𝐸〉 Neighbors 𝑁)) = ((#‘𝑉) − 1) → 𝑀 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑁)))) |
55 | 25, 54 | sylbid 229 |
. . . . . . . 8
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑁)) → ((#‘(〈𝑉, 𝐸〉 Neighbors 𝑁)) ≤ (#‘(𝑉 ∖ {𝑀, 𝑁})) → ((#‘(〈𝑉, 𝐸〉 Neighbors 𝑁)) = ((#‘𝑉) − 1) → 𝑀 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑁)))) |
56 | 55 | ex 449 |
. . . . . . 7
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → ((𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑁) → ((#‘(〈𝑉, 𝐸〉 Neighbors 𝑁)) ≤ (#‘(𝑉 ∖ {𝑀, 𝑁})) → ((#‘(〈𝑉, 𝐸〉 Neighbors 𝑁)) = ((#‘𝑉) − 1) → 𝑀 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑁))))) |
57 | 56 | com23 84 |
. . . . . 6
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → ((#‘(〈𝑉, 𝐸〉 Neighbors 𝑁)) ≤ (#‘(𝑉 ∖ {𝑀, 𝑁})) → ((𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑁) → ((#‘(〈𝑉, 𝐸〉 Neighbors 𝑁)) = ((#‘𝑉) − 1) → 𝑀 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑁))))) |
58 | 57 | com34 89 |
. . . . 5
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → ((#‘(〈𝑉, 𝐸〉 Neighbors 𝑁)) ≤ (#‘(𝑉 ∖ {𝑀, 𝑁})) → ((#‘(〈𝑉, 𝐸〉 Neighbors 𝑁)) = ((#‘𝑉) − 1) → ((𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑁) → 𝑀 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑁))))) |
59 | 6, 11, 58 | 3syld 58 |
. . . 4
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (𝑀 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑁) → ((#‘(〈𝑉, 𝐸〉 Neighbors 𝑁)) = ((#‘𝑉) − 1) → ((𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑁) → 𝑀 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑁))))) |
60 | 59 | com12 32 |
. . 3
⊢ (𝑀 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑁) → ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → ((#‘(〈𝑉, 𝐸〉 Neighbors 𝑁)) = ((#‘𝑉) − 1) → ((𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑁) → 𝑀 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑁))))) |
61 | 3, 60 | sylbir 224 |
. 2
⊢ (¬
𝑀 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑁) → ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → ((#‘(〈𝑉, 𝐸〉 Neighbors 𝑁)) = ((#‘𝑉) − 1) → ((𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑁) → 𝑀 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑁))))) |
62 | 2, 61 | pm2.61i 175 |
1
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → ((#‘(〈𝑉, 𝐸〉 Neighbors 𝑁)) = ((#‘𝑉) − 1) → ((𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑁) → 𝑀 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑁)))) |