Step | Hyp | Ref
| Expression |
1 | | frgraregorufrg 26599 |
. . 3
⊢ (𝑉 FriendGrph 𝐸 → ∀𝑛 ∈ ℕ0 (∃𝑢 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑢) = 𝑛 → (〈𝑉, 𝐸〉 RegUSGrph 𝑛 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ ran 𝐸))) |
2 | 1 | 3ad2ant1 1075 |
. 2
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉)) → ∀𝑛 ∈ ℕ0
(∃𝑢 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑢) = 𝑛 → (〈𝑉, 𝐸〉 RegUSGrph 𝑛 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ ran 𝐸))) |
3 | | frgraogt3nreg 26647 |
. 2
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉)) → ∀𝑛 ∈ ℕ0
¬ 〈𝑉, 𝐸〉 RegUSGrph 𝑛) |
4 | | frisusgra 26519 |
. . . . 5
⊢ (𝑉 FriendGrph 𝐸 → 𝑉 USGrph 𝐸) |
5 | 4 | 3ad2ant1 1075 |
. . . 4
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉)) → 𝑉 USGrph 𝐸) |
6 | | simp2 1055 |
. . . 4
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉)) → 𝑉 ∈ Fin) |
7 | | 0red 9920 |
. . . . . . . 8
⊢ ((𝑉 ∈ Fin ∧ 3 <
(#‘𝑉)) → 0
∈ ℝ) |
8 | | 3re 10971 |
. . . . . . . . 9
⊢ 3 ∈
ℝ |
9 | 8 | a1i 11 |
. . . . . . . 8
⊢ ((𝑉 ∈ Fin ∧ 3 <
(#‘𝑉)) → 3
∈ ℝ) |
10 | | hashcl 13009 |
. . . . . . . . . 10
⊢ (𝑉 ∈ Fin →
(#‘𝑉) ∈
ℕ0) |
11 | 10 | nn0red 11229 |
. . . . . . . . 9
⊢ (𝑉 ∈ Fin →
(#‘𝑉) ∈
ℝ) |
12 | 11 | adantr 480 |
. . . . . . . 8
⊢ ((𝑉 ∈ Fin ∧ 3 <
(#‘𝑉)) →
(#‘𝑉) ∈
ℝ) |
13 | | 3pos 10991 |
. . . . . . . . 9
⊢ 0 <
3 |
14 | 13 | a1i 11 |
. . . . . . . 8
⊢ ((𝑉 ∈ Fin ∧ 3 <
(#‘𝑉)) → 0 <
3) |
15 | | simpr 476 |
. . . . . . . 8
⊢ ((𝑉 ∈ Fin ∧ 3 <
(#‘𝑉)) → 3 <
(#‘𝑉)) |
16 | 7, 9, 12, 14, 15 | lttrd 10077 |
. . . . . . 7
⊢ ((𝑉 ∈ Fin ∧ 3 <
(#‘𝑉)) → 0 <
(#‘𝑉)) |
17 | 16 | gt0ne0d 10471 |
. . . . . 6
⊢ ((𝑉 ∈ Fin ∧ 3 <
(#‘𝑉)) →
(#‘𝑉) ≠
0) |
18 | | hasheq0 13015 |
. . . . . . . 8
⊢ (𝑉 ∈ Fin →
((#‘𝑉) = 0 ↔
𝑉 =
∅)) |
19 | 18 | adantr 480 |
. . . . . . 7
⊢ ((𝑉 ∈ Fin ∧ 3 <
(#‘𝑉)) →
((#‘𝑉) = 0 ↔
𝑉 =
∅)) |
20 | 19 | necon3bid 2826 |
. . . . . 6
⊢ ((𝑉 ∈ Fin ∧ 3 <
(#‘𝑉)) →
((#‘𝑉) ≠ 0 ↔
𝑉 ≠
∅)) |
21 | 17, 20 | mpbid 221 |
. . . . 5
⊢ ((𝑉 ∈ Fin ∧ 3 <
(#‘𝑉)) → 𝑉 ≠ ∅) |
22 | 21 | 3adant1 1072 |
. . . 4
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉)) → 𝑉 ≠ ∅) |
23 | | usgn0fidegnn0 26556 |
. . . 4
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ∃𝑡 ∈ 𝑉 ∃𝑚 ∈ ℕ0 ((𝑉 VDeg 𝐸)‘𝑡) = 𝑚) |
24 | 5, 6, 22, 23 | syl3anc 1318 |
. . 3
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉)) → ∃𝑡 ∈ 𝑉 ∃𝑚 ∈ ℕ0 ((𝑉 VDeg 𝐸)‘𝑡) = 𝑚) |
25 | | r19.26 3046 |
. . . . . . . 8
⊢
(∀𝑛 ∈
ℕ0 ((∃𝑢 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑢) = 𝑛 → (〈𝑉, 𝐸〉 RegUSGrph 𝑛 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ ran 𝐸)) ∧ ¬ 〈𝑉, 𝐸〉 RegUSGrph 𝑛) ↔ (∀𝑛 ∈ ℕ0 (∃𝑢 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑢) = 𝑛 → (〈𝑉, 𝐸〉 RegUSGrph 𝑛 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ ran 𝐸)) ∧ ∀𝑛 ∈ ℕ0 ¬ 〈𝑉, 𝐸〉 RegUSGrph 𝑛)) |
26 | | simpllr 795 |
. . . . . . . . . 10
⊢ ((((𝑡 ∈ 𝑉 ∧ 𝑚 ∈ ℕ0) ∧ ((𝑉 VDeg 𝐸)‘𝑡) = 𝑚) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉))) → 𝑚 ∈ ℕ0) |
27 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 = 𝑡 → ((𝑉 VDeg 𝐸)‘𝑢) = ((𝑉 VDeg 𝐸)‘𝑡)) |
28 | 27 | eqeq1d 2612 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 = 𝑡 → (((𝑉 VDeg 𝐸)‘𝑢) = 𝑚 ↔ ((𝑉 VDeg 𝐸)‘𝑡) = 𝑚)) |
29 | 28 | rspcev 3282 |
. . . . . . . . . . . . . . 15
⊢ ((𝑡 ∈ 𝑉 ∧ ((𝑉 VDeg 𝐸)‘𝑡) = 𝑚) → ∃𝑢 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑢) = 𝑚) |
30 | 29 | adantlr 747 |
. . . . . . . . . . . . . 14
⊢ (((𝑡 ∈ 𝑉 ∧ 𝑚 ∈ ℕ0) ∧ ((𝑉 VDeg 𝐸)‘𝑡) = 𝑚) → ∃𝑢 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑢) = 𝑚) |
31 | 30 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝑡 ∈ 𝑉 ∧ 𝑚 ∈ ℕ0) ∧ ((𝑉 VDeg 𝐸)‘𝑡) = 𝑚) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉))) → ∃𝑢 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑢) = 𝑚) |
32 | | ornld 938 |
. . . . . . . . . . . . 13
⊢
(∃𝑢 ∈
𝑉 ((𝑉 VDeg 𝐸)‘𝑢) = 𝑚 → (((∃𝑢 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑢) = 𝑚 → (〈𝑉, 𝐸〉 RegUSGrph 𝑚 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ ran 𝐸)) ∧ ¬ 〈𝑉, 𝐸〉 RegUSGrph 𝑚) → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ ran 𝐸)) |
33 | 31, 32 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝑡 ∈ 𝑉 ∧ 𝑚 ∈ ℕ0) ∧ ((𝑉 VDeg 𝐸)‘𝑡) = 𝑚) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉))) → (((∃𝑢 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑢) = 𝑚 → (〈𝑉, 𝐸〉 RegUSGrph 𝑚 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ ran 𝐸)) ∧ ¬ 〈𝑉, 𝐸〉 RegUSGrph 𝑚) → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ ran 𝐸)) |
34 | 33 | adantr 480 |
. . . . . . . . . . 11
⊢
(((((𝑡 ∈ 𝑉 ∧ 𝑚 ∈ ℕ0) ∧ ((𝑉 VDeg 𝐸)‘𝑡) = 𝑚) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉))) ∧ 𝑛 = 𝑚) → (((∃𝑢 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑢) = 𝑚 → (〈𝑉, 𝐸〉 RegUSGrph 𝑚 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ ran 𝐸)) ∧ ¬ 〈𝑉, 𝐸〉 RegUSGrph 𝑚) → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ ran 𝐸)) |
35 | | eqeq2 2621 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑚 → (((𝑉 VDeg 𝐸)‘𝑢) = 𝑛 ↔ ((𝑉 VDeg 𝐸)‘𝑢) = 𝑚)) |
36 | 35 | rexbidv 3034 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑚 → (∃𝑢 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑢) = 𝑛 ↔ ∃𝑢 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑢) = 𝑚)) |
37 | | breq2 4587 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑚 → (〈𝑉, 𝐸〉 RegUSGrph 𝑛 ↔ 〈𝑉, 𝐸〉 RegUSGrph 𝑚)) |
38 | 37 | orbi1d 735 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑚 → ((〈𝑉, 𝐸〉 RegUSGrph 𝑛 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ ran 𝐸) ↔ (〈𝑉, 𝐸〉 RegUSGrph 𝑚 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ ran 𝐸))) |
39 | 36, 38 | imbi12d 333 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑚 → ((∃𝑢 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑢) = 𝑛 → (〈𝑉, 𝐸〉 RegUSGrph 𝑛 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ ran 𝐸)) ↔ (∃𝑢 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑢) = 𝑚 → (〈𝑉, 𝐸〉 RegUSGrph 𝑚 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ ran 𝐸)))) |
40 | 37 | notbid 307 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑚 → (¬ 〈𝑉, 𝐸〉 RegUSGrph 𝑛 ↔ ¬ 〈𝑉, 𝐸〉 RegUSGrph 𝑚)) |
41 | 39, 40 | anbi12d 743 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑚 → (((∃𝑢 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑢) = 𝑛 → (〈𝑉, 𝐸〉 RegUSGrph 𝑛 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ ran 𝐸)) ∧ ¬ 〈𝑉, 𝐸〉 RegUSGrph 𝑛) ↔ ((∃𝑢 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑢) = 𝑚 → (〈𝑉, 𝐸〉 RegUSGrph 𝑚 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ ran 𝐸)) ∧ ¬ 〈𝑉, 𝐸〉 RegUSGrph 𝑚))) |
42 | 41 | imbi1d 330 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑚 → ((((∃𝑢 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑢) = 𝑛 → (〈𝑉, 𝐸〉 RegUSGrph 𝑛 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ ran 𝐸)) ∧ ¬ 〈𝑉, 𝐸〉 RegUSGrph 𝑛) → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ ran 𝐸) ↔ (((∃𝑢 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑢) = 𝑚 → (〈𝑉, 𝐸〉 RegUSGrph 𝑚 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ ran 𝐸)) ∧ ¬ 〈𝑉, 𝐸〉 RegUSGrph 𝑚) → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ ran 𝐸))) |
43 | 42 | adantl 481 |
. . . . . . . . . . 11
⊢
(((((𝑡 ∈ 𝑉 ∧ 𝑚 ∈ ℕ0) ∧ ((𝑉 VDeg 𝐸)‘𝑡) = 𝑚) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉))) ∧ 𝑛 = 𝑚) → ((((∃𝑢 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑢) = 𝑛 → (〈𝑉, 𝐸〉 RegUSGrph 𝑛 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ ran 𝐸)) ∧ ¬ 〈𝑉, 𝐸〉 RegUSGrph 𝑛) → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ ran 𝐸) ↔ (((∃𝑢 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑢) = 𝑚 → (〈𝑉, 𝐸〉 RegUSGrph 𝑚 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ ran 𝐸)) ∧ ¬ 〈𝑉, 𝐸〉 RegUSGrph 𝑚) → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ ran 𝐸))) |
44 | 34, 43 | mpbird 246 |
. . . . . . . . . 10
⊢
(((((𝑡 ∈ 𝑉 ∧ 𝑚 ∈ ℕ0) ∧ ((𝑉 VDeg 𝐸)‘𝑡) = 𝑚) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉))) ∧ 𝑛 = 𝑚) → (((∃𝑢 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑢) = 𝑛 → (〈𝑉, 𝐸〉 RegUSGrph 𝑛 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ ran 𝐸)) ∧ ¬ 〈𝑉, 𝐸〉 RegUSGrph 𝑛) → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ ran 𝐸)) |
45 | 26, 44 | rspcimdv 3283 |
. . . . . . . . 9
⊢ ((((𝑡 ∈ 𝑉 ∧ 𝑚 ∈ ℕ0) ∧ ((𝑉 VDeg 𝐸)‘𝑡) = 𝑚) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉))) → (∀𝑛 ∈ ℕ0
((∃𝑢 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑢) = 𝑛 → (〈𝑉, 𝐸〉 RegUSGrph 𝑛 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ ran 𝐸)) ∧ ¬ 〈𝑉, 𝐸〉 RegUSGrph 𝑛) → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ ran 𝐸)) |
46 | 45 | com12 32 |
. . . . . . . 8
⊢
(∀𝑛 ∈
ℕ0 ((∃𝑢 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑢) = 𝑛 → (〈𝑉, 𝐸〉 RegUSGrph 𝑛 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ ran 𝐸)) ∧ ¬ 〈𝑉, 𝐸〉 RegUSGrph 𝑛) → ((((𝑡 ∈ 𝑉 ∧ 𝑚 ∈ ℕ0) ∧ ((𝑉 VDeg 𝐸)‘𝑡) = 𝑚) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉))) → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ ran 𝐸)) |
47 | 25, 46 | sylbir 224 |
. . . . . . 7
⊢
((∀𝑛 ∈
ℕ0 (∃𝑢 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑢) = 𝑛 → (〈𝑉, 𝐸〉 RegUSGrph 𝑛 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ ran 𝐸)) ∧ ∀𝑛 ∈ ℕ0 ¬ 〈𝑉, 𝐸〉 RegUSGrph 𝑛) → ((((𝑡 ∈ 𝑉 ∧ 𝑚 ∈ ℕ0) ∧ ((𝑉 VDeg 𝐸)‘𝑡) = 𝑚) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉))) → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ ran 𝐸)) |
48 | 47 | expcom 450 |
. . . . . 6
⊢
(∀𝑛 ∈
ℕ0 ¬ 〈𝑉, 𝐸〉 RegUSGrph 𝑛 → (∀𝑛 ∈ ℕ0 (∃𝑢 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑢) = 𝑛 → (〈𝑉, 𝐸〉 RegUSGrph 𝑛 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ ran 𝐸)) → ((((𝑡 ∈ 𝑉 ∧ 𝑚 ∈ ℕ0) ∧ ((𝑉 VDeg 𝐸)‘𝑡) = 𝑚) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉))) → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ ran 𝐸))) |
49 | 48 | com13 86 |
. . . . 5
⊢ ((((𝑡 ∈ 𝑉 ∧ 𝑚 ∈ ℕ0) ∧ ((𝑉 VDeg 𝐸)‘𝑡) = 𝑚) ∧ (𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉))) → (∀𝑛 ∈ ℕ0
(∃𝑢 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑢) = 𝑛 → (〈𝑉, 𝐸〉 RegUSGrph 𝑛 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ ran 𝐸)) → (∀𝑛 ∈ ℕ0 ¬ 〈𝑉, 𝐸〉 RegUSGrph 𝑛 → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ ran 𝐸))) |
50 | 49 | exp31 628 |
. . . 4
⊢ ((𝑡 ∈ 𝑉 ∧ 𝑚 ∈ ℕ0) → (((𝑉 VDeg 𝐸)‘𝑡) = 𝑚 → ((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉)) → (∀𝑛 ∈ ℕ0
(∃𝑢 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑢) = 𝑛 → (〈𝑉, 𝐸〉 RegUSGrph 𝑛 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ ran 𝐸)) → (∀𝑛 ∈ ℕ0 ¬ 〈𝑉, 𝐸〉 RegUSGrph 𝑛 → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ ran 𝐸))))) |
51 | 50 | rexlimivv 3018 |
. . 3
⊢
(∃𝑡 ∈
𝑉 ∃𝑚 ∈ ℕ0 ((𝑉 VDeg 𝐸)‘𝑡) = 𝑚 → ((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉)) → (∀𝑛 ∈ ℕ0
(∃𝑢 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑢) = 𝑛 → (〈𝑉, 𝐸〉 RegUSGrph 𝑛 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ ran 𝐸)) → (∀𝑛 ∈ ℕ0 ¬ 〈𝑉, 𝐸〉 RegUSGrph 𝑛 → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ ran 𝐸)))) |
52 | 24, 51 | mpcom 37 |
. 2
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉)) → (∀𝑛 ∈ ℕ0
(∃𝑢 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑢) = 𝑛 → (〈𝑉, 𝐸〉 RegUSGrph 𝑛 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ ran 𝐸)) → (∀𝑛 ∈ ℕ0 ¬ 〈𝑉, 𝐸〉 RegUSGrph 𝑛 → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ ran 𝐸))) |
53 | 2, 3, 52 | mp2d 47 |
1
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉)) → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ ran 𝐸) |