Step | Hyp | Ref
| Expression |
1 | | frgrreggt1.v |
. . . 4
⊢ 𝑉 = (Vtx‘𝐺) |
2 | | eqid 2622 |
. . . 4
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
3 | 1, 2 | frgrregorufrg 27190 |
. . 3
⊢ (𝐺 ∈ FriendGraph →
∀𝑘 ∈
ℕ0 (∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑘 → (𝐺 RegUSGraph 𝑘 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺)))) |
4 | 3 | 3ad2ant1 1082 |
. 2
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 <
(#‘𝑉)) →
∀𝑘 ∈
ℕ0 (∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑘 → (𝐺 RegUSGraph 𝑘 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺)))) |
5 | 1 | frgrogt3nreg 27255 |
. 2
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 <
(#‘𝑉)) →
∀𝑘 ∈
ℕ0 ¬ 𝐺
RegUSGraph 𝑘) |
6 | | frgrusgr 27124 |
. . . . . . 7
⊢ (𝐺 ∈ FriendGraph → 𝐺 ∈ USGraph
) |
7 | 6 | anim1i 592 |
. . . . . 6
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) → (𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin)) |
8 | 1 | isfusgr 26210 |
. . . . . 6
⊢ (𝐺 ∈ FinUSGraph ↔ (𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin)) |
9 | 7, 8 | sylibr 224 |
. . . . 5
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) → 𝐺 ∈ FinUSGraph
) |
10 | 9 | 3adant3 1081 |
. . . 4
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 <
(#‘𝑉)) → 𝐺 ∈ FinUSGraph
) |
11 | | 0red 10041 |
. . . . . . . 8
⊢ ((𝑉 ∈ Fin ∧ 3 <
(#‘𝑉)) → 0
∈ ℝ) |
12 | | 3re 11094 |
. . . . . . . . 9
⊢ 3 ∈
ℝ |
13 | 12 | a1i 11 |
. . . . . . . 8
⊢ ((𝑉 ∈ Fin ∧ 3 <
(#‘𝑉)) → 3
∈ ℝ) |
14 | | hashcl 13147 |
. . . . . . . . . 10
⊢ (𝑉 ∈ Fin →
(#‘𝑉) ∈
ℕ0) |
15 | 14 | nn0red 11352 |
. . . . . . . . 9
⊢ (𝑉 ∈ Fin →
(#‘𝑉) ∈
ℝ) |
16 | 15 | adantr 481 |
. . . . . . . 8
⊢ ((𝑉 ∈ Fin ∧ 3 <
(#‘𝑉)) →
(#‘𝑉) ∈
ℝ) |
17 | | 3pos 11114 |
. . . . . . . . 9
⊢ 0 <
3 |
18 | 17 | a1i 11 |
. . . . . . . 8
⊢ ((𝑉 ∈ Fin ∧ 3 <
(#‘𝑉)) → 0 <
3) |
19 | | simpr 477 |
. . . . . . . 8
⊢ ((𝑉 ∈ Fin ∧ 3 <
(#‘𝑉)) → 3 <
(#‘𝑉)) |
20 | 11, 13, 16, 18, 19 | lttrd 10198 |
. . . . . . 7
⊢ ((𝑉 ∈ Fin ∧ 3 <
(#‘𝑉)) → 0 <
(#‘𝑉)) |
21 | 20 | gt0ne0d 10592 |
. . . . . 6
⊢ ((𝑉 ∈ Fin ∧ 3 <
(#‘𝑉)) →
(#‘𝑉) ≠
0) |
22 | | hasheq0 13154 |
. . . . . . . 8
⊢ (𝑉 ∈ Fin →
((#‘𝑉) = 0 ↔
𝑉 =
∅)) |
23 | 22 | adantr 481 |
. . . . . . 7
⊢ ((𝑉 ∈ Fin ∧ 3 <
(#‘𝑉)) →
((#‘𝑉) = 0 ↔
𝑉 =
∅)) |
24 | 23 | necon3bid 2838 |
. . . . . 6
⊢ ((𝑉 ∈ Fin ∧ 3 <
(#‘𝑉)) →
((#‘𝑉) ≠ 0 ↔
𝑉 ≠
∅)) |
25 | 21, 24 | mpbid 222 |
. . . . 5
⊢ ((𝑉 ∈ Fin ∧ 3 <
(#‘𝑉)) → 𝑉 ≠ ∅) |
26 | 25 | 3adant1 1079 |
. . . 4
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 <
(#‘𝑉)) → 𝑉 ≠ ∅) |
27 | 1 | fusgrn0degnn0 26395 |
. . . 4
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) →
∃𝑡 ∈ 𝑉 ∃𝑚 ∈ ℕ0
((VtxDeg‘𝐺)‘𝑡) = 𝑚) |
28 | 10, 26, 27 | syl2anc 693 |
. . 3
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 <
(#‘𝑉)) →
∃𝑡 ∈ 𝑉 ∃𝑚 ∈ ℕ0
((VtxDeg‘𝐺)‘𝑡) = 𝑚) |
29 | | r19.26 3064 |
. . . . . . . 8
⊢
(∀𝑘 ∈
ℕ0 ((∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑘 → (𝐺 RegUSGraph 𝑘 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) ∧ ¬ 𝐺 RegUSGraph 𝑘) ↔ (∀𝑘 ∈ ℕ0 (∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑘 → (𝐺 RegUSGraph 𝑘 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) ∧ ∀𝑘 ∈ ℕ0 ¬ 𝐺 RegUSGraph 𝑘)) |
30 | | simpllr 799 |
. . . . . . . . . 10
⊢ ((((𝑡 ∈ 𝑉 ∧ 𝑚 ∈ ℕ0) ∧
((VtxDeg‘𝐺)‘𝑡) = 𝑚) ∧ (𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉))) → 𝑚 ∈ ℕ0) |
31 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 = 𝑡 → ((VtxDeg‘𝐺)‘𝑢) = ((VtxDeg‘𝐺)‘𝑡)) |
32 | 31 | eqeq1d 2624 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 = 𝑡 → (((VtxDeg‘𝐺)‘𝑢) = 𝑚 ↔ ((VtxDeg‘𝐺)‘𝑡) = 𝑚)) |
33 | 32 | rspcev 3309 |
. . . . . . . . . . . . . 14
⊢ ((𝑡 ∈ 𝑉 ∧ ((VtxDeg‘𝐺)‘𝑡) = 𝑚) → ∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑚) |
34 | 33 | ad4ant13 1292 |
. . . . . . . . . . . . 13
⊢ ((((𝑡 ∈ 𝑉 ∧ 𝑚 ∈ ℕ0) ∧
((VtxDeg‘𝐺)‘𝑡) = 𝑚) ∧ (𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉))) → ∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑚) |
35 | | ornld 940 |
. . . . . . . . . . . . 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 481 |
. . . . . . . . . . 11
⊢
(((((𝑡 ∈ 𝑉 ∧ 𝑚 ∈ ℕ0) ∧
((VtxDeg‘𝐺)‘𝑡) = 𝑚) ∧ (𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉))) ∧ 𝑘 = 𝑚) → (((∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑚 → (𝐺 RegUSGraph 𝑚 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) ∧ ¬ 𝐺 RegUSGraph 𝑚) → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) |
38 | | eqeq2 2633 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑚 → (((VtxDeg‘𝐺)‘𝑢) = 𝑘 ↔ ((VtxDeg‘𝐺)‘𝑢) = 𝑚)) |
39 | 38 | rexbidv 3052 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑚 → (∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑘 ↔ ∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑚)) |
40 | | breq2 4657 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑚 → (𝐺 RegUSGraph 𝑘 ↔ 𝐺 RegUSGraph 𝑚)) |
41 | 40 | orbi1d 739 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑚 → ((𝐺 RegUSGraph 𝑘 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺)) ↔ (𝐺 RegUSGraph 𝑚 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺)))) |
42 | 39, 41 | imbi12d 334 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑚 → ((∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑘 → (𝐺 RegUSGraph 𝑘 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) ↔ (∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑚 → (𝐺 RegUSGraph 𝑚 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))))) |
43 | 40 | notbid 308 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑚 → (¬ 𝐺 RegUSGraph 𝑘 ↔ ¬ 𝐺 RegUSGraph 𝑚)) |
44 | 42, 43 | anbi12d 747 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑚 → (((∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑘 → (𝐺 RegUSGraph 𝑘 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) ∧ ¬ 𝐺 RegUSGraph 𝑘) ↔ ((∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑚 → (𝐺 RegUSGraph 𝑚 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) ∧ ¬ 𝐺 RegUSGraph 𝑚))) |
45 | 44 | imbi1d 331 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑚 → ((((∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑘 → (𝐺 RegUSGraph 𝑘 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) ∧ ¬ 𝐺 RegUSGraph 𝑘) → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺)) ↔ (((∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑚 → (𝐺 RegUSGraph 𝑚 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) ∧ ¬ 𝐺 RegUSGraph 𝑚) → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺)))) |
46 | 45 | adantl 482 |
. . . . . . . . . . 11
⊢
(((((𝑡 ∈ 𝑉 ∧ 𝑚 ∈ ℕ0) ∧
((VtxDeg‘𝐺)‘𝑡) = 𝑚) ∧ (𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉))) ∧ 𝑘 = 𝑚) → ((((∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑘 → (𝐺 RegUSGraph 𝑘 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) ∧ ¬ 𝐺 RegUSGraph 𝑘) → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺)) ↔ (((∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑚 → (𝐺 RegUSGraph 𝑚 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) ∧ ¬ 𝐺 RegUSGraph 𝑚) → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺)))) |
47 | 37, 46 | mpbird 247 |
. . . . . . . . . 10
⊢
(((((𝑡 ∈ 𝑉 ∧ 𝑚 ∈ ℕ0) ∧
((VtxDeg‘𝐺)‘𝑡) = 𝑚) ∧ (𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉))) ∧ 𝑘 = 𝑚) → (((∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑘 → (𝐺 RegUSGraph 𝑘 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) ∧ ¬ 𝐺 RegUSGraph 𝑘) → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) |
48 | 30, 47 | rspcimdv 3310 |
. . . . . . . . 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 225 |
. . . . . . 7
⊢
((∀𝑘 ∈
ℕ0 (∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑘 → (𝐺 RegUSGraph 𝑘 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) ∧ ∀𝑘 ∈ ℕ0 ¬ 𝐺 RegUSGraph 𝑘) → ((((𝑡 ∈ 𝑉 ∧ 𝑚 ∈ ℕ0) ∧
((VtxDeg‘𝐺)‘𝑡) = 𝑚) ∧ (𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉))) → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) |
51 | 50 | expcom 451 |
. . . . . 6
⊢
(∀𝑘 ∈
ℕ0 ¬ 𝐺
RegUSGraph 𝑘 →
(∀𝑘 ∈
ℕ0 (∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑘 → (𝐺 RegUSGraph 𝑘 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) → ((((𝑡 ∈ 𝑉 ∧ 𝑚 ∈ ℕ0) ∧
((VtxDeg‘𝐺)‘𝑡) = 𝑚) ∧ (𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉))) → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺)))) |
52 | 51 | com13 88 |
. . . . 5
⊢ ((((𝑡 ∈ 𝑉 ∧ 𝑚 ∈ ℕ0) ∧
((VtxDeg‘𝐺)‘𝑡) = 𝑚) ∧ (𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉))) → (∀𝑘 ∈ ℕ0
(∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑘 → (𝐺 RegUSGraph 𝑘 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) → (∀𝑘 ∈ ℕ0 ¬ 𝐺 RegUSGraph 𝑘 → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺)))) |
53 | 52 | exp31 630 |
. . . 4
⊢ ((𝑡 ∈ 𝑉 ∧ 𝑚 ∈ ℕ0) →
(((VtxDeg‘𝐺)‘𝑡) = 𝑚 → ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉)) → (∀𝑘 ∈ ℕ0
(∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑘 → (𝐺 RegUSGraph 𝑘 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) → (∀𝑘 ∈ ℕ0 ¬ 𝐺 RegUSGraph 𝑘 → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺)))))) |
54 | 53 | rexlimivv 3036 |
. . 3
⊢
(∃𝑡 ∈
𝑉 ∃𝑚 ∈ ℕ0
((VtxDeg‘𝐺)‘𝑡) = 𝑚 → ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉)) → (∀𝑘 ∈ ℕ0
(∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑘 → (𝐺 RegUSGraph 𝑘 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) → (∀𝑘 ∈ ℕ0 ¬ 𝐺 RegUSGraph 𝑘 → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))))) |
55 | 28, 54 | mpcom 38 |
. 2
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 <
(#‘𝑉)) →
(∀𝑘 ∈
ℕ0 (∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑘 → (𝐺 RegUSGraph 𝑘 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) → (∀𝑘 ∈ ℕ0 ¬ 𝐺 RegUSGraph 𝑘 → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺)))) |
56 | 4, 5, 55 | mp2d 49 |
1
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 <
(#‘𝑉)) →
∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺)) |