Step | Hyp | Ref
| Expression |
1 | | av-frgrareggt1.v |
. . . 4
⊢ 𝑉 = (Vtx‘𝐺) |
2 | | eqid 2610 |
. . . 4
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
3 | 1, 2 | frgrregorufrg 41505 |
. . 3
⊢ (𝐺 ∈ FriendGraph →
∀𝑘 ∈
ℕ0 (∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑘 → (𝐺 RegUSGraph 𝑘 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺)))) |
4 | 3 | 3ad2ant1 1075 |
. 2
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 <
(#‘𝑉)) →
∀𝑘 ∈
ℕ0 (∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑘 → (𝐺 RegUSGraph 𝑘 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺)))) |
5 | 1 | av-frgraogt3nreg 41551 |
. 2
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 <
(#‘𝑉)) →
∀𝑘 ∈
ℕ0 ¬ 𝐺
RegUSGraph 𝑘) |
6 | | frgrusgr 41432 |
. . . . . . 7
⊢ (𝐺 ∈ FriendGraph → 𝐺 ∈ USGraph
) |
7 | 6 | anim1i 590 |
. . . . . 6
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) → (𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin)) |
8 | 1 | isfusgr 40537 |
. . . . . 6
⊢ (𝐺 ∈ FinUSGraph ↔ (𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin)) |
9 | 7, 8 | sylibr 223 |
. . . . 5
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) → 𝐺 ∈ FinUSGraph
) |
10 | 9 | 3adant3 1074 |
. . . 4
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 <
(#‘𝑉)) → 𝐺 ∈ FinUSGraph
) |
11 | | 0red 9920 |
. . . . . . . 8
⊢ ((𝑉 ∈ Fin ∧ 3 <
(#‘𝑉)) → 0
∈ ℝ) |
12 | | 3re 10971 |
. . . . . . . . 9
⊢ 3 ∈
ℝ |
13 | 12 | a1i 11 |
. . . . . . . 8
⊢ ((𝑉 ∈ Fin ∧ 3 <
(#‘𝑉)) → 3
∈ ℝ) |
14 | | hashcl 13009 |
. . . . . . . . . 10
⊢ (𝑉 ∈ Fin →
(#‘𝑉) ∈
ℕ0) |
15 | 14 | nn0red 11229 |
. . . . . . . . 9
⊢ (𝑉 ∈ Fin →
(#‘𝑉) ∈
ℝ) |
16 | 15 | adantr 480 |
. . . . . . . 8
⊢ ((𝑉 ∈ Fin ∧ 3 <
(#‘𝑉)) →
(#‘𝑉) ∈
ℝ) |
17 | | 3pos 10991 |
. . . . . . . . 9
⊢ 0 <
3 |
18 | 17 | a1i 11 |
. . . . . . . 8
⊢ ((𝑉 ∈ Fin ∧ 3 <
(#‘𝑉)) → 0 <
3) |
19 | | simpr 476 |
. . . . . . . 8
⊢ ((𝑉 ∈ Fin ∧ 3 <
(#‘𝑉)) → 3 <
(#‘𝑉)) |
20 | 11, 13, 16, 18, 19 | lttrd 10077 |
. . . . . . 7
⊢ ((𝑉 ∈ Fin ∧ 3 <
(#‘𝑉)) → 0 <
(#‘𝑉)) |
21 | 20 | gt0ne0d 10471 |
. . . . . 6
⊢ ((𝑉 ∈ Fin ∧ 3 <
(#‘𝑉)) →
(#‘𝑉) ≠
0) |
22 | | hasheq0 13015 |
. . . . . . . 8
⊢ (𝑉 ∈ Fin →
((#‘𝑉) = 0 ↔
𝑉 =
∅)) |
23 | 22 | adantr 480 |
. . . . . . 7
⊢ ((𝑉 ∈ Fin ∧ 3 <
(#‘𝑉)) →
((#‘𝑉) = 0 ↔
𝑉 =
∅)) |
24 | 23 | necon3bid 2826 |
. . . . . 6
⊢ ((𝑉 ∈ Fin ∧ 3 <
(#‘𝑉)) →
((#‘𝑉) ≠ 0 ↔
𝑉 ≠
∅)) |
25 | 21, 24 | mpbid 221 |
. . . . 5
⊢ ((𝑉 ∈ Fin ∧ 3 <
(#‘𝑉)) → 𝑉 ≠ ∅) |
26 | 25 | 3adant1 1072 |
. . . 4
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 <
(#‘𝑉)) → 𝑉 ≠ ∅) |
27 | 1 | fusgrn0degnn0 40714 |
. . . 4
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) →
∃𝑡 ∈ 𝑉 ∃𝑚 ∈ ℕ0
((VtxDeg‘𝐺)‘𝑡) = 𝑚) |
28 | 10, 26, 27 | syl2anc 691 |
. . 3
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 <
(#‘𝑉)) →
∃𝑡 ∈ 𝑉 ∃𝑚 ∈ ℕ0
((VtxDeg‘𝐺)‘𝑡) = 𝑚) |
29 | | r19.26 3046 |
. . . . . . . 8
⊢
(∀𝑘 ∈
ℕ0 ((∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑘 → (𝐺 RegUSGraph 𝑘 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) ∧ ¬ 𝐺 RegUSGraph 𝑘) ↔ (∀𝑘 ∈ ℕ0 (∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑘 → (𝐺 RegUSGraph 𝑘 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) ∧ ∀𝑘 ∈ ℕ0 ¬ 𝐺 RegUSGraph 𝑘)) |
30 | | simpllr 795 |
. . . . . . . . . 10
⊢ ((((𝑡 ∈ 𝑉 ∧ 𝑚 ∈ ℕ0) ∧
((VtxDeg‘𝐺)‘𝑡) = 𝑚) ∧ (𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉))) → 𝑚 ∈ ℕ0) |
31 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 = 𝑡 → ((VtxDeg‘𝐺)‘𝑢) = ((VtxDeg‘𝐺)‘𝑡)) |
32 | 31 | eqeq1d 2612 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 = 𝑡 → (((VtxDeg‘𝐺)‘𝑢) = 𝑚 ↔ ((VtxDeg‘𝐺)‘𝑡) = 𝑚)) |
33 | 32 | rspcev 3282 |
. . . . . . . . . . . . . 14
⊢ ((𝑡 ∈ 𝑉 ∧ ((VtxDeg‘𝐺)‘𝑡) = 𝑚) → ∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑚) |
34 | 33 | ad4ant13 1284 |
. . . . . . . . . . . . 13
⊢ ((((𝑡 ∈ 𝑉 ∧ 𝑚 ∈ ℕ0) ∧
((VtxDeg‘𝐺)‘𝑡) = 𝑚) ∧ (𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉))) → ∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑚) |
35 | | ornld 938 |
. . . . . . . . . . . . 13
⊢
(∃𝑢 ∈
𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑚 → (((∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑚 → (𝐺 RegUSGraph 𝑚 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) ∧ ¬ 𝐺 RegUSGraph 𝑚) → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) |
36 | 34, 35 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝑡 ∈ 𝑉 ∧ 𝑚 ∈ ℕ0) ∧
((VtxDeg‘𝐺)‘𝑡) = 𝑚) ∧ (𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉))) → (((∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑚 → (𝐺 RegUSGraph 𝑚 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) ∧ ¬ 𝐺 RegUSGraph 𝑚) → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) |
37 | 36 | adantr 480 |
. . . . . . . . . . 11
⊢
(((((𝑡 ∈ 𝑉 ∧ 𝑚 ∈ ℕ0) ∧
((VtxDeg‘𝐺)‘𝑡) = 𝑚) ∧ (𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉))) ∧ 𝑘 = 𝑚) → (((∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑚 → (𝐺 RegUSGraph 𝑚 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) ∧ ¬ 𝐺 RegUSGraph 𝑚) → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) |
38 | | eqeq2 2621 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑚 → (((VtxDeg‘𝐺)‘𝑢) = 𝑘 ↔ ((VtxDeg‘𝐺)‘𝑢) = 𝑚)) |
39 | 38 | rexbidv 3034 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑚 → (∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑘 ↔ ∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑚)) |
40 | | breq2 4587 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑚 → (𝐺 RegUSGraph 𝑘 ↔ 𝐺 RegUSGraph 𝑚)) |
41 | 40 | orbi1d 735 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑚 → ((𝐺 RegUSGraph 𝑘 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺)) ↔ (𝐺 RegUSGraph 𝑚 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺)))) |
42 | 39, 41 | imbi12d 333 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑚 → ((∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑘 → (𝐺 RegUSGraph 𝑘 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) ↔ (∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑚 → (𝐺 RegUSGraph 𝑚 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))))) |
43 | 40 | notbid 307 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑚 → (¬ 𝐺 RegUSGraph 𝑘 ↔ ¬ 𝐺 RegUSGraph 𝑚)) |
44 | 42, 43 | anbi12d 743 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑚 → (((∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑘 → (𝐺 RegUSGraph 𝑘 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) ∧ ¬ 𝐺 RegUSGraph 𝑘) ↔ ((∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑚 → (𝐺 RegUSGraph 𝑚 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) ∧ ¬ 𝐺 RegUSGraph 𝑚))) |
45 | 44 | imbi1d 330 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑚 → ((((∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑘 → (𝐺 RegUSGraph 𝑘 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) ∧ ¬ 𝐺 RegUSGraph 𝑘) → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺)) ↔ (((∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑚 → (𝐺 RegUSGraph 𝑚 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) ∧ ¬ 𝐺 RegUSGraph 𝑚) → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺)))) |
46 | 45 | adantl 481 |
. . . . . . . . . . 11
⊢
(((((𝑡 ∈ 𝑉 ∧ 𝑚 ∈ ℕ0) ∧
((VtxDeg‘𝐺)‘𝑡) = 𝑚) ∧ (𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉))) ∧ 𝑘 = 𝑚) → ((((∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑘 → (𝐺 RegUSGraph 𝑘 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) ∧ ¬ 𝐺 RegUSGraph 𝑘) → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺)) ↔ (((∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑚 → (𝐺 RegUSGraph 𝑚 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) ∧ ¬ 𝐺 RegUSGraph 𝑚) → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺)))) |
47 | 37, 46 | mpbird 246 |
. . . . . . . . . 10
⊢
(((((𝑡 ∈ 𝑉 ∧ 𝑚 ∈ ℕ0) ∧
((VtxDeg‘𝐺)‘𝑡) = 𝑚) ∧ (𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉))) ∧ 𝑘 = 𝑚) → (((∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑘 → (𝐺 RegUSGraph 𝑘 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) ∧ ¬ 𝐺 RegUSGraph 𝑘) → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) |
48 | 30, 47 | rspcimdv 3283 |
. . . . . . . . 9
⊢ ((((𝑡 ∈ 𝑉 ∧ 𝑚 ∈ ℕ0) ∧
((VtxDeg‘𝐺)‘𝑡) = 𝑚) ∧ (𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉))) → (∀𝑘 ∈ ℕ0
((∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑘 → (𝐺 RegUSGraph 𝑘 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) ∧ ¬ 𝐺 RegUSGraph 𝑘) → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) |
49 | 48 | com12 32 |
. . . . . . . 8
⊢
(∀𝑘 ∈
ℕ0 ((∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑘 → (𝐺 RegUSGraph 𝑘 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) ∧ ¬ 𝐺 RegUSGraph 𝑘) → ((((𝑡 ∈ 𝑉 ∧ 𝑚 ∈ ℕ0) ∧
((VtxDeg‘𝐺)‘𝑡) = 𝑚) ∧ (𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉))) → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) |
50 | 29, 49 | sylbir 224 |
. . . . . . 7
⊢
((∀𝑘 ∈
ℕ0 (∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑘 → (𝐺 RegUSGraph 𝑘 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) ∧ ∀𝑘 ∈ ℕ0 ¬ 𝐺 RegUSGraph 𝑘) → ((((𝑡 ∈ 𝑉 ∧ 𝑚 ∈ ℕ0) ∧
((VtxDeg‘𝐺)‘𝑡) = 𝑚) ∧ (𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉))) → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) |
51 | 50 | expcom 450 |
. . . . . 6
⊢
(∀𝑘 ∈
ℕ0 ¬ 𝐺
RegUSGraph 𝑘 →
(∀𝑘 ∈
ℕ0 (∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑘 → (𝐺 RegUSGraph 𝑘 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) → ((((𝑡 ∈ 𝑉 ∧ 𝑚 ∈ ℕ0) ∧
((VtxDeg‘𝐺)‘𝑡) = 𝑚) ∧ (𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉))) → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺)))) |
52 | 51 | com13 86 |
. . . . 5
⊢ ((((𝑡 ∈ 𝑉 ∧ 𝑚 ∈ ℕ0) ∧
((VtxDeg‘𝐺)‘𝑡) = 𝑚) ∧ (𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉))) → (∀𝑘 ∈ ℕ0
(∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑘 → (𝐺 RegUSGraph 𝑘 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) → (∀𝑘 ∈ ℕ0 ¬ 𝐺 RegUSGraph 𝑘 → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺)))) |
53 | 52 | exp31 628 |
. . . 4
⊢ ((𝑡 ∈ 𝑉 ∧ 𝑚 ∈ ℕ0) →
(((VtxDeg‘𝐺)‘𝑡) = 𝑚 → ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉)) → (∀𝑘 ∈ ℕ0
(∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑘 → (𝐺 RegUSGraph 𝑘 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) → (∀𝑘 ∈ ℕ0 ¬ 𝐺 RegUSGraph 𝑘 → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺)))))) |
54 | 53 | rexlimivv 3018 |
. . 3
⊢
(∃𝑡 ∈
𝑉 ∃𝑚 ∈ ℕ0
((VtxDeg‘𝐺)‘𝑡) = 𝑚 → ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉)) → (∀𝑘 ∈ ℕ0
(∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑘 → (𝐺 RegUSGraph 𝑘 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) → (∀𝑘 ∈ ℕ0 ¬ 𝐺 RegUSGraph 𝑘 → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))))) |
55 | 28, 54 | mpcom 37 |
. 2
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 <
(#‘𝑉)) →
(∀𝑘 ∈
ℕ0 (∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑘 → (𝐺 RegUSGraph 𝑘 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) → (∀𝑘 ∈ ℕ0 ¬ 𝐺 RegUSGraph 𝑘 → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺)))) |
56 | 4, 5, 55 | mp2d 47 |
1
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 <
(#‘𝑉)) →
∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺)) |