Step | Hyp | Ref
| Expression |
1 | | hashcl 13009 |
. . . 4
⊢ (𝑉 ∈ Fin →
(#‘𝑉) ∈
ℕ0) |
2 | | ax-1 6 |
. . . . . 6
⊢
(((#‘𝑉) = 0
∨ (#‘𝑉) = 1 ∨
(#‘𝑉) = 3) →
((((#‘𝑉) ∈
ℕ0 ∧ 𝑉
∈ Fin ∧ 𝑉
FriendGrph 𝐸) ∧
〈𝑉, 𝐸〉 RegUSGrph 𝐾) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))) |
3 | | 3ioran 1049 |
. . . . . . 7
⊢ (¬
((#‘𝑉) = 0 ∨
(#‘𝑉) = 1 ∨
(#‘𝑉) = 3) ↔
(¬ (#‘𝑉) = 0
∧ ¬ (#‘𝑉) = 1
∧ ¬ (#‘𝑉) =
3)) |
4 | | df-ne 2782 |
. . . . . . . . . . . . . 14
⊢
((#‘𝑉) ≠ 0
↔ ¬ (#‘𝑉) =
0) |
5 | | hasheq0 13015 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑉 ∈ Fin →
((#‘𝑉) = 0 ↔
𝑉 =
∅)) |
6 | 5 | necon3bid 2826 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑉 ∈ Fin →
((#‘𝑉) ≠ 0 ↔
𝑉 ≠
∅)) |
7 | 6 | biimpa 500 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑉 ∈ Fin ∧ (#‘𝑉) ≠ 0) → 𝑉 ≠ ∅) |
8 | | elnnne0 11183 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((#‘𝑉) ∈
ℕ ↔ ((#‘𝑉)
∈ ℕ0 ∧ (#‘𝑉) ≠ 0)) |
9 | | df-ne 2782 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((#‘𝑉) ≠ 1
↔ ¬ (#‘𝑉) =
1) |
10 | | eluz2b3 11638 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((#‘𝑉) ∈
(ℤ≥‘2) ↔ ((#‘𝑉) ∈ ℕ ∧ (#‘𝑉) ≠ 1)) |
11 | | hash2prde 13109 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑉 ∈ Fin ∧ (#‘𝑉) = 2) → ∃𝑎∃𝑏(𝑎 ≠ 𝑏 ∧ 𝑉 = {𝑎, 𝑏})) |
12 | | breq1 4586 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑉 = {𝑎, 𝑏} → (𝑉 FriendGrph 𝐸 ↔ {𝑎, 𝑏} FriendGrph 𝐸)) |
13 | 12 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑎 ≠ 𝑏 ∧ 𝑉 = {𝑎, 𝑏}) → (𝑉 FriendGrph 𝐸 ↔ {𝑎, 𝑏} FriendGrph 𝐸)) |
14 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ 𝑎 ∈ V |
15 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ 𝑏 ∈ V |
16 | 14, 15 | pm3.2i 470 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (𝑎 ∈ V ∧ 𝑏 ∈ V) |
17 | 16 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝑉 = {𝑎, 𝑏} → (𝑎 ∈ V ∧ 𝑏 ∈ V)) |
18 | 17 | anim1i 590 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝑉 = {𝑎, 𝑏} ∧ 𝑎 ≠ 𝑏) → ((𝑎 ∈ V ∧ 𝑏 ∈ V) ∧ 𝑎 ≠ 𝑏)) |
19 | 18 | ancoms 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝑎 ≠ 𝑏 ∧ 𝑉 = {𝑎, 𝑏}) → ((𝑎 ∈ V ∧ 𝑏 ∈ V) ∧ 𝑎 ≠ 𝑏)) |
20 | | frgra2v 26526 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (((𝑎 ∈ V ∧ 𝑏 ∈ V) ∧ 𝑎 ≠ 𝑏) → ¬ {𝑎, 𝑏} FriendGrph 𝐸) |
21 | 19, 20 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝑎 ≠ 𝑏 ∧ 𝑉 = {𝑎, 𝑏}) → ¬ {𝑎, 𝑏} FriendGrph 𝐸) |
22 | 21 | pm2.21d 117 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑎 ≠ 𝑏 ∧ 𝑉 = {𝑎, 𝑏}) → ({𝑎, 𝑏} FriendGrph 𝐸 → (𝑉 ≠ ∅ → (¬ (#‘𝑉) = 3 → (〈𝑉, 𝐸〉 RegUSGrph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))) |
23 | 13, 22 | sylbid 229 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑎 ≠ 𝑏 ∧ 𝑉 = {𝑎, 𝑏}) → (𝑉 FriendGrph 𝐸 → (𝑉 ≠ ∅ → (¬ (#‘𝑉) = 3 → (〈𝑉, 𝐸〉 RegUSGrph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))) |
24 | 23 | com23 84 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑎 ≠ 𝑏 ∧ 𝑉 = {𝑎, 𝑏}) → (𝑉 ≠ ∅ → (𝑉 FriendGrph 𝐸 → (¬ (#‘𝑉) = 3 → (〈𝑉, 𝐸〉 RegUSGrph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))) |
25 | 24 | exlimivv 1847 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
(∃𝑎∃𝑏(𝑎 ≠ 𝑏 ∧ 𝑉 = {𝑎, 𝑏}) → (𝑉 ≠ ∅ → (𝑉 FriendGrph 𝐸 → (¬ (#‘𝑉) = 3 → (〈𝑉, 𝐸〉 RegUSGrph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))) |
26 | 11, 25 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑉 ∈ Fin ∧ (#‘𝑉) = 2) → (𝑉 ≠ ∅ → (𝑉 FriendGrph 𝐸 → (¬ (#‘𝑉) = 3 → (〈𝑉, 𝐸〉 RegUSGrph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))) |
27 | 26 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑉 ∈ Fin →
((#‘𝑉) = 2 →
(𝑉 ≠ ∅ →
(𝑉 FriendGrph 𝐸 → (¬ (#‘𝑉) = 3 → (〈𝑉, 𝐸〉 RegUSGrph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))) |
28 | 27 | com23 84 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑉 ∈ Fin → (𝑉 ≠ ∅ →
((#‘𝑉) = 2 →
(𝑉 FriendGrph 𝐸 → (¬ (#‘𝑉) = 3 → (〈𝑉, 𝐸〉 RegUSGrph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))) |
29 | 28 | com14 94 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑉 FriendGrph 𝐸 → (𝑉 ≠ ∅ → ((#‘𝑉) = 2 → (𝑉 ∈ Fin → (¬ (#‘𝑉) = 3 → (〈𝑉, 𝐸〉 RegUSGrph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))) |
30 | 29 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((#‘𝑉) ∈
(ℤ≥‘2) → (𝑉 FriendGrph 𝐸 → (𝑉 ≠ ∅ → ((#‘𝑉) = 2 → (𝑉 ∈ Fin → (¬ (#‘𝑉) = 3 → (〈𝑉, 𝐸〉 RegUSGrph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))))) |
31 | 30 | 3imp 1249 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((#‘𝑉) ∈
(ℤ≥‘2) ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ≠ ∅) → ((#‘𝑉) = 2 → (𝑉 ∈ Fin → (¬ (#‘𝑉) = 3 → (〈𝑉, 𝐸〉 RegUSGrph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))) |
32 | 31 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((#‘𝑉) = 2
→ (((#‘𝑉) ∈
(ℤ≥‘2) ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ≠ ∅) → (𝑉 ∈ Fin → (¬ (#‘𝑉) = 3 → (〈𝑉, 𝐸〉 RegUSGrph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))) |
33 | | rusgraprop 26456 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → (𝑉 USGrph 𝐸 ∧ 𝐾 ∈ ℕ0 ∧
∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾)) |
34 | | eluz2 11569 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . 53
⊢
((#‘𝑉) ∈
(ℤ≥‘2) ↔ (2 ∈ ℤ ∧ (#‘𝑉) ∈ ℤ ∧ 2 ≤
(#‘𝑉))) |
35 | | 1red 9934 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . 55
⊢
(((#‘𝑉) ∈
ℤ ∧ 2 ≤ (#‘𝑉)) → 1 ∈ ℝ) |
36 | | 2re 10967 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . 56
⊢ 2 ∈
ℝ |
37 | 36 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . 55
⊢
(((#‘𝑉) ∈
ℤ ∧ 2 ≤ (#‘𝑉)) → 2 ∈ ℝ) |
38 | | zre 11258 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . 56
⊢
((#‘𝑉) ∈
ℤ → (#‘𝑉)
∈ ℝ) |
39 | 38 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . 55
⊢
(((#‘𝑉) ∈
ℤ ∧ 2 ≤ (#‘𝑉)) → (#‘𝑉) ∈ ℝ) |
40 | | 1lt2 11071 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . 56
⊢ 1 <
2 |
41 | 40 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . 55
⊢
(((#‘𝑉) ∈
ℤ ∧ 2 ≤ (#‘𝑉)) → 1 < 2) |
42 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . 55
⊢
(((#‘𝑉) ∈
ℤ ∧ 2 ≤ (#‘𝑉)) → 2 ≤ (#‘𝑉)) |
43 | 35, 37, 39, 41, 42 | ltletrd 10076 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . 54
⊢
(((#‘𝑉) ∈
ℤ ∧ 2 ≤ (#‘𝑉)) → 1 < (#‘𝑉)) |
44 | 43 | 3adant1 1072 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . 53
⊢ ((2
∈ ℤ ∧ (#‘𝑉) ∈ ℤ ∧ 2 ≤ (#‘𝑉)) → 1 < (#‘𝑉)) |
45 | 34, 44 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . 52
⊢
((#‘𝑉) ∈
(ℤ≥‘2) → 1 < (#‘𝑉)) |
46 | 45 | anim2i 591 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . 51
⊢ ((𝑉 FriendGrph 𝐸 ∧ (#‘𝑉) ∈ (ℤ≥‘2))
→ (𝑉 FriendGrph 𝐸 ∧ 1 < (#‘𝑉))) |
47 | 46 | ancoms 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
⊢
(((#‘𝑉) ∈
(ℤ≥‘2) ∧ 𝑉 FriendGrph 𝐸) → (𝑉 FriendGrph 𝐸 ∧ 1 < (#‘𝑉))) |
48 | | vdgn0frgrav2 26551 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . 52
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑣 ∈ 𝑉) → (1 < (#‘𝑉) → ((𝑉 VDeg 𝐸)‘𝑣) ≠ 0)) |
49 | 48 | impancom 455 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . 51
⊢ ((𝑉 FriendGrph 𝐸 ∧ 1 < (#‘𝑉)) → (𝑣 ∈ 𝑉 → ((𝑉 VDeg 𝐸)‘𝑣) ≠ 0)) |
50 | 49 | ralrimiv 2948 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
⊢ ((𝑉 FriendGrph 𝐸 ∧ 1 < (#‘𝑉)) → ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) ≠ 0) |
51 | | eqeq2 2621 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . 53
⊢ (𝐾 = 0 → (((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 ↔ ((𝑉 VDeg 𝐸)‘𝑣) = 0)) |
52 | 51 | ralbidv 2969 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . 52
⊢ (𝐾 = 0 → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 ↔ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 0)) |
53 | | r19.26 3046 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . 54
⊢
(∀𝑣 ∈
𝑉 (((𝑉 VDeg 𝐸)‘𝑣) = 0 ∧ ((𝑉 VDeg 𝐸)‘𝑣) ≠ 0) ↔ (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 0 ∧ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) ≠ 0)) |
54 | | nne 2786 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . 59
⊢ (¬
((𝑉 VDeg 𝐸)‘𝑣) ≠ 0 ↔ ((𝑉 VDeg 𝐸)‘𝑣) = 0) |
55 | 54 | bicomi 213 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . 58
⊢ (((𝑉 VDeg 𝐸)‘𝑣) = 0 ↔ ¬ ((𝑉 VDeg 𝐸)‘𝑣) ≠ 0) |
56 | 55 | anbi1i 727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . 57
⊢ ((((𝑉 VDeg 𝐸)‘𝑣) = 0 ∧ ((𝑉 VDeg 𝐸)‘𝑣) ≠ 0) ↔ (¬ ((𝑉 VDeg 𝐸)‘𝑣) ≠ 0 ∧ ((𝑉 VDeg 𝐸)‘𝑣) ≠ 0)) |
57 | | ancom 465 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . 57
⊢ ((¬
((𝑉 VDeg 𝐸)‘𝑣) ≠ 0 ∧ ((𝑉 VDeg 𝐸)‘𝑣) ≠ 0) ↔ (((𝑉 VDeg 𝐸)‘𝑣) ≠ 0 ∧ ¬ ((𝑉 VDeg 𝐸)‘𝑣) ≠ 0)) |
58 | | pm3.24 922 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . 58
⊢ ¬
(((𝑉 VDeg 𝐸)‘𝑣) ≠ 0 ∧ ¬ ((𝑉 VDeg 𝐸)‘𝑣) ≠ 0) |
59 | 58 | bifal 1488 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . 57
⊢ ((((𝑉 VDeg 𝐸)‘𝑣) ≠ 0 ∧ ¬ ((𝑉 VDeg 𝐸)‘𝑣) ≠ 0) ↔ ⊥) |
60 | 56, 57, 59 | 3bitri 285 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . 56
⊢ ((((𝑉 VDeg 𝐸)‘𝑣) = 0 ∧ ((𝑉 VDeg 𝐸)‘𝑣) ≠ 0) ↔ ⊥) |
61 | 60 | ralbii 2963 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . 55
⊢
(∀𝑣 ∈
𝑉 (((𝑉 VDeg 𝐸)‘𝑣) = 0 ∧ ((𝑉 VDeg 𝐸)‘𝑣) ≠ 0) ↔ ∀𝑣 ∈ 𝑉 ⊥) |
62 | | r19.3rzv 4016 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . 58
⊢ (𝑉 ≠ ∅ → (⊥
↔ ∀𝑣 ∈
𝑉 ⊥)) |
63 | | falim 1489 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . 58
⊢ (⊥
→ ((#‘𝑉) = 0
∨ (#‘𝑉) = 1 ∨
(#‘𝑉) =
3)) |
64 | 62, 63 | syl6bir 243 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . 57
⊢ (𝑉 ≠ ∅ →
(∀𝑣 ∈ 𝑉 ⊥ → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))) |
65 | 64 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . 56
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) →
(∀𝑣 ∈ 𝑉 ⊥ → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))) |
66 | 65 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . 55
⊢
(∀𝑣 ∈
𝑉 ⊥ → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) →
((#‘𝑉) = 0 ∨
(#‘𝑉) = 1 ∨
(#‘𝑉) =
3))) |
67 | 61, 66 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . 54
⊢
(∀𝑣 ∈
𝑉 (((𝑉 VDeg 𝐸)‘𝑣) = 0 ∧ ((𝑉 VDeg 𝐸)‘𝑣) ≠ 0) → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))) |
68 | 53, 67 | sylbir 224 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . 53
⊢
((∀𝑣 ∈
𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 0 ∧ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) ≠ 0) → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))) |
69 | 68 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . 52
⊢
(∀𝑣 ∈
𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 0 → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) ≠ 0 → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))) |
70 | 52, 69 | syl6bi 242 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . 51
⊢ (𝐾 = 0 → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) ≠ 0 → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))) |
71 | 70 | com4t 91 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
⊢
(∀𝑣 ∈
𝑉 ((𝑉 VDeg 𝐸)‘𝑣) ≠ 0 → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))) |
72 | 47, 50, 71 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
⊢
(((#‘𝑉) ∈
(ℤ≥‘2) ∧ 𝑉 FriendGrph 𝐸) → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))) |
73 | 72 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢
((#‘𝑉) ∈
(ℤ≥‘2) → (𝑉 FriendGrph 𝐸 → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))) |
74 | 73 | com25 97 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢
((#‘𝑉) ∈
(ℤ≥‘2) → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (𝑉 FriendGrph 𝐸 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))) |
75 | 74 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ (((¬
(#‘𝑉) = 3 ∧ ¬
(#‘𝑉) = 2) ∧
(#‘𝑉) ∈
(ℤ≥‘2)) → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (𝑉 FriendGrph 𝐸 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))) |
76 | 75 | com15 99 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (𝑉 FriendGrph 𝐸 → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (((¬ (#‘𝑉) = 3 ∧ ¬ (#‘𝑉) = 2) ∧ (#‘𝑉) ∈
(ℤ≥‘2)) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))) |
77 | 76 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢
(∀𝑣 ∈
𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 → (𝑉 FriendGrph 𝐸 → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (((¬ (#‘𝑉) = 3 ∧ ¬ (#‘𝑉) = 2) ∧ (#‘𝑉) ∈
(ℤ≥‘2)) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))) |
78 | 77 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((𝑉 USGrph 𝐸 ∧ 𝐾 ∈ ℕ0 ∧
∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) → (𝑉 FriendGrph 𝐸 → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (((¬ (#‘𝑉) = 3 ∧ ¬ (#‘𝑉) = 2) ∧ (#‘𝑉) ∈
(ℤ≥‘2)) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))) |
79 | 33, 78 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → (𝑉 FriendGrph 𝐸 → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (((¬ (#‘𝑉) = 3 ∧ ¬ (#‘𝑉) = 2) ∧ (#‘𝑉) ∈
(ℤ≥‘2)) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))) |
80 | 79 | impcom 445 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝑉 FriendGrph 𝐸 ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (((¬ (#‘𝑉) = 3 ∧ ¬ (#‘𝑉) = 2) ∧ (#‘𝑉) ∈
(ℤ≥‘2)) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))) |
81 | 80 | impcom 445 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝑉 FriendGrph 𝐸 ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾)) → (𝐾 = 0 → (((¬ (#‘𝑉) = 3 ∧ ¬ (#‘𝑉) = 2) ∧ (#‘𝑉) ∈
(ℤ≥‘2)) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))) |
82 | | frrusgraord 26598 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((𝑉 FriendGrph 𝐸 ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) → (#‘𝑉) = ((𝐾 · (𝐾 − 1)) + 1))) |
83 | 82 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝑉 FriendGrph 𝐸 ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾)) → (#‘𝑉) = ((𝐾 · (𝐾 − 1)) + 1)) |
84 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ (𝐾 = 2 → 𝐾 = 2) |
85 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ (𝐾 = 2 → (𝐾 − 1) = (2 −
1)) |
86 | 84, 85 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (𝐾 = 2 → (𝐾 · (𝐾 − 1)) = (2 · (2 −
1))) |
87 | 86 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (𝐾 = 2 → ((𝐾 · (𝐾 − 1)) + 1) = ((2 · (2 −
1)) + 1)) |
88 | | 2m1e1 11012 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ (2
− 1) = 1 |
89 | 88 | oveq2i 6560 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ (2
· (2 − 1)) = (2 · 1) |
90 | | 2t1e2 11053 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ (2
· 1) = 2 |
91 | 89, 90 | eqtri 2632 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ (2
· (2 − 1)) = 2 |
92 | 91 | oveq1i 6559 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ ((2
· (2 − 1)) + 1) = (2 + 1) |
93 | | 2p1e3 11028 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (2 + 1) =
3 |
94 | 92, 93 | eqtri 2632 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ ((2
· (2 − 1)) + 1) = 3 |
95 | 87, 94 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (𝐾 = 2 → ((𝐾 · (𝐾 − 1)) + 1) = 3) |
96 | 95 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝐾 = 2 → ((#‘𝑉) = ((𝐾 · (𝐾 − 1)) + 1) ↔ (#‘𝑉) = 3)) |
97 | | pm2.21 119 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (¬
(#‘𝑉) = 3 →
((#‘𝑉) = 3 →
((#‘𝑉) = 0 ∨
(#‘𝑉) = 1 ∨
(#‘𝑉) =
3))) |
98 | 97 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ ((¬
(#‘𝑉) = 3 ∧ ¬
(#‘𝑉) = 2) →
((#‘𝑉) = 3 →
((#‘𝑉) = 0 ∨
(#‘𝑉) = 1 ∨
(#‘𝑉) =
3))) |
99 | 98 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (((¬
(#‘𝑉) = 3 ∧ ¬
(#‘𝑉) = 2) ∧
(#‘𝑉) ∈
(ℤ≥‘2)) → ((#‘𝑉) = 3 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))) |
100 | 99 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢
((#‘𝑉) = 3
→ (((¬ (#‘𝑉)
= 3 ∧ ¬ (#‘𝑉)
= 2) ∧ (#‘𝑉)
∈ (ℤ≥‘2)) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))) |
101 | 96, 100 | syl6bi 242 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝐾 = 2 → ((#‘𝑉) = ((𝐾 · (𝐾 − 1)) + 1) → (((¬
(#‘𝑉) = 3 ∧ ¬
(#‘𝑉) = 2) ∧
(#‘𝑉) ∈
(ℤ≥‘2)) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))) |
102 | 83, 101 | syl5com 31 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝑉 FriendGrph 𝐸 ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾)) → (𝐾 = 2 → (((¬ (#‘𝑉) = 3 ∧ ¬ (#‘𝑉) = 2) ∧ (#‘𝑉) ∈
(ℤ≥‘2)) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))) |
103 | | frgrareg 26644 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((𝑉 FriendGrph 𝐸 ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) → (𝐾 = 0 ∨ 𝐾 = 2))) |
104 | 103 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝑉 FriendGrph 𝐸 ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾)) → (𝐾 = 0 ∨ 𝐾 = 2)) |
105 | 81, 102, 104 | mpjaod 395 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝑉 FriendGrph 𝐸 ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾)) → (((¬ (#‘𝑉) = 3 ∧ ¬ (#‘𝑉) = 2) ∧ (#‘𝑉) ∈
(ℤ≥‘2)) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))) |
106 | 105 | exp32 629 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝑉 FriendGrph 𝐸 → (〈𝑉, 𝐸〉 RegUSGrph 𝐾 → (((¬ (#‘𝑉) = 3 ∧ ¬ (#‘𝑉) = 2) ∧ (#‘𝑉) ∈ (ℤ≥‘2))
→ ((#‘𝑉) = 0
∨ (#‘𝑉) = 1 ∨
(#‘𝑉) =
3))))) |
107 | 106 | com34 89 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝑉 FriendGrph 𝐸 → (((¬ (#‘𝑉) = 3 ∧ ¬ (#‘𝑉) = 2) ∧ (#‘𝑉) ∈ (ℤ≥‘2))
→ (〈𝑉, 𝐸〉 RegUSGrph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))) |
108 | 107 | com23 84 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (((¬
(#‘𝑉) = 3 ∧ ¬
(#‘𝑉) = 2) ∧
(#‘𝑉) ∈
(ℤ≥‘2)) → (𝑉 FriendGrph 𝐸 → (〈𝑉, 𝐸〉 RegUSGrph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))) |
109 | 108 | exp4c 634 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (¬
(#‘𝑉) = 3 →
(¬ (#‘𝑉) = 2
→ ((#‘𝑉) ∈
(ℤ≥‘2) → (𝑉 FriendGrph 𝐸 → (〈𝑉, 𝐸〉 RegUSGrph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))) |
110 | 109 | com34 89 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (¬
(#‘𝑉) = 3 →
((#‘𝑉) ∈
(ℤ≥‘2) → (¬ (#‘𝑉) = 2 → (𝑉 FriendGrph 𝐸 → (〈𝑉, 𝐸〉 RegUSGrph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))) |
111 | 110 | com25 97 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝑉 FriendGrph 𝐸 → ((#‘𝑉) ∈ (ℤ≥‘2)
→ (¬ (#‘𝑉) =
2 → (¬ (#‘𝑉)
= 3 → (〈𝑉, 𝐸〉 RegUSGrph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))) |
112 | 111 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑉 ∈ Fin → (𝑉 ≠ ∅ → (𝑉 FriendGrph 𝐸 → ((#‘𝑉) ∈ (ℤ≥‘2)
→ (¬ (#‘𝑉) =
2 → (¬ (#‘𝑉)
= 3 → (〈𝑉, 𝐸〉 RegUSGrph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))))) |
113 | 112 | com23 84 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑉 ∈ Fin → (𝑉 FriendGrph 𝐸 → (𝑉 ≠ ∅ → ((#‘𝑉) ∈
(ℤ≥‘2) → (¬ (#‘𝑉) = 2 → (¬ (#‘𝑉) = 3 → (〈𝑉, 𝐸〉 RegUSGrph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))))) |
114 | 113 | com14 94 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((#‘𝑉) ∈
(ℤ≥‘2) → (𝑉 FriendGrph 𝐸 → (𝑉 ≠ ∅ → (𝑉 ∈ Fin → (¬ (#‘𝑉) = 2 → (¬
(#‘𝑉) = 3 →
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))))) |
115 | 114 | 3imp 1249 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((#‘𝑉) ∈
(ℤ≥‘2) ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ≠ ∅) → (𝑉 ∈ Fin → (¬ (#‘𝑉) = 2 → (¬
(#‘𝑉) = 3 →
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))) |
116 | 115 | com3r 85 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (¬
(#‘𝑉) = 2 →
(((#‘𝑉) ∈
(ℤ≥‘2) ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ≠ ∅) → (𝑉 ∈ Fin → (¬ (#‘𝑉) = 3 → (〈𝑉, 𝐸〉 RegUSGrph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))) |
117 | 32, 116 | pm2.61i 175 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((#‘𝑉) ∈
(ℤ≥‘2) ∧ 𝑉 FriendGrph 𝐸 ∧ 𝑉 ≠ ∅) → (𝑉 ∈ Fin → (¬ (#‘𝑉) = 3 → (〈𝑉, 𝐸〉 RegUSGrph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))) |
118 | 117 | 3exp 1256 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((#‘𝑉) ∈
(ℤ≥‘2) → (𝑉 FriendGrph 𝐸 → (𝑉 ≠ ∅ → (𝑉 ∈ Fin → (¬ (#‘𝑉) = 3 → (〈𝑉, 𝐸〉 RegUSGrph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))) |
119 | 10, 118 | sylbir 224 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((#‘𝑉) ∈
ℕ ∧ (#‘𝑉)
≠ 1) → (𝑉
FriendGrph 𝐸 → (𝑉 ≠ ∅ → (𝑉 ∈ Fin → (¬
(#‘𝑉) = 3 →
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))) |
120 | 119 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((#‘𝑉) ∈
ℕ → ((#‘𝑉)
≠ 1 → (𝑉 FriendGrph
𝐸 → (𝑉 ≠ ∅ → (𝑉 ∈ Fin → (¬ (#‘𝑉) = 3 → (〈𝑉, 𝐸〉 RegUSGrph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))))) |
121 | 9, 120 | syl5bir 232 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((#‘𝑉) ∈
ℕ → (¬ (#‘𝑉) = 1 → (𝑉 FriendGrph 𝐸 → (𝑉 ≠ ∅ → (𝑉 ∈ Fin → (¬ (#‘𝑉) = 3 → (〈𝑉, 𝐸〉 RegUSGrph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))))) |
122 | 121 | com25 97 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((#‘𝑉) ∈
ℕ → (𝑉 ∈
Fin → (𝑉 FriendGrph
𝐸 → (𝑉 ≠ ∅ → (¬ (#‘𝑉) = 1 → (¬
(#‘𝑉) = 3 →
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))))) |
123 | 8, 122 | sylbir 224 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((#‘𝑉) ∈
ℕ0 ∧ (#‘𝑉) ≠ 0) → (𝑉 ∈ Fin → (𝑉 FriendGrph 𝐸 → (𝑉 ≠ ∅ → (¬ (#‘𝑉) = 1 → (¬
(#‘𝑉) = 3 →
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))))) |
124 | 123 | ex 449 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((#‘𝑉) ∈
ℕ0 → ((#‘𝑉) ≠ 0 → (𝑉 ∈ Fin → (𝑉 FriendGrph 𝐸 → (𝑉 ≠ ∅ → (¬ (#‘𝑉) = 1 → (¬
(#‘𝑉) = 3 →
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))))) |
125 | 124 | com23 84 |
. . . . . . . . . . . . . . . . . . 19
⊢
((#‘𝑉) ∈
ℕ0 → (𝑉 ∈ Fin → ((#‘𝑉) ≠ 0 → (𝑉 FriendGrph 𝐸 → (𝑉 ≠ ∅ → (¬ (#‘𝑉) = 1 → (¬
(#‘𝑉) = 3 →
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))))) |
126 | 125 | impd 446 |
. . . . . . . . . . . . . . . . . 18
⊢
((#‘𝑉) ∈
ℕ0 → ((𝑉 ∈ Fin ∧ (#‘𝑉) ≠ 0) → (𝑉 FriendGrph 𝐸 → (𝑉 ≠ ∅ → (¬ (#‘𝑉) = 1 → (¬
(#‘𝑉) = 3 →
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))))) |
127 | 126 | com14 94 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑉 ≠ ∅ → ((𝑉 ∈ Fin ∧ (#‘𝑉) ≠ 0) → (𝑉 FriendGrph 𝐸 → ((#‘𝑉) ∈ ℕ0 → (¬
(#‘𝑉) = 1 →
(¬ (#‘𝑉) = 3
→ (〈𝑉, 𝐸〉 RegUSGrph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))))) |
128 | 7, 127 | mpcom 37 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑉 ∈ Fin ∧ (#‘𝑉) ≠ 0) → (𝑉 FriendGrph 𝐸 → ((#‘𝑉) ∈ ℕ0 → (¬
(#‘𝑉) = 1 →
(¬ (#‘𝑉) = 3
→ (〈𝑉, 𝐸〉 RegUSGrph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))) |
129 | 128 | ex 449 |
. . . . . . . . . . . . . . 15
⊢ (𝑉 ∈ Fin →
((#‘𝑉) ≠ 0 →
(𝑉 FriendGrph 𝐸 → ((#‘𝑉) ∈ ℕ0
→ (¬ (#‘𝑉) =
1 → (¬ (#‘𝑉)
= 3 → (〈𝑉, 𝐸〉 RegUSGrph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))))) |
130 | 129 | com14 94 |
. . . . . . . . . . . . . 14
⊢
((#‘𝑉) ∈
ℕ0 → ((#‘𝑉) ≠ 0 → (𝑉 FriendGrph 𝐸 → (𝑉 ∈ Fin → (¬ (#‘𝑉) = 1 → (¬
(#‘𝑉) = 3 →
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))))) |
131 | 4, 130 | syl5bir 232 |
. . . . . . . . . . . . 13
⊢
((#‘𝑉) ∈
ℕ0 → (¬ (#‘𝑉) = 0 → (𝑉 FriendGrph 𝐸 → (𝑉 ∈ Fin → (¬ (#‘𝑉) = 1 → (¬
(#‘𝑉) = 3 →
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))))) |
132 | 131 | com24 93 |
. . . . . . . . . . . 12
⊢
((#‘𝑉) ∈
ℕ0 → (𝑉 ∈ Fin → (𝑉 FriendGrph 𝐸 → (¬ (#‘𝑉) = 0 → (¬ (#‘𝑉) = 1 → (¬
(#‘𝑉) = 3 →
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))))) |
133 | 132 | 3imp 1249 |
. . . . . . . . . . 11
⊢
(((#‘𝑉) ∈
ℕ0 ∧ 𝑉
∈ Fin ∧ 𝑉
FriendGrph 𝐸) → (¬
(#‘𝑉) = 0 →
(¬ (#‘𝑉) = 1
→ (¬ (#‘𝑉) =
3 → (〈𝑉, 𝐸〉 RegUSGrph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))) |
134 | 133 | com25 97 |
. . . . . . . . . 10
⊢
(((#‘𝑉) ∈
ℕ0 ∧ 𝑉
∈ Fin ∧ 𝑉
FriendGrph 𝐸) →
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → (¬ (#‘𝑉) = 1 → (¬ (#‘𝑉) = 3 → (¬
(#‘𝑉) = 0 →
((#‘𝑉) = 0 ∨
(#‘𝑉) = 1 ∨
(#‘𝑉) =
3)))))) |
135 | 134 | imp 444 |
. . . . . . . . 9
⊢
((((#‘𝑉)
∈ ℕ0 ∧ 𝑉 ∈ Fin ∧ 𝑉 FriendGrph 𝐸) ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) → (¬ (#‘𝑉) = 1 → (¬ (#‘𝑉) = 3 → (¬
(#‘𝑉) = 0 →
((#‘𝑉) = 0 ∨
(#‘𝑉) = 1 ∨
(#‘𝑉) =
3))))) |
136 | 135 | com14 94 |
. . . . . . . 8
⊢ (¬
(#‘𝑉) = 0 →
(¬ (#‘𝑉) = 1
→ (¬ (#‘𝑉) =
3 → ((((#‘𝑉)
∈ ℕ0 ∧ 𝑉 ∈ Fin ∧ 𝑉 FriendGrph 𝐸) ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))) |
137 | 136 | 3imp 1249 |
. . . . . . 7
⊢ ((¬
(#‘𝑉) = 0 ∧ ¬
(#‘𝑉) = 1 ∧ ¬
(#‘𝑉) = 3) →
((((#‘𝑉) ∈
ℕ0 ∧ 𝑉
∈ Fin ∧ 𝑉
FriendGrph 𝐸) ∧
〈𝑉, 𝐸〉 RegUSGrph 𝐾) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))) |
138 | 3, 137 | sylbi 206 |
. . . . . 6
⊢ (¬
((#‘𝑉) = 0 ∨
(#‘𝑉) = 1 ∨
(#‘𝑉) = 3) →
((((#‘𝑉) ∈
ℕ0 ∧ 𝑉
∈ Fin ∧ 𝑉
FriendGrph 𝐸) ∧
〈𝑉, 𝐸〉 RegUSGrph 𝐾) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))) |
139 | 2, 138 | pm2.61i 175 |
. . . . 5
⊢
((((#‘𝑉)
∈ ℕ0 ∧ 𝑉 ∈ Fin ∧ 𝑉 FriendGrph 𝐸) ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)) |
140 | 139 | 3exp1 1275 |
. . . 4
⊢
((#‘𝑉) ∈
ℕ0 → (𝑉 ∈ Fin → (𝑉 FriendGrph 𝐸 → (〈𝑉, 𝐸〉 RegUSGrph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))) |
141 | 1, 140 | mpcom 37 |
. . 3
⊢ (𝑉 ∈ Fin → (𝑉 FriendGrph 𝐸 → (〈𝑉, 𝐸〉 RegUSGrph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))) |
142 | 141 | com12 32 |
. 2
⊢ (𝑉 FriendGrph 𝐸 → (𝑉 ∈ Fin → (〈𝑉, 𝐸〉 RegUSGrph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))) |
143 | 142 | 3imp 1249 |
1
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)) |