Step | Hyp | Ref
| Expression |
1 | | frgrreggt1.v |
. . . 4
⊢ 𝑉 = (Vtx‘𝐺) |
2 | | eqid 2740 |
. . . 4
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
3 | 1, 2 | frgrregorufrg 28686 |
. . 3
⊢ (𝐺 ∈ FriendGraph →
∀𝑘 ∈
ℕ0 (∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑘 → (𝐺 RegUSGraph 𝑘 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺)))) |
4 | 3 | 3ad2ant1 1132 |
. 2
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 <
(♯‘𝑉)) →
∀𝑘 ∈
ℕ0 (∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑘 → (𝐺 RegUSGraph 𝑘 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺)))) |
5 | 1 | frgrogt3nreg 28757 |
. 2
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 <
(♯‘𝑉)) →
∀𝑘 ∈
ℕ0 ¬ 𝐺
RegUSGraph 𝑘) |
6 | | frgrusgr 28621 |
. . . . . . 7
⊢ (𝐺 ∈ FriendGraph → 𝐺 ∈
USGraph) |
7 | 6 | anim1i 615 |
. . . . . 6
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) → (𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin)) |
8 | 1 | isfusgr 27683 |
. . . . . 6
⊢ (𝐺 ∈ FinUSGraph ↔ (𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin)) |
9 | 7, 8 | sylibr 233 |
. . . . 5
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) → 𝐺 ∈
FinUSGraph) |
10 | 9 | 3adant3 1131 |
. . . 4
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 <
(♯‘𝑉)) →
𝐺 ∈
FinUSGraph) |
11 | | 0red 10979 |
. . . . . . . 8
⊢ ((𝑉 ∈ Fin ∧ 3 <
(♯‘𝑉)) → 0
∈ ℝ) |
12 | | 3re 12053 |
. . . . . . . . 9
⊢ 3 ∈
ℝ |
13 | 12 | a1i 11 |
. . . . . . . 8
⊢ ((𝑉 ∈ Fin ∧ 3 <
(♯‘𝑉)) → 3
∈ ℝ) |
14 | | hashcl 14069 |
. . . . . . . . . 10
⊢ (𝑉 ∈ Fin →
(♯‘𝑉) ∈
ℕ0) |
15 | 14 | nn0red 12294 |
. . . . . . . . 9
⊢ (𝑉 ∈ Fin →
(♯‘𝑉) ∈
ℝ) |
16 | 15 | adantr 481 |
. . . . . . . 8
⊢ ((𝑉 ∈ Fin ∧ 3 <
(♯‘𝑉)) →
(♯‘𝑉) ∈
ℝ) |
17 | | 3pos 12078 |
. . . . . . . . 9
⊢ 0 <
3 |
18 | 17 | a1i 11 |
. . . . . . . 8
⊢ ((𝑉 ∈ Fin ∧ 3 <
(♯‘𝑉)) → 0
< 3) |
19 | | simpr 485 |
. . . . . . . 8
⊢ ((𝑉 ∈ Fin ∧ 3 <
(♯‘𝑉)) → 3
< (♯‘𝑉)) |
20 | 11, 13, 16, 18, 19 | lttrd 11136 |
. . . . . . 7
⊢ ((𝑉 ∈ Fin ∧ 3 <
(♯‘𝑉)) → 0
< (♯‘𝑉)) |
21 | 20 | gt0ne0d 11539 |
. . . . . 6
⊢ ((𝑉 ∈ Fin ∧ 3 <
(♯‘𝑉)) →
(♯‘𝑉) ≠
0) |
22 | | hasheq0 14076 |
. . . . . . . 8
⊢ (𝑉 ∈ Fin →
((♯‘𝑉) = 0
↔ 𝑉 =
∅)) |
23 | 22 | adantr 481 |
. . . . . . 7
⊢ ((𝑉 ∈ Fin ∧ 3 <
(♯‘𝑉)) →
((♯‘𝑉) = 0
↔ 𝑉 =
∅)) |
24 | 23 | necon3bid 2990 |
. . . . . 6
⊢ ((𝑉 ∈ Fin ∧ 3 <
(♯‘𝑉)) →
((♯‘𝑉) ≠ 0
↔ 𝑉 ≠
∅)) |
25 | 21, 24 | mpbid 231 |
. . . . 5
⊢ ((𝑉 ∈ Fin ∧ 3 <
(♯‘𝑉)) →
𝑉 ≠
∅) |
26 | 25 | 3adant1 1129 |
. . . 4
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 <
(♯‘𝑉)) →
𝑉 ≠
∅) |
27 | 1 | fusgrn0degnn0 27864 |
. . . 4
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) →
∃𝑡 ∈ 𝑉 ∃𝑚 ∈ ℕ0
((VtxDeg‘𝐺)‘𝑡) = 𝑚) |
28 | 10, 26, 27 | syl2anc 584 |
. . 3
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 <
(♯‘𝑉)) →
∃𝑡 ∈ 𝑉 ∃𝑚 ∈ ℕ0
((VtxDeg‘𝐺)‘𝑡) = 𝑚) |
29 | | r19.26 3097 |
. . . . . . . 8
⊢
(∀𝑘 ∈
ℕ0 ((∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑘 → (𝐺 RegUSGraph 𝑘 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) ∧ ¬ 𝐺 RegUSGraph 𝑘) ↔ (∀𝑘 ∈ ℕ0 (∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑘 → (𝐺 RegUSGraph 𝑘 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) ∧ ∀𝑘 ∈ ℕ0 ¬ 𝐺 RegUSGraph 𝑘)) |
30 | | simpllr 773 |
. . . . . . . . . 10
⊢ ((((𝑡 ∈ 𝑉 ∧ 𝑚 ∈ ℕ0) ∧
((VtxDeg‘𝐺)‘𝑡) = 𝑚) ∧ (𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 <
(♯‘𝑉))) →
𝑚 ∈
ℕ0) |
31 | | fveqeq2 6780 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 = 𝑡 → (((VtxDeg‘𝐺)‘𝑢) = 𝑚 ↔ ((VtxDeg‘𝐺)‘𝑡) = 𝑚)) |
32 | 31 | rspcev 3561 |
. . . . . . . . . . . . . 14
⊢ ((𝑡 ∈ 𝑉 ∧ ((VtxDeg‘𝐺)‘𝑡) = 𝑚) → ∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑚) |
33 | 32 | ad4ant13 748 |
. . . . . . . . . . . . 13
⊢ ((((𝑡 ∈ 𝑉 ∧ 𝑚 ∈ ℕ0) ∧
((VtxDeg‘𝐺)‘𝑡) = 𝑚) ∧ (𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 <
(♯‘𝑉))) →
∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑚) |
34 | | ornld 1059 |
. . . . . . . . . . . . 13
⊢
(∃𝑢 ∈
𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑚 → (((∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑚 → (𝐺 RegUSGraph 𝑚 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) ∧ ¬ 𝐺 RegUSGraph 𝑚) → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) |
35 | 33, 34 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝑡 ∈ 𝑉 ∧ 𝑚 ∈ ℕ0) ∧
((VtxDeg‘𝐺)‘𝑡) = 𝑚) ∧ (𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 <
(♯‘𝑉))) →
(((∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑚 → (𝐺 RegUSGraph 𝑚 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) ∧ ¬ 𝐺 RegUSGraph 𝑚) → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) |
36 | 35 | adantr 481 |
. . . . . . . . . . 11
⊢
(((((𝑡 ∈ 𝑉 ∧ 𝑚 ∈ ℕ0) ∧
((VtxDeg‘𝐺)‘𝑡) = 𝑚) ∧ (𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 <
(♯‘𝑉))) ∧
𝑘 = 𝑚) → (((∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑚 → (𝐺 RegUSGraph 𝑚 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) ∧ ¬ 𝐺 RegUSGraph 𝑚) → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) |
37 | | eqeq2 2752 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑚 → (((VtxDeg‘𝐺)‘𝑢) = 𝑘 ↔ ((VtxDeg‘𝐺)‘𝑢) = 𝑚)) |
38 | 37 | rexbidv 3228 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑚 → (∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑘 ↔ ∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑚)) |
39 | | breq2 5083 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑚 → (𝐺 RegUSGraph 𝑘 ↔ 𝐺 RegUSGraph 𝑚)) |
40 | 39 | orbi1d 914 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑚 → ((𝐺 RegUSGraph 𝑘 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺)) ↔ (𝐺 RegUSGraph 𝑚 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺)))) |
41 | 38, 40 | imbi12d 345 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑚 → ((∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑘 → (𝐺 RegUSGraph 𝑘 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) ↔ (∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑚 → (𝐺 RegUSGraph 𝑚 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))))) |
42 | 39 | notbid 318 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑚 → (¬ 𝐺 RegUSGraph 𝑘 ↔ ¬ 𝐺 RegUSGraph 𝑚)) |
43 | 41, 42 | anbi12d 631 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑚 → (((∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑘 → (𝐺 RegUSGraph 𝑘 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) ∧ ¬ 𝐺 RegUSGraph 𝑘) ↔ ((∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑚 → (𝐺 RegUSGraph 𝑚 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) ∧ ¬ 𝐺 RegUSGraph 𝑚))) |
44 | 43 | imbi1d 342 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑚 → ((((∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑘 → (𝐺 RegUSGraph 𝑘 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) ∧ ¬ 𝐺 RegUSGraph 𝑘) → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺)) ↔ (((∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑚 → (𝐺 RegUSGraph 𝑚 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) ∧ ¬ 𝐺 RegUSGraph 𝑚) → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺)))) |
45 | 44 | adantl 482 |
. . . . . . . . . . 11
⊢
(((((𝑡 ∈ 𝑉 ∧ 𝑚 ∈ ℕ0) ∧
((VtxDeg‘𝐺)‘𝑡) = 𝑚) ∧ (𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 <
(♯‘𝑉))) ∧
𝑘 = 𝑚) → ((((∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑘 → (𝐺 RegUSGraph 𝑘 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) ∧ ¬ 𝐺 RegUSGraph 𝑘) → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺)) ↔ (((∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑚 → (𝐺 RegUSGraph 𝑚 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) ∧ ¬ 𝐺 RegUSGraph 𝑚) → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺)))) |
46 | 36, 45 | mpbird 256 |
. . . . . . . . . 10
⊢
(((((𝑡 ∈ 𝑉 ∧ 𝑚 ∈ ℕ0) ∧
((VtxDeg‘𝐺)‘𝑡) = 𝑚) ∧ (𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 <
(♯‘𝑉))) ∧
𝑘 = 𝑚) → (((∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑘 → (𝐺 RegUSGraph 𝑘 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) ∧ ¬ 𝐺 RegUSGraph 𝑘) → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) |
47 | 30, 46 | rspcimdv 3550 |
. . . . . . . . 9
⊢ ((((𝑡 ∈ 𝑉 ∧ 𝑚 ∈ ℕ0) ∧
((VtxDeg‘𝐺)‘𝑡) = 𝑚) ∧ (𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 <
(♯‘𝑉))) →
(∀𝑘 ∈
ℕ0 ((∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑘 → (𝐺 RegUSGraph 𝑘 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) ∧ ¬ 𝐺 RegUSGraph 𝑘) → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) |
48 | 47 | com12 32 |
. . . . . . . 8
⊢
(∀𝑘 ∈
ℕ0 ((∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑘 → (𝐺 RegUSGraph 𝑘 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) ∧ ¬ 𝐺 RegUSGraph 𝑘) → ((((𝑡 ∈ 𝑉 ∧ 𝑚 ∈ ℕ0) ∧
((VtxDeg‘𝐺)‘𝑡) = 𝑚) ∧ (𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 <
(♯‘𝑉))) →
∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) |
49 | 29, 48 | sylbir 234 |
. . . . . . 7
⊢
((∀𝑘 ∈
ℕ0 (∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑘 → (𝐺 RegUSGraph 𝑘 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) ∧ ∀𝑘 ∈ ℕ0 ¬ 𝐺 RegUSGraph 𝑘) → ((((𝑡 ∈ 𝑉 ∧ 𝑚 ∈ ℕ0) ∧
((VtxDeg‘𝐺)‘𝑡) = 𝑚) ∧ (𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 <
(♯‘𝑉))) →
∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) |
50 | 49 | expcom 414 |
. . . . . 6
⊢
(∀𝑘 ∈
ℕ0 ¬ 𝐺
RegUSGraph 𝑘 →
(∀𝑘 ∈
ℕ0 (∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑘 → (𝐺 RegUSGraph 𝑘 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) → ((((𝑡 ∈ 𝑉 ∧ 𝑚 ∈ ℕ0) ∧
((VtxDeg‘𝐺)‘𝑡) = 𝑚) ∧ (𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 <
(♯‘𝑉))) →
∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺)))) |
51 | 50 | com13 88 |
. . . . 5
⊢ ((((𝑡 ∈ 𝑉 ∧ 𝑚 ∈ ℕ0) ∧
((VtxDeg‘𝐺)‘𝑡) = 𝑚) ∧ (𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 <
(♯‘𝑉))) →
(∀𝑘 ∈
ℕ0 (∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑘 → (𝐺 RegUSGraph 𝑘 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) → (∀𝑘 ∈ ℕ0 ¬ 𝐺 RegUSGraph 𝑘 → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺)))) |
52 | 51 | exp31 420 |
. . . 4
⊢ ((𝑡 ∈ 𝑉 ∧ 𝑚 ∈ ℕ0) →
(((VtxDeg‘𝐺)‘𝑡) = 𝑚 → ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 <
(♯‘𝑉)) →
(∀𝑘 ∈
ℕ0 (∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑘 → (𝐺 RegUSGraph 𝑘 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) → (∀𝑘 ∈ ℕ0 ¬ 𝐺 RegUSGraph 𝑘 → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺)))))) |
53 | 52 | rexlimivv 3223 |
. . 3
⊢
(∃𝑡 ∈
𝑉 ∃𝑚 ∈ ℕ0
((VtxDeg‘𝐺)‘𝑡) = 𝑚 → ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 <
(♯‘𝑉)) →
(∀𝑘 ∈
ℕ0 (∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑘 → (𝐺 RegUSGraph 𝑘 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) → (∀𝑘 ∈ ℕ0 ¬ 𝐺 RegUSGraph 𝑘 → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))))) |
54 | 28, 53 | mpcom 38 |
. 2
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 <
(♯‘𝑉)) →
(∀𝑘 ∈
ℕ0 (∃𝑢 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑢) = 𝑘 → (𝐺 RegUSGraph 𝑘 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) → (∀𝑘 ∈ ℕ0 ¬ 𝐺 RegUSGraph 𝑘 → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺)))) |
55 | 4, 5, 54 | mp2d 49 |
1
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 <
(♯‘𝑉)) →
∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺)) |