Step | Hyp | Ref
| Expression |
1 | | hashcl 13923 |
. . 3
⊢ (𝑉 ∈ Fin →
(♯‘𝑉) ∈
ℕ0) |
2 | | ax-1 6 |
. . . . 5
⊢
(((♯‘𝑉)
= 0 ∨ (♯‘𝑉)
= 1 ∨ (♯‘𝑉)
= 3) → ((((♯‘𝑉) ∈ ℕ0 ∧ 𝑉 ∈ Fin ∧ 𝐺 ∈ FriendGraph ) ∧
𝐺 RegUSGraph 𝐾) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))) |
3 | | 3ioran 1108 |
. . . . . 6
⊢ (¬
((♯‘𝑉) = 0 ∨
(♯‘𝑉) = 1 ∨
(♯‘𝑉) = 3)
↔ (¬ (♯‘𝑉) = 0 ∧ ¬ (♯‘𝑉) = 1 ∧ ¬
(♯‘𝑉) =
3)) |
4 | | df-ne 2941 |
. . . . . . . . . . . . 13
⊢
((♯‘𝑉)
≠ 0 ↔ ¬ (♯‘𝑉) = 0) |
5 | | hasheq0 13930 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑉 ∈ Fin →
((♯‘𝑉) = 0
↔ 𝑉 =
∅)) |
6 | 5 | necon3bid 2985 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑉 ∈ Fin →
((♯‘𝑉) ≠ 0
↔ 𝑉 ≠
∅)) |
7 | 6 | biimpa 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑉 ∈ Fin ∧
(♯‘𝑉) ≠ 0)
→ 𝑉 ≠
∅) |
8 | | elnnne0 12104 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((♯‘𝑉)
∈ ℕ ↔ ((♯‘𝑉) ∈ ℕ0 ∧
(♯‘𝑉) ≠
0)) |
9 | | df-ne 2941 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((♯‘𝑉)
≠ 1 ↔ ¬ (♯‘𝑉) = 1) |
10 | | eluz2b3 12518 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((♯‘𝑉)
∈ (ℤ≥‘2) ↔ ((♯‘𝑉) ∈ ℕ ∧
(♯‘𝑉) ≠
1)) |
11 | | hash2prde 14036 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑉 ∈ Fin ∧
(♯‘𝑉) = 2)
→ ∃𝑎∃𝑏(𝑎 ≠ 𝑏 ∧ 𝑉 = {𝑎, 𝑏})) |
12 | | vex 3412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ 𝑎 ∈ V |
13 | 12 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑎 ≠ 𝑏 → 𝑎 ∈ V) |
14 | | vex 3412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ 𝑏 ∈ V |
15 | 14 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑎 ≠ 𝑏 → 𝑏 ∈ V) |
16 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑎 ≠ 𝑏 → 𝑎 ≠ 𝑏) |
17 | 13, 15, 16 | 3jca 1130 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑎 ≠ 𝑏 → (𝑎 ∈ V ∧ 𝑏 ∈ V ∧ 𝑎 ≠ 𝑏)) |
18 | | frgrreggt1.v |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ 𝑉 = (Vtx‘𝐺) |
19 | 18 | eqeq1i 2742 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑉 = {𝑎, 𝑏} ↔ (Vtx‘𝐺) = {𝑎, 𝑏}) |
20 | 19 | biimpi 219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑉 = {𝑎, 𝑏} → (Vtx‘𝐺) = {𝑎, 𝑏}) |
21 | | nfrgr2v 28355 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (((𝑎 ∈ V ∧ 𝑏 ∈ V ∧ 𝑎 ≠ 𝑏) ∧ (Vtx‘𝐺) = {𝑎, 𝑏}) → 𝐺 ∉ FriendGraph ) |
22 | 17, 20, 21 | syl2an 599 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑎 ≠ 𝑏 ∧ 𝑉 = {𝑎, 𝑏}) → 𝐺 ∉ FriendGraph ) |
23 | | df-nel 3047 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝐺 ∉ FriendGraph ↔
¬ 𝐺 ∈ FriendGraph
) |
24 | 22, 23 | sylib 221 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑎 ≠ 𝑏 ∧ 𝑉 = {𝑎, 𝑏}) → ¬ 𝐺 ∈ FriendGraph ) |
25 | 24 | pm2.21d 121 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑎 ≠ 𝑏 ∧ 𝑉 = {𝑎, 𝑏}) → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → (¬
(♯‘𝑉) = 3
→ (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))) |
26 | 25 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑎 ≠ 𝑏 ∧ 𝑉 = {𝑎, 𝑏}) → (𝑉 ≠ ∅ → (𝐺 ∈ FriendGraph → (¬
(♯‘𝑉) = 3
→ (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))) |
27 | 26 | exlimivv 1940 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(∃𝑎∃𝑏(𝑎 ≠ 𝑏 ∧ 𝑉 = {𝑎, 𝑏}) → (𝑉 ≠ ∅ → (𝐺 ∈ FriendGraph → (¬
(♯‘𝑉) = 3
→ (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))) |
28 | 11, 27 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑉 ∈ Fin ∧
(♯‘𝑉) = 2)
→ (𝑉 ≠ ∅
→ (𝐺 ∈
FriendGraph → (¬ (♯‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))) |
29 | 28 | ex 416 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑉 ∈ Fin →
((♯‘𝑉) = 2
→ (𝑉 ≠ ∅
→ (𝐺 ∈
FriendGraph → (¬ (♯‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))))) |
30 | 29 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑉 ∈ Fin → (𝑉 ≠ ∅ →
((♯‘𝑉) = 2
→ (𝐺 ∈
FriendGraph → (¬ (♯‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))))) |
31 | 30 | com14 96 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝐺 ∈ FriendGraph →
(𝑉 ≠ ∅ →
((♯‘𝑉) = 2
→ (𝑉 ∈ Fin →
(¬ (♯‘𝑉) =
3 → (𝐺 RegUSGraph
𝐾 →
((♯‘𝑉) = 0 ∨
(♯‘𝑉) = 1 ∨
(♯‘𝑉) =
3))))))) |
32 | 31 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((♯‘𝑉)
∈ (ℤ≥‘2) → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ →
((♯‘𝑉) = 2
→ (𝑉 ∈ Fin →
(¬ (♯‘𝑉) =
3 → (𝐺 RegUSGraph
𝐾 →
((♯‘𝑉) = 0 ∨
(♯‘𝑉) = 1 ∨
(♯‘𝑉) =
3)))))))) |
33 | 32 | 3imp 1113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((♯‘𝑉)
∈ (ℤ≥‘2) ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ≠ ∅) → ((♯‘𝑉) = 2 → (𝑉 ∈ Fin → (¬
(♯‘𝑉) = 3
→ (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))) |
34 | 33 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((♯‘𝑉) =
2 → (((♯‘𝑉) ∈ (ℤ≥‘2)
∧ 𝐺 ∈ FriendGraph
∧ 𝑉 ≠ ∅)
→ (𝑉 ∈ Fin →
(¬ (♯‘𝑉) =
3 → (𝐺 RegUSGraph
𝐾 →
((♯‘𝑉) = 0 ∨
(♯‘𝑉) = 1 ∨
(♯‘𝑉) =
3)))))) |
35 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢
(VtxDeg‘𝐺) =
(VtxDeg‘𝐺) |
36 | 18, 35 | rusgrprop0 27655 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝐺 RegUSGraph 𝐾 → (𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0*
∧ ∀𝑣 ∈
𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾)) |
37 | | eluz2gt1 12516 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
⊢
((♯‘𝑉)
∈ (ℤ≥‘2) → 1 < (♯‘𝑉)) |
38 | 37 | anim1ci 619 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢
(((♯‘𝑉)
∈ (ℤ≥‘2) ∧ 𝐺 ∈ FriendGraph ) → (𝐺 ∈ FriendGraph ∧ 1 <
(♯‘𝑉))) |
39 | 18 | vdgn0frgrv2 28378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑣 ∈ 𝑉) → (1 < (♯‘𝑉) → ((VtxDeg‘𝐺)‘𝑣) ≠ 0)) |
40 | 39 | impancom 455 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
⊢ ((𝐺 ∈ FriendGraph ∧ 1 <
(♯‘𝑉)) →
(𝑣 ∈ 𝑉 → ((VtxDeg‘𝐺)‘𝑣) ≠ 0)) |
41 | 40 | ralrimiv 3104 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ ((𝐺 ∈ FriendGraph ∧ 1 <
(♯‘𝑉)) →
∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) ≠ 0) |
42 | | eqeq2 2749 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . 51
⊢ (𝐾 = 0 →
(((VtxDeg‘𝐺)‘𝑣) = 𝐾 ↔ ((VtxDeg‘𝐺)‘𝑣) = 0)) |
43 | 42 | ralbidv 3118 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
⊢ (𝐾 = 0 → (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 ↔ ∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 0)) |
44 | | r19.26 3092 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . 52
⊢
(∀𝑣 ∈
𝑉 (((VtxDeg‘𝐺)‘𝑣) = 0 ∧ ((VtxDeg‘𝐺)‘𝑣) ≠ 0) ↔ (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 0 ∧ ∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) ≠ 0)) |
45 | | nne 2944 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . 57
⊢ (¬
((VtxDeg‘𝐺)‘𝑣) ≠ 0 ↔ ((VtxDeg‘𝐺)‘𝑣) = 0) |
46 | 45 | bicomi 227 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . 56
⊢
(((VtxDeg‘𝐺)‘𝑣) = 0 ↔ ¬ ((VtxDeg‘𝐺)‘𝑣) ≠ 0) |
47 | 46 | anbi1i 627 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . 55
⊢
((((VtxDeg‘𝐺)‘𝑣) = 0 ∧ ((VtxDeg‘𝐺)‘𝑣) ≠ 0) ↔ (¬ ((VtxDeg‘𝐺)‘𝑣) ≠ 0 ∧ ((VtxDeg‘𝐺)‘𝑣) ≠ 0)) |
48 | | ancom 464 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . 55
⊢ ((¬
((VtxDeg‘𝐺)‘𝑣) ≠ 0 ∧ ((VtxDeg‘𝐺)‘𝑣) ≠ 0) ↔ (((VtxDeg‘𝐺)‘𝑣) ≠ 0 ∧ ¬ ((VtxDeg‘𝐺)‘𝑣) ≠ 0)) |
49 | | pm3.24 406 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . 56
⊢ ¬
(((VtxDeg‘𝐺)‘𝑣) ≠ 0 ∧ ¬ ((VtxDeg‘𝐺)‘𝑣) ≠ 0) |
50 | 49 | bifal 1559 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . 55
⊢
((((VtxDeg‘𝐺)‘𝑣) ≠ 0 ∧ ¬ ((VtxDeg‘𝐺)‘𝑣) ≠ 0) ↔ ⊥) |
51 | 47, 48, 50 | 3bitri 300 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . 54
⊢
((((VtxDeg‘𝐺)‘𝑣) = 0 ∧ ((VtxDeg‘𝐺)‘𝑣) ≠ 0) ↔ ⊥) |
52 | 51 | ralbii 3088 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . 53
⊢
(∀𝑣 ∈
𝑉 (((VtxDeg‘𝐺)‘𝑣) = 0 ∧ ((VtxDeg‘𝐺)‘𝑣) ≠ 0) ↔ ∀𝑣 ∈ 𝑉 ⊥) |
53 | | r19.3rzv 4410 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . 56
⊢ (𝑉 ≠ ∅ → (⊥
↔ ∀𝑣 ∈
𝑉 ⊥)) |
54 | | falim 1560 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . 56
⊢ (⊥
→ ((♯‘𝑉) =
0 ∨ (♯‘𝑉) =
1 ∨ (♯‘𝑉) =
3)) |
55 | 53, 54 | syl6bir 257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . 55
⊢ (𝑉 ≠ ∅ →
(∀𝑣 ∈ 𝑉 ⊥ →
((♯‘𝑉) = 0 ∨
(♯‘𝑉) = 1 ∨
(♯‘𝑉) =
3))) |
56 | 55 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . 54
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) →
(∀𝑣 ∈ 𝑉 ⊥ →
((♯‘𝑉) = 0 ∨
(♯‘𝑉) = 1 ∨
(♯‘𝑉) =
3))) |
57 | 56 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . 53
⊢
(∀𝑣 ∈
𝑉 ⊥ → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) →
((♯‘𝑉) = 0 ∨
(♯‘𝑉) = 1 ∨
(♯‘𝑉) =
3))) |
58 | 52, 57 | sylbi 220 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . 52
⊢
(∀𝑣 ∈
𝑉 (((VtxDeg‘𝐺)‘𝑣) = 0 ∧ ((VtxDeg‘𝐺)‘𝑣) ≠ 0) → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))) |
59 | 44, 58 | sylbir 238 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . 51
⊢
((∀𝑣 ∈
𝑉 ((VtxDeg‘𝐺)‘𝑣) = 0 ∧ ∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) ≠ 0) → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))) |
60 | 59 | ex 416 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
⊢
(∀𝑣 ∈
𝑉 ((VtxDeg‘𝐺)‘𝑣) = 0 → (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) ≠ 0 → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))) |
61 | 43, 60 | syl6bi 256 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
⊢ (𝐾 = 0 → (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) ≠ 0 → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))) |
62 | 61 | com4t 93 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢
(∀𝑣 ∈
𝑉 ((VtxDeg‘𝐺)‘𝑣) ≠ 0 → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))) |
63 | 38, 41, 62 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢
(((♯‘𝑉)
∈ (ℤ≥‘2) ∧ 𝐺 ∈ FriendGraph ) → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))) |
64 | 63 | ex 416 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢
((♯‘𝑉)
∈ (ℤ≥‘2) → (𝐺 ∈ FriendGraph → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))) |
65 | 64 | com25 99 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢
((♯‘𝑉)
∈ (ℤ≥‘2) → (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (𝐺 ∈ FriendGraph →
((♯‘𝑉) = 0 ∨
(♯‘𝑉) = 1 ∨
(♯‘𝑉) =
3)))))) |
66 | 65 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (((¬
(♯‘𝑉) = 3 ∧
¬ (♯‘𝑉) =
2) ∧ (♯‘𝑉)
∈ (ℤ≥‘2)) → (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (𝐺 ∈ FriendGraph →
((♯‘𝑉) = 0 ∨
(♯‘𝑉) = 1 ∨
(♯‘𝑉) =
3)))))) |
67 | 66 | com15 101 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (𝐺 ∈ FriendGraph →
(∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (((¬ (♯‘𝑉) = 3 ∧ ¬
(♯‘𝑉) = 2)
∧ (♯‘𝑉)
∈ (ℤ≥‘2)) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))) |
68 | 67 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢
(∀𝑣 ∈
𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → (𝐺 ∈ FriendGraph → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (((¬
(♯‘𝑉) = 3 ∧
¬ (♯‘𝑉) =
2) ∧ (♯‘𝑉)
∈ (ℤ≥‘2)) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))) |
69 | 68 | 3ad2ant3 1137 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝐺 ∈ USGraph ∧ 𝐾 ∈
ℕ0* ∧ ∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → (𝐺 ∈ FriendGraph → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (((¬
(♯‘𝑉) = 3 ∧
¬ (♯‘𝑉) =
2) ∧ (♯‘𝑉)
∈ (ℤ≥‘2)) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))) |
70 | 36, 69 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝐺 RegUSGraph 𝐾 → (𝐺 ∈ FriendGraph → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (((¬
(♯‘𝑉) = 3 ∧
¬ (♯‘𝑉) =
2) ∧ (♯‘𝑉)
∈ (ℤ≥‘2)) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))) |
71 | 70 | impcom 411 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾) → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (((¬ (♯‘𝑉) = 3 ∧ ¬
(♯‘𝑉) = 2)
∧ (♯‘𝑉)
∈ (ℤ≥‘2)) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))) |
72 | 71 | impcom 411 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) → (𝐾 = 0 → (((¬ (♯‘𝑉) = 3 ∧ ¬
(♯‘𝑉) = 2)
∧ (♯‘𝑉)
∈ (ℤ≥‘2)) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))) |
73 | 18 | frrusgrord 28424 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾) → (♯‘𝑉) = ((𝐾 · (𝐾 − 1)) + 1))) |
74 | 73 | imp 410 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) → (♯‘𝑉) = ((𝐾 · (𝐾 − 1)) + 1)) |
75 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (𝐾 = 2 → 𝐾 = 2) |
76 | | oveq1 7220 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (𝐾 = 2 → (𝐾 − 1) = (2 −
1)) |
77 | 75, 76 | oveq12d 7231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (𝐾 = 2 → (𝐾 · (𝐾 − 1)) = (2 · (2 −
1))) |
78 | 77 | oveq1d 7228 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝐾 = 2 → ((𝐾 · (𝐾 − 1)) + 1) = ((2 · (2 −
1)) + 1)) |
79 | | 2m1e1 11956 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ (2
− 1) = 1 |
80 | 79 | oveq2i 7224 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (2
· (2 − 1)) = (2 · 1) |
81 | | 2t1e2 11993 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (2
· 1) = 2 |
82 | 80, 81 | eqtri 2765 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (2
· (2 − 1)) = 2 |
83 | 82 | oveq1i 7223 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((2
· (2 − 1)) + 1) = (2 + 1) |
84 | | 2p1e3 11972 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (2 + 1) =
3 |
85 | 83, 84 | eqtri 2765 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((2
· (2 − 1)) + 1) = 3 |
86 | 78, 85 | eqtrdi 2794 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝐾 = 2 → ((𝐾 · (𝐾 − 1)) + 1) = 3) |
87 | 86 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝐾 = 2 →
((♯‘𝑉) =
((𝐾 · (𝐾 − 1)) + 1) ↔
(♯‘𝑉) =
3)) |
88 | | pm2.21 123 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (¬
(♯‘𝑉) = 3
→ ((♯‘𝑉) =
3 → ((♯‘𝑉)
= 0 ∨ (♯‘𝑉)
= 1 ∨ (♯‘𝑉)
= 3))) |
89 | 88 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (((¬
(♯‘𝑉) = 3 ∧
¬ (♯‘𝑉) =
2) ∧ (♯‘𝑉)
∈ (ℤ≥‘2)) → ((♯‘𝑉) = 3 →
((♯‘𝑉) = 0 ∨
(♯‘𝑉) = 1 ∨
(♯‘𝑉) =
3))) |
90 | 89 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢
((♯‘𝑉) =
3 → (((¬ (♯‘𝑉) = 3 ∧ ¬ (♯‘𝑉) = 2) ∧
(♯‘𝑉) ∈
(ℤ≥‘2)) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))) |
91 | 87, 90 | syl6bi 256 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝐾 = 2 →
((♯‘𝑉) =
((𝐾 · (𝐾 − 1)) + 1) →
(((¬ (♯‘𝑉)
= 3 ∧ ¬ (♯‘𝑉) = 2) ∧ (♯‘𝑉) ∈
(ℤ≥‘2)) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))) |
92 | 74, 91 | syl5com 31 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) → (𝐾 = 2 → (((¬ (♯‘𝑉) = 3 ∧ ¬
(♯‘𝑉) = 2)
∧ (♯‘𝑉)
∈ (ℤ≥‘2)) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))) |
93 | 18 | frgrreg 28477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾) → (𝐾 = 0 ∨ 𝐾 = 2))) |
94 | 93 | imp 410 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) → (𝐾 = 0 ∨ 𝐾 = 2)) |
95 | 72, 92, 94 | mpjaod 860 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) → (((¬ (♯‘𝑉) = 3 ∧ ¬
(♯‘𝑉) = 2)
∧ (♯‘𝑉)
∈ (ℤ≥‘2)) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))) |
96 | 95 | exp32 424 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐺 ∈ FriendGraph →
(𝐺 RegUSGraph 𝐾 → (((¬
(♯‘𝑉) = 3 ∧
¬ (♯‘𝑉) =
2) ∧ (♯‘𝑉)
∈ (ℤ≥‘2)) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))) |
97 | 96 | com34 91 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐺 ∈ FriendGraph →
(((¬ (♯‘𝑉)
= 3 ∧ ¬ (♯‘𝑉) = 2) ∧ (♯‘𝑉) ∈
(ℤ≥‘2)) → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))) |
98 | 97 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (((¬
(♯‘𝑉) = 3 ∧
¬ (♯‘𝑉) =
2) ∧ (♯‘𝑉)
∈ (ℤ≥‘2)) → (𝐺 ∈ FriendGraph → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))) |
99 | 98 | exp4c 436 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (¬
(♯‘𝑉) = 3
→ (¬ (♯‘𝑉) = 2 → ((♯‘𝑉) ∈
(ℤ≥‘2) → (𝐺 ∈ FriendGraph → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))))) |
100 | 99 | com34 91 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (¬
(♯‘𝑉) = 3
→ ((♯‘𝑉)
∈ (ℤ≥‘2) → (¬ (♯‘𝑉) = 2 → (𝐺 ∈ FriendGraph → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))))) |
101 | 100 | com25 99 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐺 ∈ FriendGraph →
((♯‘𝑉) ∈
(ℤ≥‘2) → (¬ (♯‘𝑉) = 2 → (¬ (♯‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))))) |
102 | 101 | ex 416 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑉 ∈ Fin → (𝑉 ≠ ∅ → (𝐺 ∈ FriendGraph →
((♯‘𝑉) ∈
(ℤ≥‘2) → (¬ (♯‘𝑉) = 2 → (¬ (♯‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))))) |
103 | 102 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑉 ∈ Fin → (𝐺 ∈ FriendGraph →
(𝑉 ≠ ∅ →
((♯‘𝑉) ∈
(ℤ≥‘2) → (¬ (♯‘𝑉) = 2 → (¬ (♯‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))))) |
104 | 103 | com14 96 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((♯‘𝑉)
∈ (ℤ≥‘2) → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → (𝑉 ∈ Fin → (¬
(♯‘𝑉) = 2
→ (¬ (♯‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))))) |
105 | 104 | 3imp 1113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((♯‘𝑉)
∈ (ℤ≥‘2) ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ≠ ∅) → (𝑉 ∈ Fin → (¬
(♯‘𝑉) = 2
→ (¬ (♯‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))) |
106 | 105 | com3r 87 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (¬
(♯‘𝑉) = 2
→ (((♯‘𝑉)
∈ (ℤ≥‘2) ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ≠ ∅) → (𝑉 ∈ Fin → (¬
(♯‘𝑉) = 3
→ (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))) |
107 | 34, 106 | pm2.61i 185 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((♯‘𝑉)
∈ (ℤ≥‘2) ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ≠ ∅) → (𝑉 ∈ Fin → (¬
(♯‘𝑉) = 3
→ (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))) |
108 | 107 | 3exp 1121 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((♯‘𝑉)
∈ (ℤ≥‘2) → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → (𝑉 ∈ Fin → (¬
(♯‘𝑉) = 3
→ (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))))) |
109 | 10, 108 | sylbir 238 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((♯‘𝑉)
∈ ℕ ∧ (♯‘𝑉) ≠ 1) → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → (𝑉 ∈ Fin → (¬
(♯‘𝑉) = 3
→ (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))))) |
110 | 109 | ex 416 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((♯‘𝑉)
∈ ℕ → ((♯‘𝑉) ≠ 1 → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → (𝑉 ∈ Fin → (¬
(♯‘𝑉) = 3
→ (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))))) |
111 | 9, 110 | syl5bir 246 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((♯‘𝑉)
∈ ℕ → (¬ (♯‘𝑉) = 1 → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → (𝑉 ∈ Fin → (¬
(♯‘𝑉) = 3
→ (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))))) |
112 | 111 | com25 99 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((♯‘𝑉)
∈ ℕ → (𝑉
∈ Fin → (𝐺 ∈
FriendGraph → (𝑉 ≠
∅ → (¬ (♯‘𝑉) = 1 → (¬ (♯‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))))) |
113 | 8, 112 | sylbir 238 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((♯‘𝑉)
∈ ℕ0 ∧ (♯‘𝑉) ≠ 0) → (𝑉 ∈ Fin → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → (¬
(♯‘𝑉) = 1
→ (¬ (♯‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))))) |
114 | 113 | ex 416 |
. . . . . . . . . . . . . . . . . 18
⊢
((♯‘𝑉)
∈ ℕ0 → ((♯‘𝑉) ≠ 0 → (𝑉 ∈ Fin → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → (¬
(♯‘𝑉) = 1
→ (¬ (♯‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))))))) |
115 | 114 | impcomd 415 |
. . . . . . . . . . . . . . . . 17
⊢
((♯‘𝑉)
∈ ℕ0 → ((𝑉 ∈ Fin ∧ (♯‘𝑉) ≠ 0) → (𝐺 ∈ FriendGraph →
(𝑉 ≠ ∅ →
(¬ (♯‘𝑉) =
1 → (¬ (♯‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))))) |
116 | 115 | com14 96 |
. . . . . . . . . . . . . . . 16
⊢ (𝑉 ≠ ∅ → ((𝑉 ∈ Fin ∧
(♯‘𝑉) ≠ 0)
→ (𝐺 ∈
FriendGraph → ((♯‘𝑉) ∈ ℕ0 → (¬
(♯‘𝑉) = 1
→ (¬ (♯‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))))) |
117 | 7, 116 | mpcom 38 |
. . . . . . . . . . . . . . 15
⊢ ((𝑉 ∈ Fin ∧
(♯‘𝑉) ≠ 0)
→ (𝐺 ∈
FriendGraph → ((♯‘𝑉) ∈ ℕ0 → (¬
(♯‘𝑉) = 1
→ (¬ (♯‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))))) |
118 | 117 | ex 416 |
. . . . . . . . . . . . . 14
⊢ (𝑉 ∈ Fin →
((♯‘𝑉) ≠ 0
→ (𝐺 ∈
FriendGraph → ((♯‘𝑉) ∈ ℕ0 → (¬
(♯‘𝑉) = 1
→ (¬ (♯‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))))) |
119 | 118 | com14 96 |
. . . . . . . . . . . . 13
⊢
((♯‘𝑉)
∈ ℕ0 → ((♯‘𝑉) ≠ 0 → (𝐺 ∈ FriendGraph → (𝑉 ∈ Fin → (¬
(♯‘𝑉) = 1
→ (¬ (♯‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))))) |
120 | 4, 119 | syl5bir 246 |
. . . . . . . . . . . 12
⊢
((♯‘𝑉)
∈ ℕ0 → (¬ (♯‘𝑉) = 0 → (𝐺 ∈ FriendGraph → (𝑉 ∈ Fin → (¬
(♯‘𝑉) = 1
→ (¬ (♯‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))))) |
121 | 120 | com24 95 |
. . . . . . . . . . 11
⊢
((♯‘𝑉)
∈ ℕ0 → (𝑉 ∈ Fin → (𝐺 ∈ FriendGraph → (¬
(♯‘𝑉) = 0
→ (¬ (♯‘𝑉) = 1 → (¬ (♯‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))))) |
122 | 121 | 3imp 1113 |
. . . . . . . . . 10
⊢
(((♯‘𝑉)
∈ ℕ0 ∧ 𝑉 ∈ Fin ∧ 𝐺 ∈ FriendGraph ) → (¬
(♯‘𝑉) = 0
→ (¬ (♯‘𝑉) = 1 → (¬ (♯‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))) |
123 | 122 | com25 99 |
. . . . . . . . 9
⊢
(((♯‘𝑉)
∈ ℕ0 ∧ 𝑉 ∈ Fin ∧ 𝐺 ∈ FriendGraph ) → (𝐺 RegUSGraph 𝐾 → (¬ (♯‘𝑉) = 1 → (¬
(♯‘𝑉) = 3
→ (¬ (♯‘𝑉) = 0 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))) |
124 | 123 | imp 410 |
. . . . . . . 8
⊢
((((♯‘𝑉)
∈ ℕ0 ∧ 𝑉 ∈ Fin ∧ 𝐺 ∈ FriendGraph ) ∧ 𝐺 RegUSGraph 𝐾) → (¬ (♯‘𝑉) = 1 → (¬
(♯‘𝑉) = 3
→ (¬ (♯‘𝑉) = 0 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))) |
125 | 124 | com14 96 |
. . . . . . 7
⊢ (¬
(♯‘𝑉) = 0
→ (¬ (♯‘𝑉) = 1 → (¬ (♯‘𝑉) = 3 →
((((♯‘𝑉) ∈
ℕ0 ∧ 𝑉
∈ Fin ∧ 𝐺 ∈
FriendGraph ) ∧ 𝐺
RegUSGraph 𝐾) →
((♯‘𝑉) = 0 ∨
(♯‘𝑉) = 1 ∨
(♯‘𝑉) =
3))))) |
126 | 125 | 3imp 1113 |
. . . . . 6
⊢ ((¬
(♯‘𝑉) = 0 ∧
¬ (♯‘𝑉) = 1
∧ ¬ (♯‘𝑉) = 3) → ((((♯‘𝑉) ∈ ℕ0
∧ 𝑉 ∈ Fin ∧
𝐺 ∈ FriendGraph )
∧ 𝐺 RegUSGraph 𝐾) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))) |
127 | 3, 126 | sylbi 220 |
. . . . 5
⊢ (¬
((♯‘𝑉) = 0 ∨
(♯‘𝑉) = 1 ∨
(♯‘𝑉) = 3)
→ ((((♯‘𝑉)
∈ ℕ0 ∧ 𝑉 ∈ Fin ∧ 𝐺 ∈ FriendGraph ) ∧ 𝐺 RegUSGraph 𝐾) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))) |
128 | 2, 127 | pm2.61i 185 |
. . . 4
⊢
((((♯‘𝑉)
∈ ℕ0 ∧ 𝑉 ∈ Fin ∧ 𝐺 ∈ FriendGraph ) ∧ 𝐺 RegUSGraph 𝐾) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)) |
129 | 128 | 3exp1 1354 |
. . 3
⊢
((♯‘𝑉)
∈ ℕ0 → (𝑉 ∈ Fin → (𝐺 ∈ FriendGraph → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))) |
130 | 1, 129 | mpcom 38 |
. 2
⊢ (𝑉 ∈ Fin → (𝐺 ∈ FriendGraph →
(𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))) |
131 | 130 | 3imp21 1116 |
1
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)) |