Proof of Theorem cusgrsize2inds
Step | Hyp | Ref
| Expression |
1 | | cusgrsizeindb0.v |
. . . . 5
⊢ 𝑉 = (Vtx‘𝐺) |
2 | | fvex 6362 |
. . . . 5
⊢
(Vtx‘𝐺) ∈
V |
3 | 1, 2 | eqeltri 2835 |
. . . 4
⊢ 𝑉 ∈ V |
4 | | hashnn0n0nn 13372 |
. . . . . . . 8
⊢ (((𝑉 ∈ V ∧ 𝑌 ∈ ℕ0)
∧ ((♯‘𝑉) =
𝑌 ∧ 𝑁 ∈ 𝑉)) → 𝑌 ∈ ℕ) |
5 | 4 | anassrs 683 |
. . . . . . 7
⊢ ((((𝑉 ∈ V ∧ 𝑌 ∈ ℕ0)
∧ (♯‘𝑉) =
𝑌) ∧ 𝑁 ∈ 𝑉) → 𝑌 ∈ ℕ) |
6 | | simplll 815 |
. . . . . . . . . . 11
⊢ ((((𝑉 ∈ V ∧
(♯‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) ∧ 𝑌 ∈ ℕ) → 𝑉 ∈ V) |
7 | | simplr 809 |
. . . . . . . . . . 11
⊢ ((((𝑉 ∈ V ∧
(♯‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) ∧ 𝑌 ∈ ℕ) → 𝑁 ∈ 𝑉) |
8 | | eleq1 2827 |
. . . . . . . . . . . . . . 15
⊢ (𝑌 = (♯‘𝑉) → (𝑌 ∈ ℕ ↔ (♯‘𝑉) ∈
ℕ)) |
9 | 8 | eqcoms 2768 |
. . . . . . . . . . . . . 14
⊢
((♯‘𝑉) =
𝑌 → (𝑌 ∈ ℕ ↔ (♯‘𝑉) ∈
ℕ)) |
10 | | nnm1nn0 11526 |
. . . . . . . . . . . . . 14
⊢
((♯‘𝑉)
∈ ℕ → ((♯‘𝑉) − 1) ∈
ℕ0) |
11 | 9, 10 | syl6bi 243 |
. . . . . . . . . . . . 13
⊢
((♯‘𝑉) =
𝑌 → (𝑌 ∈ ℕ → ((♯‘𝑉) − 1) ∈
ℕ0)) |
12 | 11 | ad2antlr 765 |
. . . . . . . . . . . 12
⊢ (((𝑉 ∈ V ∧
(♯‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) → (𝑌 ∈ ℕ → ((♯‘𝑉) − 1) ∈
ℕ0)) |
13 | 12 | imp 444 |
. . . . . . . . . . 11
⊢ ((((𝑉 ∈ V ∧
(♯‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) ∧ 𝑌 ∈ ℕ) →
((♯‘𝑉) −
1) ∈ ℕ0) |
14 | | nncn 11220 |
. . . . . . . . . . . . . . . 16
⊢
((♯‘𝑉)
∈ ℕ → (♯‘𝑉) ∈ ℂ) |
15 | | 1cnd 10248 |
. . . . . . . . . . . . . . . 16
⊢
((♯‘𝑉)
∈ ℕ → 1 ∈ ℂ) |
16 | 14, 15 | npcand 10588 |
. . . . . . . . . . . . . . 15
⊢
((♯‘𝑉)
∈ ℕ → (((♯‘𝑉) − 1) + 1) = (♯‘𝑉)) |
17 | 16 | eqcomd 2766 |
. . . . . . . . . . . . . 14
⊢
((♯‘𝑉)
∈ ℕ → (♯‘𝑉) = (((♯‘𝑉) − 1) + 1)) |
18 | 9, 17 | syl6bi 243 |
. . . . . . . . . . . . 13
⊢
((♯‘𝑉) =
𝑌 → (𝑌 ∈ ℕ → (♯‘𝑉) = (((♯‘𝑉) − 1) +
1))) |
19 | 18 | ad2antlr 765 |
. . . . . . . . . . . 12
⊢ (((𝑉 ∈ V ∧
(♯‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) → (𝑌 ∈ ℕ → (♯‘𝑉) = (((♯‘𝑉) − 1) +
1))) |
20 | 19 | imp 444 |
. . . . . . . . . . 11
⊢ ((((𝑉 ∈ V ∧
(♯‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) ∧ 𝑌 ∈ ℕ) → (♯‘𝑉) = (((♯‘𝑉) − 1) +
1)) |
21 | | brfi1indlem 13470 |
. . . . . . . . . . . 12
⊢ ((𝑉 ∈ V ∧ 𝑁 ∈ 𝑉 ∧ ((♯‘𝑉) − 1) ∈ ℕ0)
→ ((♯‘𝑉) =
(((♯‘𝑉) −
1) + 1) → (♯‘(𝑉 ∖ {𝑁})) = ((♯‘𝑉) − 1))) |
22 | 21 | imp 444 |
. . . . . . . . . . 11
⊢ (((𝑉 ∈ V ∧ 𝑁 ∈ 𝑉 ∧ ((♯‘𝑉) − 1) ∈ ℕ0)
∧ (♯‘𝑉) =
(((♯‘𝑉) −
1) + 1)) → (♯‘(𝑉 ∖ {𝑁})) = ((♯‘𝑉) − 1)) |
23 | 6, 7, 13, 20, 22 | syl31anc 1480 |
. . . . . . . . . 10
⊢ ((((𝑉 ∈ V ∧
(♯‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) ∧ 𝑌 ∈ ℕ) →
(♯‘(𝑉 ∖
{𝑁})) =
((♯‘𝑉) −
1)) |
24 | | oveq1 6820 |
. . . . . . . . . . . . 13
⊢
((♯‘(𝑉
∖ {𝑁})) =
((♯‘𝑉) −
1) → ((♯‘(𝑉 ∖ {𝑁}))C2) = (((♯‘𝑉) − 1)C2)) |
25 | 24 | eqeq2d 2770 |
. . . . . . . . . . . 12
⊢
((♯‘(𝑉
∖ {𝑁})) =
((♯‘𝑉) −
1) → ((♯‘𝐹) = ((♯‘(𝑉 ∖ {𝑁}))C2) ↔ (♯‘𝐹) = (((♯‘𝑉) −
1)C2))) |
26 | 9 | ad2antlr 765 |
. . . . . . . . . . . . . . 15
⊢ (((𝑉 ∈ V ∧
(♯‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) → (𝑌 ∈ ℕ ↔ (♯‘𝑉) ∈
ℕ)) |
27 | | nnnn0 11491 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((♯‘𝑉)
∈ ℕ → (♯‘𝑉) ∈
ℕ0) |
28 | | hashclb 13341 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑉 ∈ V → (𝑉 ∈ Fin ↔
(♯‘𝑉) ∈
ℕ0)) |
29 | 27, 28 | syl5ibrcom 237 |
. . . . . . . . . . . . . . . . . . 19
⊢
((♯‘𝑉)
∈ ℕ → (𝑉
∈ V → 𝑉 ∈
Fin)) |
30 | | cusgrsizeindb0.e |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝐸 = (Edg‘𝐺) |
31 | | cusgrsizeinds.f |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒} |
32 | 1, 30, 31 | cusgrsizeinds 26558 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐺 ∈ ComplUSGraph ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (♯‘𝐸) = (((♯‘𝑉) − 1) + (♯‘𝐹))) |
33 | | oveq2 6821 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((♯‘𝐹) =
(((♯‘𝑉) −
1)C2) → (((♯‘𝑉) − 1) + (♯‘𝐹)) = (((♯‘𝑉) − 1) +
(((♯‘𝑉) −
1)C2))) |
34 | 33 | eqeq2d 2770 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((♯‘𝐹) =
(((♯‘𝑉) −
1)C2) → ((♯‘𝐸) = (((♯‘𝑉) − 1) + (♯‘𝐹)) ↔ (♯‘𝐸) = (((♯‘𝑉) − 1) +
(((♯‘𝑉) −
1)C2)))) |
35 | 34 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((♯‘𝑉)
∈ ℕ ∧ (♯‘𝐹) = (((♯‘𝑉) − 1)C2)) →
((♯‘𝐸) =
(((♯‘𝑉) −
1) + (♯‘𝐹))
↔ (♯‘𝐸) =
(((♯‘𝑉) −
1) + (((♯‘𝑉)
− 1)C2)))) |
36 | | bcn2m1 13305 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((♯‘𝑉)
∈ ℕ → (((♯‘𝑉) − 1) + (((♯‘𝑉) − 1)C2)) =
((♯‘𝑉)C2)) |
37 | 36 | eqeq2d 2770 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((♯‘𝑉)
∈ ℕ → ((♯‘𝐸) = (((♯‘𝑉) − 1) + (((♯‘𝑉) − 1)C2)) ↔
(♯‘𝐸) =
((♯‘𝑉)C2))) |
38 | 37 | biimpd 219 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((♯‘𝑉)
∈ ℕ → ((♯‘𝐸) = (((♯‘𝑉) − 1) + (((♯‘𝑉) − 1)C2)) →
(♯‘𝐸) =
((♯‘𝑉)C2))) |
39 | 38 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((♯‘𝑉)
∈ ℕ ∧ (♯‘𝐹) = (((♯‘𝑉) − 1)C2)) →
((♯‘𝐸) =
(((♯‘𝑉) −
1) + (((♯‘𝑉)
− 1)C2)) → (♯‘𝐸) = ((♯‘𝑉)C2))) |
40 | 35, 39 | sylbid 230 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((♯‘𝑉)
∈ ℕ ∧ (♯‘𝐹) = (((♯‘𝑉) − 1)C2)) →
((♯‘𝐸) =
(((♯‘𝑉) −
1) + (♯‘𝐹))
→ (♯‘𝐸) =
((♯‘𝑉)C2))) |
41 | 40 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((♯‘𝑉)
∈ ℕ → ((♯‘𝐹) = (((♯‘𝑉) − 1)C2) → ((♯‘𝐸) = (((♯‘𝑉) − 1) +
(♯‘𝐹)) →
(♯‘𝐸) =
((♯‘𝑉)C2)))) |
42 | 41 | com3r 87 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((♯‘𝐸) =
(((♯‘𝑉) −
1) + (♯‘𝐹))
→ ((♯‘𝑉)
∈ ℕ → ((♯‘𝐹) = (((♯‘𝑉) − 1)C2) → (♯‘𝐸) = ((♯‘𝑉)C2)))) |
43 | 32, 42 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐺 ∈ ComplUSGraph ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → ((♯‘𝑉) ∈ ℕ →
((♯‘𝐹) =
(((♯‘𝑉) −
1)C2) → (♯‘𝐸) = ((♯‘𝑉)C2)))) |
44 | 43 | 3exp 1113 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐺 ∈ ComplUSGraph →
(𝑉 ∈ Fin → (𝑁 ∈ 𝑉 → ((♯‘𝑉) ∈ ℕ →
((♯‘𝐹) =
(((♯‘𝑉) −
1)C2) → (♯‘𝐸) = ((♯‘𝑉)C2)))))) |
45 | 44 | com14 96 |
. . . . . . . . . . . . . . . . . . 19
⊢
((♯‘𝑉)
∈ ℕ → (𝑉
∈ Fin → (𝑁 ∈
𝑉 → (𝐺 ∈ ComplUSGraph →
((♯‘𝐹) =
(((♯‘𝑉) −
1)C2) → (♯‘𝐸) = ((♯‘𝑉)C2)))))) |
46 | 29, 45 | syldc 48 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑉 ∈ V →
((♯‘𝑉) ∈
ℕ → (𝑁 ∈
𝑉 → (𝐺 ∈ ComplUSGraph →
((♯‘𝐹) =
(((♯‘𝑉) −
1)C2) → (♯‘𝐸) = ((♯‘𝑉)C2)))))) |
47 | 46 | com23 86 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑉 ∈ V → (𝑁 ∈ 𝑉 → ((♯‘𝑉) ∈ ℕ → (𝐺 ∈ ComplUSGraph →
((♯‘𝐹) =
(((♯‘𝑉) −
1)C2) → (♯‘𝐸) = ((♯‘𝑉)C2)))))) |
48 | 47 | adantr 472 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑉 ∈ V ∧
(♯‘𝑉) = 𝑌) → (𝑁 ∈ 𝑉 → ((♯‘𝑉) ∈ ℕ → (𝐺 ∈ ComplUSGraph →
((♯‘𝐹) =
(((♯‘𝑉) −
1)C2) → (♯‘𝐸) = ((♯‘𝑉)C2)))))) |
49 | 48 | imp 444 |
. . . . . . . . . . . . . . 15
⊢ (((𝑉 ∈ V ∧
(♯‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) → ((♯‘𝑉) ∈ ℕ → (𝐺 ∈ ComplUSGraph →
((♯‘𝐹) =
(((♯‘𝑉) −
1)C2) → (♯‘𝐸) = ((♯‘𝑉)C2))))) |
50 | 26, 49 | sylbid 230 |
. . . . . . . . . . . . . 14
⊢ (((𝑉 ∈ V ∧
(♯‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) → (𝑌 ∈ ℕ → (𝐺 ∈ ComplUSGraph →
((♯‘𝐹) =
(((♯‘𝑉) −
1)C2) → (♯‘𝐸) = ((♯‘𝑉)C2))))) |
51 | 50 | imp 444 |
. . . . . . . . . . . . 13
⊢ ((((𝑉 ∈ V ∧
(♯‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) ∧ 𝑌 ∈ ℕ) → (𝐺 ∈ ComplUSGraph →
((♯‘𝐹) =
(((♯‘𝑉) −
1)C2) → (♯‘𝐸) = ((♯‘𝑉)C2)))) |
52 | 51 | com13 88 |
. . . . . . . . . . . 12
⊢
((♯‘𝐹) =
(((♯‘𝑉) −
1)C2) → (𝐺 ∈
ComplUSGraph → ((((𝑉
∈ V ∧ (♯‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) ∧ 𝑌 ∈ ℕ) → (♯‘𝐸) = ((♯‘𝑉)C2)))) |
53 | 25, 52 | syl6bi 243 |
. . . . . . . . . . 11
⊢
((♯‘(𝑉
∖ {𝑁})) =
((♯‘𝑉) −
1) → ((♯‘𝐹) = ((♯‘(𝑉 ∖ {𝑁}))C2) → (𝐺 ∈ ComplUSGraph → ((((𝑉 ∈ V ∧
(♯‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) ∧ 𝑌 ∈ ℕ) → (♯‘𝐸) = ((♯‘𝑉)C2))))) |
54 | 53 | com24 95 |
. . . . . . . . . 10
⊢
((♯‘(𝑉
∖ {𝑁})) =
((♯‘𝑉) −
1) → ((((𝑉 ∈ V
∧ (♯‘𝑉) =
𝑌) ∧ 𝑁 ∈ 𝑉) ∧ 𝑌 ∈ ℕ) → (𝐺 ∈ ComplUSGraph →
((♯‘𝐹) =
((♯‘(𝑉 ∖
{𝑁}))C2) →
(♯‘𝐸) =
((♯‘𝑉)C2))))) |
55 | 23, 54 | mpcom 38 |
. . . . . . . . 9
⊢ ((((𝑉 ∈ V ∧
(♯‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) ∧ 𝑌 ∈ ℕ) → (𝐺 ∈ ComplUSGraph →
((♯‘𝐹) =
((♯‘(𝑉 ∖
{𝑁}))C2) →
(♯‘𝐸) =
((♯‘𝑉)C2)))) |
56 | 55 | ex 449 |
. . . . . . . 8
⊢ (((𝑉 ∈ V ∧
(♯‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) → (𝑌 ∈ ℕ → (𝐺 ∈ ComplUSGraph →
((♯‘𝐹) =
((♯‘(𝑉 ∖
{𝑁}))C2) →
(♯‘𝐸) =
((♯‘𝑉)C2))))) |
57 | 56 | adantllr 757 |
. . . . . . 7
⊢ ((((𝑉 ∈ V ∧ 𝑌 ∈ ℕ0)
∧ (♯‘𝑉) =
𝑌) ∧ 𝑁 ∈ 𝑉) → (𝑌 ∈ ℕ → (𝐺 ∈ ComplUSGraph →
((♯‘𝐹) =
((♯‘(𝑉 ∖
{𝑁}))C2) →
(♯‘𝐸) =
((♯‘𝑉)C2))))) |
58 | 5, 57 | mpd 15 |
. . . . . 6
⊢ ((((𝑉 ∈ V ∧ 𝑌 ∈ ℕ0)
∧ (♯‘𝑉) =
𝑌) ∧ 𝑁 ∈ 𝑉) → (𝐺 ∈ ComplUSGraph →
((♯‘𝐹) =
((♯‘(𝑉 ∖
{𝑁}))C2) →
(♯‘𝐸) =
((♯‘𝑉)C2)))) |
59 | 58 | exp41 639 |
. . . . 5
⊢ (𝑉 ∈ V → (𝑌 ∈ ℕ0
→ ((♯‘𝑉) =
𝑌 → (𝑁 ∈ 𝑉 → (𝐺 ∈ ComplUSGraph →
((♯‘𝐹) =
((♯‘(𝑉 ∖
{𝑁}))C2) →
(♯‘𝐸) =
((♯‘𝑉)C2))))))) |
60 | 59 | com25 99 |
. . . 4
⊢ (𝑉 ∈ V → (𝐺 ∈ ComplUSGraph →
((♯‘𝑉) = 𝑌 → (𝑁 ∈ 𝑉 → (𝑌 ∈ ℕ0 →
((♯‘𝐹) =
((♯‘(𝑉 ∖
{𝑁}))C2) →
(♯‘𝐸) =
((♯‘𝑉)C2))))))) |
61 | 3, 60 | ax-mp 5 |
. . 3
⊢ (𝐺 ∈ ComplUSGraph →
((♯‘𝑉) = 𝑌 → (𝑁 ∈ 𝑉 → (𝑌 ∈ ℕ0 →
((♯‘𝐹) =
((♯‘(𝑉 ∖
{𝑁}))C2) →
(♯‘𝐸) =
((♯‘𝑉)C2)))))) |
62 | 61 | 3imp 1102 |
. 2
⊢ ((𝐺 ∈ ComplUSGraph ∧
(♯‘𝑉) = 𝑌 ∧ 𝑁 ∈ 𝑉) → (𝑌 ∈ ℕ0 →
((♯‘𝐹) =
((♯‘(𝑉 ∖
{𝑁}))C2) →
(♯‘𝐸) =
((♯‘𝑉)C2)))) |
63 | 62 | com12 32 |
1
⊢ (𝑌 ∈ ℕ0
→ ((𝐺 ∈
ComplUSGraph ∧ (♯‘𝑉) = 𝑌 ∧ 𝑁 ∈ 𝑉) → ((♯‘𝐹) = ((♯‘(𝑉 ∖ {𝑁}))C2) → (♯‘𝐸) = ((♯‘𝑉)C2)))) |