| Step | Hyp | Ref
| Expression |
| 1 | | hashcl 14395 |
. . 3
⊢ (𝑉 ∈ Fin →
(♯‘𝑉) ∈
ℕ0) |
| 2 | | ax-1 6 |
. . . . 5
⊢
(((♯‘𝑉)
= 0 ∨ (♯‘𝑉)
= 1 ∨ (♯‘𝑉)
= 3) → ((((♯‘𝑉) ∈ ℕ0 ∧ 𝑉 ∈ Fin ∧ 𝐺 ∈ FriendGraph ) ∧
𝐺 RegUSGraph 𝐾) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))) |
| 3 | | 3ioran 1106 |
. . . . . 6
⊢ (¬
((♯‘𝑉) = 0 ∨
(♯‘𝑉) = 1 ∨
(♯‘𝑉) = 3)
↔ (¬ (♯‘𝑉) = 0 ∧ ¬ (♯‘𝑉) = 1 ∧ ¬
(♯‘𝑉) =
3)) |
| 4 | | df-ne 2941 |
. . . . . . . . . . . . 13
⊢
((♯‘𝑉)
≠ 0 ↔ ¬ (♯‘𝑉) = 0) |
| 5 | | hasheq0 14402 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑉 ∈ Fin →
((♯‘𝑉) = 0
↔ 𝑉 =
∅)) |
| 6 | 5 | necon3bid 2985 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑉 ∈ Fin →
((♯‘𝑉) ≠ 0
↔ 𝑉 ≠
∅)) |
| 7 | 6 | biimpa 476 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑉 ∈ Fin ∧
(♯‘𝑉) ≠ 0)
→ 𝑉 ≠
∅) |
| 8 | | elnnne0 12540 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((♯‘𝑉)
∈ ℕ ↔ ((♯‘𝑉) ∈ ℕ0 ∧
(♯‘𝑉) ≠
0)) |
| 9 | | df-ne 2941 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((♯‘𝑉)
≠ 1 ↔ ¬ (♯‘𝑉) = 1) |
| 10 | | eluz2b3 12964 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((♯‘𝑉)
∈ (ℤ≥‘2) ↔ ((♯‘𝑉) ∈ ℕ ∧
(♯‘𝑉) ≠
1)) |
| 11 | | hash2prde 14509 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑉 ∈ Fin ∧
(♯‘𝑉) = 2)
→ ∃𝑎∃𝑏(𝑎 ≠ 𝑏 ∧ 𝑉 = {𝑎, 𝑏})) |
| 12 | | vex 3484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ 𝑎 ∈ V |
| 13 | 12 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑎 ≠ 𝑏 → 𝑎 ∈ V) |
| 14 | | vex 3484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ 𝑏 ∈ V |
| 15 | 14 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑎 ≠ 𝑏 → 𝑏 ∈ V) |
| 16 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑎 ≠ 𝑏 → 𝑎 ≠ 𝑏) |
| 17 | 13, 15, 16 | 3jca 1129 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑎 ≠ 𝑏 → (𝑎 ∈ V ∧ 𝑏 ∈ V ∧ 𝑎 ≠ 𝑏)) |
| 18 | | frgrreggt1.v |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ 𝑉 = (Vtx‘𝐺) |
| 19 | 18 | eqeq1i 2742 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑉 = {𝑎, 𝑏} ↔ (Vtx‘𝐺) = {𝑎, 𝑏}) |
| 20 | 19 | biimpi 216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑉 = {𝑎, 𝑏} → (Vtx‘𝐺) = {𝑎, 𝑏}) |
| 21 | | nfrgr2v 30291 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (((𝑎 ∈ V ∧ 𝑏 ∈ V ∧ 𝑎 ≠ 𝑏) ∧ (Vtx‘𝐺) = {𝑎, 𝑏}) → 𝐺 ∉ FriendGraph ) |
| 22 | 17, 20, 21 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑎 ≠ 𝑏 ∧ 𝑉 = {𝑎, 𝑏}) → 𝐺 ∉ FriendGraph ) |
| 23 | | df-nel 3047 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝐺 ∉ FriendGraph ↔
¬ 𝐺 ∈ FriendGraph
) |
| 24 | 22, 23 | sylib 218 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 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 1932 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(∃𝑎∃𝑏(𝑎 ≠ 𝑏 ∧ 𝑉 = {𝑎, 𝑏}) → (𝑉 ≠ ∅ → (𝐺 ∈ FriendGraph → (¬
(♯‘𝑉) = 3
→ (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))) |
| 28 | 11, 27 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑉 ∈ Fin ∧
(♯‘𝑉) = 2)
→ (𝑉 ≠ ∅
→ (𝐺 ∈
FriendGraph → (¬ (♯‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))) |
| 29 | 28 | ex 412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
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 1111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 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 29585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝐺 RegUSGraph 𝐾 → (𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0*
∧ ∀𝑣 ∈
𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾)) |
| 37 | | eluz2gt1 12962 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
⊢
((♯‘𝑉)
∈ (ℤ≥‘2) → 1 < (♯‘𝑉)) |
| 38 | 37 | anim1ci 616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢
(((♯‘𝑉)
∈ (ℤ≥‘2) ∧ 𝐺 ∈ FriendGraph ) → (𝐺 ∈ FriendGraph ∧ 1 <
(♯‘𝑉))) |
| 39 | 18 | vdgn0frgrv2 30314 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑣 ∈ 𝑉) → (1 < (♯‘𝑉) → ((VtxDeg‘𝐺)‘𝑣) ≠ 0)) |
| 40 | 39 | impancom 451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
⊢ ((𝐺 ∈ FriendGraph ∧ 1 <
(♯‘𝑉)) →
(𝑣 ∈ 𝑉 → ((VtxDeg‘𝐺)‘𝑣) ≠ 0)) |
| 41 | 40 | ralrimiv 3145 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ ((𝐺 ∈ FriendGraph ∧ 1 <
(♯‘𝑉)) →
∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) ≠ 0) |
| 42 | | eqeq2 2749 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . 51
⊢ (𝐾 = 0 →
(((VtxDeg‘𝐺)‘𝑣) = 𝐾 ↔ ((VtxDeg‘𝐺)‘𝑣) = 0)) |
| 43 | 42 | ralbidv 3178 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
⊢ (𝐾 = 0 → (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 ↔ ∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 0)) |
| 44 | | r19.26 3111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . 52
⊢
(∀𝑣 ∈
𝑉 (((VtxDeg‘𝐺)‘𝑣) = 0 ∧ ((VtxDeg‘𝐺)‘𝑣) ≠ 0) ↔ (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 0 ∧ ∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) ≠ 0)) |
| 45 | | nne 2944 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . 57
⊢ (¬
((VtxDeg‘𝐺)‘𝑣) ≠ 0 ↔ ((VtxDeg‘𝐺)‘𝑣) = 0) |
| 46 | 45 | bicomi 224 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . 56
⊢
(((VtxDeg‘𝐺)‘𝑣) = 0 ↔ ¬ ((VtxDeg‘𝐺)‘𝑣) ≠ 0) |
| 47 | 46 | anbi1i 624 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . 55
⊢
((((VtxDeg‘𝐺)‘𝑣) = 0 ∧ ((VtxDeg‘𝐺)‘𝑣) ≠ 0) ↔ (¬ ((VtxDeg‘𝐺)‘𝑣) ≠ 0 ∧ ((VtxDeg‘𝐺)‘𝑣) ≠ 0)) |
| 48 | | ancom 460 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . 55
⊢ ((¬
((VtxDeg‘𝐺)‘𝑣) ≠ 0 ∧ ((VtxDeg‘𝐺)‘𝑣) ≠ 0) ↔ (((VtxDeg‘𝐺)‘𝑣) ≠ 0 ∧ ¬ ((VtxDeg‘𝐺)‘𝑣) ≠ 0)) |
| 49 | | pm3.24 402 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . 56
⊢ ¬
(((VtxDeg‘𝐺)‘𝑣) ≠ 0 ∧ ¬ ((VtxDeg‘𝐺)‘𝑣) ≠ 0) |
| 50 | 49 | bifal 1556 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . 55
⊢
((((VtxDeg‘𝐺)‘𝑣) ≠ 0 ∧ ¬ ((VtxDeg‘𝐺)‘𝑣) ≠ 0) ↔ ⊥) |
| 51 | 47, 48, 50 | 3bitri 297 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . 54
⊢
((((VtxDeg‘𝐺)‘𝑣) = 0 ∧ ((VtxDeg‘𝐺)‘𝑣) ≠ 0) ↔ ⊥) |
| 52 | 51 | ralbii 3093 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . 53
⊢
(∀𝑣 ∈
𝑉 (((VtxDeg‘𝐺)‘𝑣) = 0 ∧ ((VtxDeg‘𝐺)‘𝑣) ≠ 0) ↔ ∀𝑣 ∈ 𝑉 ⊥) |
| 53 | | r19.3rzv 4499 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . 56
⊢ (𝑉 ≠ ∅ → (⊥
↔ ∀𝑣 ∈
𝑉 ⊥)) |
| 54 | | falim 1557 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . 56
⊢ (⊥
→ ((♯‘𝑉) =
0 ∨ (♯‘𝑉) =
1 ∨ (♯‘𝑉) =
3)) |
| 55 | 53, 54 | biimtrrdi 254 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . 55
⊢ (𝑉 ≠ ∅ →
(∀𝑣 ∈ 𝑉 ⊥ →
((♯‘𝑉) = 0 ∨
(♯‘𝑉) = 1 ∨
(♯‘𝑉) =
3))) |
| 56 | 55 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . 54
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) →
(∀𝑣 ∈ 𝑉 ⊥ →
((♯‘𝑉) = 0 ∨
(♯‘𝑉) = 1 ∨
(♯‘𝑉) =
3))) |
| 57 | 56 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . 53
⊢
(∀𝑣 ∈
𝑉 ⊥ → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) →
((♯‘𝑉) = 0 ∨
(♯‘𝑉) = 1 ∨
(♯‘𝑉) =
3))) |
| 58 | 52, 57 | sylbi 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . 52
⊢
(∀𝑣 ∈
𝑉 (((VtxDeg‘𝐺)‘𝑣) = 0 ∧ ((VtxDeg‘𝐺)‘𝑣) ≠ 0) → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))) |
| 59 | 44, 58 | sylbir 235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . 51
⊢
((∀𝑣 ∈
𝑉 ((VtxDeg‘𝐺)‘𝑣) = 0 ∧ ∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) ≠ 0) → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))) |
| 60 | 59 | ex 412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
⊢
(∀𝑣 ∈
𝑉 ((VtxDeg‘𝐺)‘𝑣) = 0 → (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) ≠ 0 → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))) |
| 61 | 43, 60 | biimtrdi 253 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 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 412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 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 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 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 1136 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 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 407 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾) → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (((¬ (♯‘𝑉) = 3 ∧ ¬
(♯‘𝑉) = 2)
∧ (♯‘𝑉)
∈ (ℤ≥‘2)) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))) |
| 72 | 71 | impcom 407 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) → (𝐾 = 0 → (((¬ (♯‘𝑉) = 3 ∧ ¬
(♯‘𝑉) = 2)
∧ (♯‘𝑉)
∈ (ℤ≥‘2)) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))) |
| 73 | 18 | frrusgrord 30360 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾) → (♯‘𝑉) = ((𝐾 · (𝐾 − 1)) + 1))) |
| 74 | 73 | imp 406 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) → (♯‘𝑉) = ((𝐾 · (𝐾 − 1)) + 1)) |
| 75 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (𝐾 = 2 → 𝐾 = 2) |
| 76 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (𝐾 = 2 → (𝐾 − 1) = (2 −
1)) |
| 77 | 75, 76 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (𝐾 = 2 → (𝐾 · (𝐾 − 1)) = (2 · (2 −
1))) |
| 78 | 77 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝐾 = 2 → ((𝐾 · (𝐾 − 1)) + 1) = ((2 · (2 −
1)) + 1)) |
| 79 | | 2m1e1 12392 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ (2
− 1) = 1 |
| 80 | 79 | oveq2i 7442 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (2
· (2 − 1)) = (2 · 1) |
| 81 | | 2t1e2 12429 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (2
· 1) = 2 |
| 82 | 80, 81 | eqtri 2765 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (2
· (2 − 1)) = 2 |
| 83 | 82 | oveq1i 7441 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((2
· (2 − 1)) + 1) = (2 + 1) |
| 84 | | 2p1e3 12408 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (2 + 1) =
3 |
| 85 | 83, 84 | eqtri 2765 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((2
· (2 − 1)) + 1) = 3 |
| 86 | 78, 85 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 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 | biimtrdi 253 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 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 30413 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾) → (𝐾 = 0 ∨ 𝐾 = 2))) |
| 94 | 93 | imp 406 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) → (𝐾 = 0 ∨ 𝐾 = 2)) |
| 95 | 72, 92, 94 | mpjaod 861 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) → (((¬ (♯‘𝑉) = 3 ∧ ¬
(♯‘𝑉) = 2)
∧ (♯‘𝑉)
∈ (ℤ≥‘2)) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))) |
| 96 | 95 | exp32 420 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 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 432 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
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 412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
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 1111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 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 182 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((♯‘𝑉)
∈ (ℤ≥‘2) ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ≠ ∅) → (𝑉 ∈ Fin → (¬
(♯‘𝑉) = 3
→ (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))) |
| 108 | 107 | 3exp 1120 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((♯‘𝑉)
∈ (ℤ≥‘2) → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → (𝑉 ∈ Fin → (¬
(♯‘𝑉) = 3
→ (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))))) |
| 109 | 10, 108 | sylbir 235 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((♯‘𝑉)
∈ ℕ ∧ (♯‘𝑉) ≠ 1) → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → (𝑉 ∈ Fin → (¬
(♯‘𝑉) = 3
→ (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))))) |
| 110 | 109 | ex 412 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((♯‘𝑉)
∈ ℕ → ((♯‘𝑉) ≠ 1 → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → (𝑉 ∈ Fin → (¬
(♯‘𝑉) = 3
→ (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))))) |
| 111 | 9, 110 | biimtrrid 243 |
. . . . . . . . . . . . . . . . . . . . 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 235 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((♯‘𝑉)
∈ ℕ0 ∧ (♯‘𝑉) ≠ 0) → (𝑉 ∈ Fin → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → (¬
(♯‘𝑉) = 1
→ (¬ (♯‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))))) |
| 114 | 113 | ex 412 |
. . . . . . . . . . . . . . . . . 18
⊢
((♯‘𝑉)
∈ ℕ0 → ((♯‘𝑉) ≠ 0 → (𝑉 ∈ Fin → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → (¬
(♯‘𝑉) = 1
→ (¬ (♯‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))))))) |
| 115 | 114 | impcomd 411 |
. . . . . . . . . . . . . . . . 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 412 |
. . . . . . . . . . . . . 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 | biimtrrid 243 |
. . . . . . . . . . . 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 1111 |
. . . . . . . . . 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 406 |
. . . . . . . 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 1111 |
. . . . . 6
⊢ ((¬
(♯‘𝑉) = 0 ∧
¬ (♯‘𝑉) = 1
∧ ¬ (♯‘𝑉) = 3) → ((((♯‘𝑉) ∈ ℕ0
∧ 𝑉 ∈ Fin ∧
𝐺 ∈ FriendGraph )
∧ 𝐺 RegUSGraph 𝐾) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))) |
| 127 | 3, 126 | sylbi 217 |
. . . . 5
⊢ (¬
((♯‘𝑉) = 0 ∨
(♯‘𝑉) = 1 ∨
(♯‘𝑉) = 3)
→ ((((♯‘𝑉)
∈ ℕ0 ∧ 𝑉 ∈ Fin ∧ 𝐺 ∈ FriendGraph ) ∧ 𝐺 RegUSGraph 𝐾) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))) |
| 128 | 2, 127 | pm2.61i 182 |
. . . 4
⊢
((((♯‘𝑉)
∈ ℕ0 ∧ 𝑉 ∈ Fin ∧ 𝐺 ∈ FriendGraph ) ∧ 𝐺 RegUSGraph 𝐾) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)) |
| 129 | 128 | 3exp1 1353 |
. . 3
⊢
((♯‘𝑉)
∈ ℕ0 → (𝑉 ∈ Fin → (𝐺 ∈ FriendGraph → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))) |
| 130 | 1, 129 | mpcom 38 |
. 2
⊢ (𝑉 ∈ Fin → (𝐺 ∈ FriendGraph →
(𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))) |
| 131 | 130 | 3imp21 1114 |
1
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)) |