Step | Hyp | Ref
| Expression |
1 | | nbcusgra 25992 |
. . . 4
⊢ ((𝑉 ComplUSGrph 𝐸 ∧ 𝑣 ∈ 𝑉) → (〈𝑉, 𝐸〉 Neighbors 𝑣) = (𝑉 ∖ {𝑣})) |
2 | 1 | ralrimiva 2949 |
. . 3
⊢ (𝑉 ComplUSGrph 𝐸 → ∀𝑣 ∈ 𝑉 (〈𝑉, 𝐸〉 Neighbors 𝑣) = (𝑉 ∖ {𝑣})) |
3 | | cusisusgra 25987 |
. . . . . . . 8
⊢ (𝑉 ComplUSGrph 𝐸 → 𝑉 USGrph 𝐸) |
4 | 3 | adantr 480 |
. . . . . . 7
⊢ ((𝑉 ComplUSGrph 𝐸 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) → 𝑉 USGrph 𝐸) |
5 | 4 | adantr 480 |
. . . . . 6
⊢ (((𝑉 ComplUSGrph 𝐸 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) ∧ ∀𝑣 ∈ 𝑉 (〈𝑉, 𝐸〉 Neighbors 𝑣) = (𝑉 ∖ {𝑣})) → 𝑉 USGrph 𝐸) |
6 | | hashnncl 13018 |
. . . . . . . . 9
⊢ (𝑉 ∈ Fin →
((#‘𝑉) ∈ ℕ
↔ 𝑉 ≠
∅)) |
7 | | nnm1nn0 11211 |
. . . . . . . . 9
⊢
((#‘𝑉) ∈
ℕ → ((#‘𝑉)
− 1) ∈ ℕ0) |
8 | 6, 7 | syl6bir 243 |
. . . . . . . 8
⊢ (𝑉 ∈ Fin → (𝑉 ≠ ∅ →
((#‘𝑉) − 1)
∈ ℕ0)) |
9 | 8 | imp 444 |
. . . . . . 7
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) →
((#‘𝑉) − 1)
∈ ℕ0) |
10 | 9 | ad2antlr 759 |
. . . . . 6
⊢ (((𝑉 ComplUSGrph 𝐸 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) ∧ ∀𝑣 ∈ 𝑉 (〈𝑉, 𝐸〉 Neighbors 𝑣) = (𝑉 ∖ {𝑣})) → ((#‘𝑉) − 1) ∈
ℕ0) |
11 | 4 | anim1i 590 |
. . . . . . . . . . . 12
⊢ (((𝑉 ComplUSGrph 𝐸 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) ∧ 𝑣 ∈ 𝑉) → (𝑉 USGrph 𝐸 ∧ 𝑣 ∈ 𝑉)) |
12 | 11 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝑉 ComplUSGrph 𝐸 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) ∧ 𝑣 ∈ 𝑉) ∧ (〈𝑉, 𝐸〉 Neighbors 𝑣) = (𝑉 ∖ {𝑣})) → (𝑉 USGrph 𝐸 ∧ 𝑣 ∈ 𝑉)) |
13 | | hashnbgravdg 26440 |
. . . . . . . . . . 11
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑣 ∈ 𝑉) → (#‘(〈𝑉, 𝐸〉 Neighbors 𝑣)) = ((𝑉 VDeg 𝐸)‘𝑣)) |
14 | 12, 13 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝑉 ComplUSGrph 𝐸 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) ∧ 𝑣 ∈ 𝑉) ∧ (〈𝑉, 𝐸〉 Neighbors 𝑣) = (𝑉 ∖ {𝑣})) → (#‘(〈𝑉, 𝐸〉 Neighbors 𝑣)) = ((𝑉 VDeg 𝐸)‘𝑣)) |
15 | | fveq2 6103 |
. . . . . . . . . . 11
⊢
((〈𝑉, 𝐸〉 Neighbors 𝑣) = (𝑉 ∖ {𝑣}) → (#‘(〈𝑉, 𝐸〉 Neighbors 𝑣)) = (#‘(𝑉 ∖ {𝑣}))) |
16 | | simprl 790 |
. . . . . . . . . . . 12
⊢ ((𝑉 ComplUSGrph 𝐸 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) → 𝑉 ∈ Fin) |
17 | | hashdifsn 13063 |
. . . . . . . . . . . 12
⊢ ((𝑉 ∈ Fin ∧ 𝑣 ∈ 𝑉) → (#‘(𝑉 ∖ {𝑣})) = ((#‘𝑉) − 1)) |
18 | 16, 17 | sylan 487 |
. . . . . . . . . . 11
⊢ (((𝑉 ComplUSGrph 𝐸 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) ∧ 𝑣 ∈ 𝑉) → (#‘(𝑉 ∖ {𝑣})) = ((#‘𝑉) − 1)) |
19 | 15, 18 | sylan9eqr 2666 |
. . . . . . . . . 10
⊢ ((((𝑉 ComplUSGrph 𝐸 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) ∧ 𝑣 ∈ 𝑉) ∧ (〈𝑉, 𝐸〉 Neighbors 𝑣) = (𝑉 ∖ {𝑣})) → (#‘(〈𝑉, 𝐸〉 Neighbors 𝑣)) = ((#‘𝑉) − 1)) |
20 | 14, 19 | eqtr3d 2646 |
. . . . . . . . 9
⊢ ((((𝑉 ComplUSGrph 𝐸 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) ∧ 𝑣 ∈ 𝑉) ∧ (〈𝑉, 𝐸〉 Neighbors 𝑣) = (𝑉 ∖ {𝑣})) → ((𝑉 VDeg 𝐸)‘𝑣) = ((#‘𝑉) − 1)) |
21 | 20 | ex 449 |
. . . . . . . 8
⊢ (((𝑉 ComplUSGrph 𝐸 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) ∧ 𝑣 ∈ 𝑉) → ((〈𝑉, 𝐸〉 Neighbors 𝑣) = (𝑉 ∖ {𝑣}) → ((𝑉 VDeg 𝐸)‘𝑣) = ((#‘𝑉) − 1))) |
22 | 21 | ralimdva 2945 |
. . . . . . 7
⊢ ((𝑉 ComplUSGrph 𝐸 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) → (∀𝑣 ∈ 𝑉 (〈𝑉, 𝐸〉 Neighbors 𝑣) = (𝑉 ∖ {𝑣}) → ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = ((#‘𝑉) − 1))) |
23 | 22 | imp 444 |
. . . . . 6
⊢ (((𝑉 ComplUSGrph 𝐸 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) ∧ ∀𝑣 ∈ 𝑉 (〈𝑉, 𝐸〉 Neighbors 𝑣) = (𝑉 ∖ {𝑣})) → ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = ((#‘𝑉) − 1)) |
24 | | usgrav 25867 |
. . . . . . . . . . 11
⊢ (𝑉 USGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
25 | 3, 24 | syl 17 |
. . . . . . . . . 10
⊢ (𝑉 ComplUSGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
26 | 25 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑉 ComplUSGrph 𝐸 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
27 | | ovex 6577 |
. . . . . . . . . 10
⊢
((#‘𝑉) −
1) ∈ V |
28 | 27 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑉 ComplUSGrph 𝐸 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) → ((#‘𝑉) − 1) ∈
V) |
29 | | df-3an 1033 |
. . . . . . . . 9
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ ((#‘𝑉) − 1) ∈ V) ↔
((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ ((#‘𝑉) − 1) ∈
V)) |
30 | 26, 28, 29 | sylanbrc 695 |
. . . . . . . 8
⊢ ((𝑉 ComplUSGrph 𝐸 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) → (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ ((#‘𝑉) − 1) ∈ V)) |
31 | 30 | adantr 480 |
. . . . . . 7
⊢ (((𝑉 ComplUSGrph 𝐸 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) ∧ ∀𝑣 ∈ 𝑉 (〈𝑉, 𝐸〉 Neighbors 𝑣) = (𝑉 ∖ {𝑣})) → (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ ((#‘𝑉) − 1) ∈ V)) |
32 | | isrusgra 26454 |
. . . . . . 7
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ ((#‘𝑉) − 1) ∈ V) →
(〈𝑉, 𝐸〉 RegUSGrph ((#‘𝑉) − 1) ↔ (𝑉 USGrph 𝐸 ∧ ((#‘𝑉) − 1) ∈ ℕ0
∧ ∀𝑣 ∈
𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = ((#‘𝑉) − 1)))) |
33 | 31, 32 | syl 17 |
. . . . . 6
⊢ (((𝑉 ComplUSGrph 𝐸 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) ∧ ∀𝑣 ∈ 𝑉 (〈𝑉, 𝐸〉 Neighbors 𝑣) = (𝑉 ∖ {𝑣})) → (〈𝑉, 𝐸〉 RegUSGrph ((#‘𝑉) − 1) ↔ (𝑉 USGrph 𝐸 ∧ ((#‘𝑉) − 1) ∈ ℕ0
∧ ∀𝑣 ∈
𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = ((#‘𝑉) − 1)))) |
34 | 5, 10, 23, 33 | mpbir3and 1238 |
. . . . 5
⊢ (((𝑉 ComplUSGrph 𝐸 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) ∧ ∀𝑣 ∈ 𝑉 (〈𝑉, 𝐸〉 Neighbors 𝑣) = (𝑉 ∖ {𝑣})) → 〈𝑉, 𝐸〉 RegUSGrph ((#‘𝑉) − 1)) |
35 | 34 | expcom 450 |
. . . 4
⊢
(∀𝑣 ∈
𝑉 (〈𝑉, 𝐸〉 Neighbors 𝑣) = (𝑉 ∖ {𝑣}) → ((𝑉 ComplUSGrph 𝐸 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) → 〈𝑉, 𝐸〉 RegUSGrph ((#‘𝑉) − 1))) |
36 | 35 | expd 451 |
. . 3
⊢
(∀𝑣 ∈
𝑉 (〈𝑉, 𝐸〉 Neighbors 𝑣) = (𝑉 ∖ {𝑣}) → (𝑉 ComplUSGrph 𝐸 → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → 〈𝑉, 𝐸〉 RegUSGrph ((#‘𝑉) − 1)))) |
37 | 2, 36 | mpcom 37 |
. 2
⊢ (𝑉 ComplUSGrph 𝐸 → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → 〈𝑉, 𝐸〉 RegUSGrph ((#‘𝑉) − 1))) |
38 | 37 | 3impib 1254 |
1
⊢ ((𝑉 ComplUSGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → 〈𝑉, 𝐸〉 RegUSGrph ((#‘𝑉) − 1)) |