Step | Hyp | Ref
| Expression |
1 | | hashcl 13310 |
. . 3
⊢ (𝑉 ∈ Fin →
(♯‘𝑉) ∈
ℕ0) |
2 | | ax-1 6 |
. . . . 5
⊢
(((♯‘𝑉)
= 0 ∨ (♯‘𝑉)
= 1 ∨ (♯‘𝑉)
= 3) → ((((♯‘𝑉) ∈ ℕ0 ∧ 𝑉 ∈ Fin ∧ 𝐺 ∈ FriendGraph ) ∧
𝐺RegUSGraph𝐾) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))) |
3 | | 3ioran 1095 |
. . . . . 6
⊢ (¬
((♯‘𝑉) = 0 ∨
(♯‘𝑉) = 1 ∨
(♯‘𝑉) = 3)
↔ (¬ (♯‘𝑉) = 0 ∧ ¬ (♯‘𝑉) = 1 ∧ ¬
(♯‘𝑉) =
3)) |
4 | | df-ne 2921 |
. . . . . . . . . . . . 13
⊢
((♯‘𝑉)
≠ 0 ↔ ¬ (♯‘𝑉) = 0) |
5 | | hasheq0 13317 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑉 ∈ Fin →
((♯‘𝑉) = 0
↔ 𝑉 =
∅)) |
6 | 5 | necon3bid 2964 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑉 ∈ Fin →
((♯‘𝑉) ≠ 0
↔ 𝑉 ≠
∅)) |
7 | 6 | biimpa 502 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑉 ∈ Fin ∧
(♯‘𝑉) ≠ 0)
→ 𝑉 ≠
∅) |
8 | | elnnne0 11469 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((♯‘𝑉)
∈ ℕ ↔ ((♯‘𝑉) ∈ ℕ0 ∧
(♯‘𝑉) ≠
0)) |
9 | | df-ne 2921 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((♯‘𝑉)
≠ 1 ↔ ¬ (♯‘𝑉) = 1) |
10 | | eluz2b3 11926 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((♯‘𝑉)
∈ (ℤ≥‘2) ↔ ((♯‘𝑉) ∈ ℕ ∧
(♯‘𝑉) ≠
1)) |
11 | | hash2prde 13415 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑉 ∈ Fin ∧
(♯‘𝑉) = 2)
→ ∃𝑎∃𝑏(𝑎 ≠ 𝑏 ∧ 𝑉 = {𝑎, 𝑏})) |
12 | | vex 3331 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ 𝑎 ∈ V |
13 | 12 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑎 ≠ 𝑏 → 𝑎 ∈ V) |
14 | | vex 3331 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ 𝑏 ∈ V |
15 | 14 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑎 ≠ 𝑏 → 𝑏 ∈ V) |
16 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑎 ≠ 𝑏 → 𝑎 ≠ 𝑏) |
17 | 13, 15, 16 | 3jca 1403 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑎 ≠ 𝑏 → (𝑎 ∈ V ∧ 𝑏 ∈ V ∧ 𝑎 ≠ 𝑏)) |
18 | | frgrreggt1.v |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ 𝑉 = (Vtx‘𝐺) |
19 | 18 | eqeq1i 2753 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑉 = {𝑎, 𝑏} ↔ (Vtx‘𝐺) = {𝑎, 𝑏}) |
20 | 19 | biimpi 206 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑉 = {𝑎, 𝑏} → (Vtx‘𝐺) = {𝑎, 𝑏}) |
21 | | nfrgr2v 27397 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (((𝑎 ∈ V ∧ 𝑏 ∈ V ∧ 𝑎 ≠ 𝑏) ∧ (Vtx‘𝐺) = {𝑎, 𝑏}) → 𝐺 ∉ FriendGraph ) |
22 | 17, 20, 21 | syl2an 495 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑎 ≠ 𝑏 ∧ 𝑉 = {𝑎, 𝑏}) → 𝐺 ∉ FriendGraph ) |
23 | | df-nel 3024 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝐺 ∉ FriendGraph ↔
¬ 𝐺 ∈ FriendGraph
) |
24 | 22, 23 | sylib 208 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑎 ≠ 𝑏 ∧ 𝑉 = {𝑎, 𝑏}) → ¬ 𝐺 ∈ FriendGraph ) |
25 | 24 | pm2.21d 118 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑎 ≠ 𝑏 ∧ 𝑉 = {𝑎, 𝑏}) → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → (¬
(♯‘𝑉) = 3
→ (𝐺RegUSGraph𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))) |
26 | 25 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑎 ≠ 𝑏 ∧ 𝑉 = {𝑎, 𝑏}) → (𝑉 ≠ ∅ → (𝐺 ∈ FriendGraph → (¬
(♯‘𝑉) = 3
→ (𝐺RegUSGraph𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))) |
27 | 26 | exlimivv 1997 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
(∃𝑎∃𝑏(𝑎 ≠ 𝑏 ∧ 𝑉 = {𝑎, 𝑏}) → (𝑉 ≠ ∅ → (𝐺 ∈ FriendGraph → (¬
(♯‘𝑉) = 3
→ (𝐺RegUSGraph𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))) |
28 | 11, 27 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑉 ∈ Fin ∧
(♯‘𝑉) = 2)
→ (𝑉 ≠ ∅
→ (𝐺 ∈
FriendGraph → (¬ (♯‘𝑉) = 3 → (𝐺RegUSGraph𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))) |
29 | 28 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑉 ∈ Fin →
((♯‘𝑉) = 2
→ (𝑉 ≠ ∅
→ (𝐺 ∈
FriendGraph → (¬ (♯‘𝑉) = 3 → (𝐺RegUSGraph𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))))) |
30 | 29 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑉 ∈ Fin → (𝑉 ≠ ∅ →
((♯‘𝑉) = 2
→ (𝐺 ∈
FriendGraph → (¬ (♯‘𝑉) = 3 → (𝐺RegUSGraph𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))))) |
31 | 30 | com14 96 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝐺 ∈ FriendGraph →
(𝑉 ≠ ∅ →
((♯‘𝑉) = 2
→ (𝑉 ∈ Fin →
(¬ (♯‘𝑉) =
3 → (𝐺RegUSGraph𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))))) |
32 | 31 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((♯‘𝑉)
∈ (ℤ≥‘2) → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ →
((♯‘𝑉) = 2
→ (𝑉 ∈ Fin →
(¬ (♯‘𝑉) =
3 → (𝐺RegUSGraph𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))))) |
33 | 32 | 3imp 1101 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((♯‘𝑉)
∈ (ℤ≥‘2) ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ≠ ∅) → ((♯‘𝑉) = 2 → (𝑉 ∈ Fin → (¬
(♯‘𝑉) = 3
→ (𝐺RegUSGraph𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))) |
34 | 33 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((♯‘𝑉) =
2 → (((♯‘𝑉) ∈ (ℤ≥‘2)
∧ 𝐺 ∈ FriendGraph
∧ 𝑉 ≠ ∅)
→ (𝑉 ∈ Fin →
(¬ (♯‘𝑉) =
3 → (𝐺RegUSGraph𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))) |
35 | | eqid 2748 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢
(VtxDeg‘𝐺) =
(VtxDeg‘𝐺) |
36 | 18, 35 | rusgrprop0 26644 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝐺RegUSGraph𝐾 → (𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0*
∧ ∀𝑣 ∈
𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾)) |
37 | | eluz2gt1 11924 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . 51
⊢
((♯‘𝑉)
∈ (ℤ≥‘2) → 1 < (♯‘𝑉)) |
38 | 37 | anim2i 594 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
⊢ ((𝐺 ∈ FriendGraph ∧
(♯‘𝑉) ∈
(ℤ≥‘2)) → (𝐺 ∈ FriendGraph ∧ 1 <
(♯‘𝑉))) |
39 | 38 | ancoms 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
⊢
(((♯‘𝑉)
∈ (ℤ≥‘2) ∧ 𝐺 ∈ FriendGraph ) → (𝐺 ∈ FriendGraph ∧ 1 <
(♯‘𝑉))) |
40 | 18 | vdgn0frgrv2 27420 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . 51
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑣 ∈ 𝑉) → (1 < (♯‘𝑉) → ((VtxDeg‘𝐺)‘𝑣) ≠ 0)) |
41 | 40 | impancom 455 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
⊢ ((𝐺 ∈ FriendGraph ∧ 1 <
(♯‘𝑉)) →
(𝑣 ∈ 𝑉 → ((VtxDeg‘𝐺)‘𝑣) ≠ 0)) |
42 | 41 | ralrimiv 3091 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
⊢ ((𝐺 ∈ FriendGraph ∧ 1 <
(♯‘𝑉)) →
∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) ≠ 0) |
43 | | eqeq2 2759 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . 52
⊢ (𝐾 = 0 →
(((VtxDeg‘𝐺)‘𝑣) = 𝐾 ↔ ((VtxDeg‘𝐺)‘𝑣) = 0)) |
44 | 43 | ralbidv 3112 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . 51
⊢ (𝐾 = 0 → (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 ↔ ∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 0)) |
45 | | r19.26 3190 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . 53
⊢
(∀𝑣 ∈
𝑉 (((VtxDeg‘𝐺)‘𝑣) = 0 ∧ ((VtxDeg‘𝐺)‘𝑣) ≠ 0) ↔ (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 0 ∧ ∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) ≠ 0)) |
46 | | nne 2924 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . 58
⊢ (¬
((VtxDeg‘𝐺)‘𝑣) ≠ 0 ↔ ((VtxDeg‘𝐺)‘𝑣) = 0) |
47 | 46 | bicomi 214 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . 57
⊢
(((VtxDeg‘𝐺)‘𝑣) = 0 ↔ ¬ ((VtxDeg‘𝐺)‘𝑣) ≠ 0) |
48 | 47 | anbi1i 733 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . 56
⊢
((((VtxDeg‘𝐺)‘𝑣) = 0 ∧ ((VtxDeg‘𝐺)‘𝑣) ≠ 0) ↔ (¬ ((VtxDeg‘𝐺)‘𝑣) ≠ 0 ∧ ((VtxDeg‘𝐺)‘𝑣) ≠ 0)) |
49 | | ancom 465 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . 56
⊢ ((¬
((VtxDeg‘𝐺)‘𝑣) ≠ 0 ∧ ((VtxDeg‘𝐺)‘𝑣) ≠ 0) ↔ (((VtxDeg‘𝐺)‘𝑣) ≠ 0 ∧ ¬ ((VtxDeg‘𝐺)‘𝑣) ≠ 0)) |
50 | | pm3.24 962 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . 57
⊢ ¬
(((VtxDeg‘𝐺)‘𝑣) ≠ 0 ∧ ¬ ((VtxDeg‘𝐺)‘𝑣) ≠ 0) |
51 | 50 | bifal 1634 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . 56
⊢
((((VtxDeg‘𝐺)‘𝑣) ≠ 0 ∧ ¬ ((VtxDeg‘𝐺)‘𝑣) ≠ 0) ↔ ⊥) |
52 | 48, 49, 51 | 3bitri 286 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . 55
⊢
((((VtxDeg‘𝐺)‘𝑣) = 0 ∧ ((VtxDeg‘𝐺)‘𝑣) ≠ 0) ↔ ⊥) |
53 | 52 | ralbii 3106 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . 54
⊢
(∀𝑣 ∈
𝑉 (((VtxDeg‘𝐺)‘𝑣) = 0 ∧ ((VtxDeg‘𝐺)‘𝑣) ≠ 0) ↔ ∀𝑣 ∈ 𝑉 ⊥) |
54 | | r19.3rzv 4196 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . 57
⊢ (𝑉 ≠ ∅ → (⊥
↔ ∀𝑣 ∈
𝑉 ⊥)) |
55 | | falim 1635 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . 57
⊢ (⊥
→ ((♯‘𝑉) =
0 ∨ (♯‘𝑉) =
1 ∨ (♯‘𝑉) =
3)) |
56 | 54, 55 | syl6bir 244 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . 56
⊢ (𝑉 ≠ ∅ →
(∀𝑣 ∈ 𝑉 ⊥ →
((♯‘𝑉) = 0 ∨
(♯‘𝑉) = 1 ∨
(♯‘𝑉) =
3))) |
57 | 56 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . 55
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) →
(∀𝑣 ∈ 𝑉 ⊥ →
((♯‘𝑉) = 0 ∨
(♯‘𝑉) = 1 ∨
(♯‘𝑉) =
3))) |
58 | 57 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . 54
⊢
(∀𝑣 ∈
𝑉 ⊥ → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) →
((♯‘𝑉) = 0 ∨
(♯‘𝑉) = 1 ∨
(♯‘𝑉) =
3))) |
59 | 53, 58 | sylbi 207 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . 53
⊢
(∀𝑣 ∈
𝑉 (((VtxDeg‘𝐺)‘𝑣) = 0 ∧ ((VtxDeg‘𝐺)‘𝑣) ≠ 0) → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))) |
60 | 45, 59 | sylbir 225 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . 52
⊢
((∀𝑣 ∈
𝑉 ((VtxDeg‘𝐺)‘𝑣) = 0 ∧ ∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) ≠ 0) → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))) |
61 | 60 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . 51
⊢
(∀𝑣 ∈
𝑉 ((VtxDeg‘𝐺)‘𝑣) = 0 → (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) ≠ 0 → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))) |
62 | 44, 61 | syl6bi 243 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
⊢ (𝐾 = 0 → (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) ≠ 0 → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))) |
63 | 62 | com4t 93 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
⊢
(∀𝑣 ∈
𝑉 ((VtxDeg‘𝐺)‘𝑣) ≠ 0 → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))) |
64 | 39, 42, 63 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢
(((♯‘𝑉)
∈ (ℤ≥‘2) ∧ 𝐺 ∈ FriendGraph ) → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))) |
65 | 64 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢
((♯‘𝑉)
∈ (ℤ≥‘2) → (𝐺 ∈ FriendGraph → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))) |
66 | 65 | com25 99 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢
((♯‘𝑉)
∈ (ℤ≥‘2) → (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (𝐺 ∈ FriendGraph →
((♯‘𝑉) = 0 ∨
(♯‘𝑉) = 1 ∨
(♯‘𝑉) =
3)))))) |
67 | 66 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (((¬
(♯‘𝑉) = 3 ∧
¬ (♯‘𝑉) =
2) ∧ (♯‘𝑉)
∈ (ℤ≥‘2)) → (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (𝐺 ∈ FriendGraph →
((♯‘𝑉) = 0 ∨
(♯‘𝑉) = 1 ∨
(♯‘𝑉) =
3)))))) |
68 | 67 | com15 101 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (𝐺 ∈ FriendGraph →
(∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (((¬ (♯‘𝑉) = 3 ∧ ¬
(♯‘𝑉) = 2)
∧ (♯‘𝑉)
∈ (ℤ≥‘2)) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))) |
69 | 68 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢
(∀𝑣 ∈
𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → (𝐺 ∈ FriendGraph → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (((¬
(♯‘𝑉) = 3 ∧
¬ (♯‘𝑉) =
2) ∧ (♯‘𝑉)
∈ (ℤ≥‘2)) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))) |
70 | 69 | 3ad2ant3 1127 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((𝐺 ∈ USGraph ∧ 𝐾 ∈
ℕ0* ∧ ∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → (𝐺 ∈ FriendGraph → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (((¬
(♯‘𝑉) = 3 ∧
¬ (♯‘𝑉) =
2) ∧ (♯‘𝑉)
∈ (ℤ≥‘2)) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))) |
71 | 36, 70 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝐺RegUSGraph𝐾 → (𝐺 ∈ FriendGraph → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (((¬
(♯‘𝑉) = 3 ∧
¬ (♯‘𝑉) =
2) ∧ (♯‘𝑉)
∈ (ℤ≥‘2)) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))) |
72 | 71 | impcom 445 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝐺 ∈ FriendGraph ∧ 𝐺RegUSGraph𝐾) → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (((¬ (♯‘𝑉) = 3 ∧ ¬
(♯‘𝑉) = 2)
∧ (♯‘𝑉)
∈ (ℤ≥‘2)) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))) |
73 | 72 | impcom 445 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺RegUSGraph𝐾)) → (𝐾 = 0 → (((¬ (♯‘𝑉) = 3 ∧ ¬
(♯‘𝑉) = 2)
∧ (♯‘𝑉)
∈ (ℤ≥‘2)) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))) |
74 | 18 | frrusgrord 27466 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((𝐺 ∈ FriendGraph ∧ 𝐺RegUSGraph𝐾) → (♯‘𝑉) = ((𝐾 · (𝐾 − 1)) + 1))) |
75 | 74 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺RegUSGraph𝐾)) → (♯‘𝑉) = ((𝐾 · (𝐾 − 1)) + 1)) |
76 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (𝐾 = 2 → 𝐾 = 2) |
77 | | oveq1 6808 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (𝐾 = 2 → (𝐾 − 1) = (2 −
1)) |
78 | 76, 77 | oveq12d 6819 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (𝐾 = 2 → (𝐾 · (𝐾 − 1)) = (2 · (2 −
1))) |
79 | 78 | oveq1d 6816 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (𝐾 = 2 → ((𝐾 · (𝐾 − 1)) + 1) = ((2 · (2 −
1)) + 1)) |
80 | | 2m1e1 11298 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ (2
− 1) = 1 |
81 | 80 | oveq2i 6812 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ (2
· (2 − 1)) = (2 · 1) |
82 | | 2t1e2 11339 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ (2
· 1) = 2 |
83 | 81, 82 | eqtri 2770 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (2
· (2 − 1)) = 2 |
84 | 83 | oveq1i 6811 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ ((2
· (2 − 1)) + 1) = (2 + 1) |
85 | | 2p1e3 11314 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (2 + 1) =
3 |
86 | 84, 85 | eqtri 2770 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((2
· (2 − 1)) + 1) = 3 |
87 | 79, 86 | syl6eq 2798 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝐾 = 2 → ((𝐾 · (𝐾 − 1)) + 1) = 3) |
88 | 87 | eqeq2d 2758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝐾 = 2 →
((♯‘𝑉) =
((𝐾 · (𝐾 − 1)) + 1) ↔
(♯‘𝑉) =
3)) |
89 | | pm2.21 120 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (¬
(♯‘𝑉) = 3
→ ((♯‘𝑉) =
3 → ((♯‘𝑉)
= 0 ∨ (♯‘𝑉)
= 1 ∨ (♯‘𝑉)
= 3))) |
90 | 89 | ad2antrr 764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (((¬
(♯‘𝑉) = 3 ∧
¬ (♯‘𝑉) =
2) ∧ (♯‘𝑉)
∈ (ℤ≥‘2)) → ((♯‘𝑉) = 3 →
((♯‘𝑉) = 0 ∨
(♯‘𝑉) = 1 ∨
(♯‘𝑉) =
3))) |
91 | 90 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢
((♯‘𝑉) =
3 → (((¬ (♯‘𝑉) = 3 ∧ ¬ (♯‘𝑉) = 2) ∧
(♯‘𝑉) ∈
(ℤ≥‘2)) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))) |
92 | 88, 91 | syl6bi 243 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝐾 = 2 →
((♯‘𝑉) =
((𝐾 · (𝐾 − 1)) + 1) →
(((¬ (♯‘𝑉)
= 3 ∧ ¬ (♯‘𝑉) = 2) ∧ (♯‘𝑉) ∈
(ℤ≥‘2)) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))) |
93 | 75, 92 | syl5com 31 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺RegUSGraph𝐾)) → (𝐾 = 2 → (((¬ (♯‘𝑉) = 3 ∧ ¬
(♯‘𝑉) = 2)
∧ (♯‘𝑉)
∈ (ℤ≥‘2)) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))) |
94 | 18 | frgrreg 27533 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((𝐺 ∈ FriendGraph ∧ 𝐺RegUSGraph𝐾) → (𝐾 = 0 ∨ 𝐾 = 2))) |
95 | 94 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺RegUSGraph𝐾)) → (𝐾 = 0 ∨ 𝐾 = 2)) |
96 | 73, 93, 95 | mpjaod 395 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺RegUSGraph𝐾)) → (((¬ (♯‘𝑉) = 3 ∧ ¬
(♯‘𝑉) = 2)
∧ (♯‘𝑉)
∈ (ℤ≥‘2)) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))) |
97 | 96 | exp32 632 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐺 ∈ FriendGraph →
(𝐺RegUSGraph𝐾 → (((¬
(♯‘𝑉) = 3 ∧
¬ (♯‘𝑉) =
2) ∧ (♯‘𝑉)
∈ (ℤ≥‘2)) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))) |
98 | 97 | com34 91 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐺 ∈ FriendGraph →
(((¬ (♯‘𝑉)
= 3 ∧ ¬ (♯‘𝑉) = 2) ∧ (♯‘𝑉) ∈
(ℤ≥‘2)) → (𝐺RegUSGraph𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))) |
99 | 98 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (((¬
(♯‘𝑉) = 3 ∧
¬ (♯‘𝑉) =
2) ∧ (♯‘𝑉)
∈ (ℤ≥‘2)) → (𝐺 ∈ FriendGraph → (𝐺RegUSGraph𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))) |
100 | 99 | exp4c 637 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (¬
(♯‘𝑉) = 3
→ (¬ (♯‘𝑉) = 2 → ((♯‘𝑉) ∈
(ℤ≥‘2) → (𝐺 ∈ FriendGraph → (𝐺RegUSGraph𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))))) |
101 | 100 | com34 91 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (¬
(♯‘𝑉) = 3
→ ((♯‘𝑉)
∈ (ℤ≥‘2) → (¬ (♯‘𝑉) = 2 → (𝐺 ∈ FriendGraph → (𝐺RegUSGraph𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))))) |
102 | 101 | com25 99 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐺 ∈ FriendGraph →
((♯‘𝑉) ∈
(ℤ≥‘2) → (¬ (♯‘𝑉) = 2 → (¬ (♯‘𝑉) = 3 → (𝐺RegUSGraph𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))))) |
103 | 102 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑉 ∈ Fin → (𝑉 ≠ ∅ → (𝐺 ∈ FriendGraph →
((♯‘𝑉) ∈
(ℤ≥‘2) → (¬ (♯‘𝑉) = 2 → (¬ (♯‘𝑉) = 3 → (𝐺RegUSGraph𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))))) |
104 | 103 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑉 ∈ Fin → (𝐺 ∈ FriendGraph →
(𝑉 ≠ ∅ →
((♯‘𝑉) ∈
(ℤ≥‘2) → (¬ (♯‘𝑉) = 2 → (¬ (♯‘𝑉) = 3 → (𝐺RegUSGraph𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))))) |
105 | 104 | com14 96 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((♯‘𝑉)
∈ (ℤ≥‘2) → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → (𝑉 ∈ Fin → (¬
(♯‘𝑉) = 2
→ (¬ (♯‘𝑉) = 3 → (𝐺RegUSGraph𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))))) |
106 | 105 | 3imp 1101 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((♯‘𝑉)
∈ (ℤ≥‘2) ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ≠ ∅) → (𝑉 ∈ Fin → (¬
(♯‘𝑉) = 2
→ (¬ (♯‘𝑉) = 3 → (𝐺RegUSGraph𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))) |
107 | 106 | com3r 87 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (¬
(♯‘𝑉) = 2
→ (((♯‘𝑉)
∈ (ℤ≥‘2) ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ≠ ∅) → (𝑉 ∈ Fin → (¬
(♯‘𝑉) = 3
→ (𝐺RegUSGraph𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))) |
108 | 34, 107 | pm2.61i 176 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((♯‘𝑉)
∈ (ℤ≥‘2) ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ≠ ∅) → (𝑉 ∈ Fin → (¬
(♯‘𝑉) = 3
→ (𝐺RegUSGraph𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))) |
109 | 108 | 3exp 1112 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((♯‘𝑉)
∈ (ℤ≥‘2) → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → (𝑉 ∈ Fin → (¬
(♯‘𝑉) = 3
→ (𝐺RegUSGraph𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))))) |
110 | 10, 109 | sylbir 225 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((♯‘𝑉)
∈ ℕ ∧ (♯‘𝑉) ≠ 1) → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → (𝑉 ∈ Fin → (¬
(♯‘𝑉) = 3
→ (𝐺RegUSGraph𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))))) |
111 | 110 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((♯‘𝑉)
∈ ℕ → ((♯‘𝑉) ≠ 1 → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → (𝑉 ∈ Fin → (¬
(♯‘𝑉) = 3
→ (𝐺RegUSGraph𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))))) |
112 | 9, 111 | syl5bir 233 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((♯‘𝑉)
∈ ℕ → (¬ (♯‘𝑉) = 1 → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → (𝑉 ∈ Fin → (¬
(♯‘𝑉) = 3
→ (𝐺RegUSGraph𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))))) |
113 | 112 | com25 99 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((♯‘𝑉)
∈ ℕ → (𝑉
∈ Fin → (𝐺 ∈
FriendGraph → (𝑉 ≠
∅ → (¬ (♯‘𝑉) = 1 → (¬ (♯‘𝑉) = 3 → (𝐺RegUSGraph𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))))) |
114 | 8, 113 | sylbir 225 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((♯‘𝑉)
∈ ℕ0 ∧ (♯‘𝑉) ≠ 0) → (𝑉 ∈ Fin → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → (¬
(♯‘𝑉) = 1
→ (¬ (♯‘𝑉) = 3 → (𝐺RegUSGraph𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))))) |
115 | 114 | ex 449 |
. . . . . . . . . . . . . . . . . . 19
⊢
((♯‘𝑉)
∈ ℕ0 → ((♯‘𝑉) ≠ 0 → (𝑉 ∈ Fin → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → (¬
(♯‘𝑉) = 1
→ (¬ (♯‘𝑉) = 3 → (𝐺RegUSGraph𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))))))) |
116 | 115 | com23 86 |
. . . . . . . . . . . . . . . . . 18
⊢
((♯‘𝑉)
∈ ℕ0 → (𝑉 ∈ Fin → ((♯‘𝑉) ≠ 0 → (𝐺 ∈ FriendGraph →
(𝑉 ≠ ∅ →
(¬ (♯‘𝑉) =
1 → (¬ (♯‘𝑉) = 3 → (𝐺RegUSGraph𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))))))) |
117 | 116 | impd 446 |
. . . . . . . . . . . . . . . . 17
⊢
((♯‘𝑉)
∈ ℕ0 → ((𝑉 ∈ Fin ∧ (♯‘𝑉) ≠ 0) → (𝐺 ∈ FriendGraph →
(𝑉 ≠ ∅ →
(¬ (♯‘𝑉) =
1 → (¬ (♯‘𝑉) = 3 → (𝐺RegUSGraph𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))))) |
118 | 117 | com14 96 |
. . . . . . . . . . . . . . . 16
⊢ (𝑉 ≠ ∅ → ((𝑉 ∈ Fin ∧
(♯‘𝑉) ≠ 0)
→ (𝐺 ∈
FriendGraph → ((♯‘𝑉) ∈ ℕ0 → (¬
(♯‘𝑉) = 1
→ (¬ (♯‘𝑉) = 3 → (𝐺RegUSGraph𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))))) |
119 | 7, 118 | mpcom 38 |
. . . . . . . . . . . . . . 15
⊢ ((𝑉 ∈ Fin ∧
(♯‘𝑉) ≠ 0)
→ (𝐺 ∈
FriendGraph → ((♯‘𝑉) ∈ ℕ0 → (¬
(♯‘𝑉) = 1
→ (¬ (♯‘𝑉) = 3 → (𝐺RegUSGraph𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))))) |
120 | 119 | ex 449 |
. . . . . . . . . . . . . 14
⊢ (𝑉 ∈ Fin →
((♯‘𝑉) ≠ 0
→ (𝐺 ∈
FriendGraph → ((♯‘𝑉) ∈ ℕ0 → (¬
(♯‘𝑉) = 1
→ (¬ (♯‘𝑉) = 3 → (𝐺RegUSGraph𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))))) |
121 | 120 | com14 96 |
. . . . . . . . . . . . 13
⊢
((♯‘𝑉)
∈ ℕ0 → ((♯‘𝑉) ≠ 0 → (𝐺 ∈ FriendGraph → (𝑉 ∈ Fin → (¬
(♯‘𝑉) = 1
→ (¬ (♯‘𝑉) = 3 → (𝐺RegUSGraph𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))))) |
122 | 4, 121 | syl5bir 233 |
. . . . . . . . . . . 12
⊢
((♯‘𝑉)
∈ ℕ0 → (¬ (♯‘𝑉) = 0 → (𝐺 ∈ FriendGraph → (𝑉 ∈ Fin → (¬
(♯‘𝑉) = 1
→ (¬ (♯‘𝑉) = 3 → (𝐺RegUSGraph𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))))) |
123 | 122 | com24 95 |
. . . . . . . . . . 11
⊢
((♯‘𝑉)
∈ ℕ0 → (𝑉 ∈ Fin → (𝐺 ∈ FriendGraph → (¬
(♯‘𝑉) = 0
→ (¬ (♯‘𝑉) = 1 → (¬ (♯‘𝑉) = 3 → (𝐺RegUSGraph𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))))) |
124 | 123 | 3imp 1101 |
. . . . . . . . . 10
⊢
(((♯‘𝑉)
∈ ℕ0 ∧ 𝑉 ∈ Fin ∧ 𝐺 ∈ FriendGraph ) → (¬
(♯‘𝑉) = 0
→ (¬ (♯‘𝑉) = 1 → (¬ (♯‘𝑉) = 3 → (𝐺RegUSGraph𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))) |
125 | 124 | com25 99 |
. . . . . . . . 9
⊢
(((♯‘𝑉)
∈ ℕ0 ∧ 𝑉 ∈ Fin ∧ 𝐺 ∈ FriendGraph ) → (𝐺RegUSGraph𝐾 → (¬ (♯‘𝑉) = 1 → (¬
(♯‘𝑉) = 3
→ (¬ (♯‘𝑉) = 0 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))) |
126 | 125 | imp 444 |
. . . . . . . 8
⊢
((((♯‘𝑉)
∈ ℕ0 ∧ 𝑉 ∈ Fin ∧ 𝐺 ∈ FriendGraph ) ∧ 𝐺RegUSGraph𝐾) → (¬ (♯‘𝑉) = 1 → (¬
(♯‘𝑉) = 3
→ (¬ (♯‘𝑉) = 0 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))) |
127 | 126 | com14 96 |
. . . . . . 7
⊢ (¬
(♯‘𝑉) = 0
→ (¬ (♯‘𝑉) = 1 → (¬ (♯‘𝑉) = 3 →
((((♯‘𝑉) ∈
ℕ0 ∧ 𝑉
∈ Fin ∧ 𝐺 ∈
FriendGraph ) ∧ 𝐺RegUSGraph𝐾) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))) |
128 | 127 | 3imp 1101 |
. . . . . 6
⊢ ((¬
(♯‘𝑉) = 0 ∧
¬ (♯‘𝑉) = 1
∧ ¬ (♯‘𝑉) = 3) → ((((♯‘𝑉) ∈ ℕ0
∧ 𝑉 ∈ Fin ∧
𝐺 ∈ FriendGraph )
∧ 𝐺RegUSGraph𝐾) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))) |
129 | 3, 128 | sylbi 207 |
. . . . 5
⊢ (¬
((♯‘𝑉) = 0 ∨
(♯‘𝑉) = 1 ∨
(♯‘𝑉) = 3)
→ ((((♯‘𝑉)
∈ ℕ0 ∧ 𝑉 ∈ Fin ∧ 𝐺 ∈ FriendGraph ) ∧ 𝐺RegUSGraph𝐾) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))) |
130 | 2, 129 | pm2.61i 176 |
. . . 4
⊢
((((♯‘𝑉)
∈ ℕ0 ∧ 𝑉 ∈ Fin ∧ 𝐺 ∈ FriendGraph ) ∧ 𝐺RegUSGraph𝐾) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)) |
131 | 130 | 3exp1 1431 |
. . 3
⊢
((♯‘𝑉)
∈ ℕ0 → (𝑉 ∈ Fin → (𝐺 ∈ FriendGraph → (𝐺RegUSGraph𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))) |
132 | 1, 131 | mpcom 38 |
. 2
⊢ (𝑉 ∈ Fin → (𝐺 ∈ FriendGraph →
(𝐺RegUSGraph𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))) |
133 | 132 | 3imp21 1105 |
1
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝐺RegUSGraph𝐾) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)) |