Proof of Theorem cusgrasize2inds
Step | Hyp | Ref
| Expression |
1 | | cusisusgra 25987 |
. . . . 5
⊢ (𝑉 ComplUSGrph 𝐸 → 𝑉 USGrph 𝐸) |
2 | | usgrav 25867 |
. . . . 5
⊢ (𝑉 USGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
3 | 1, 2 | syl 17 |
. . . 4
⊢ (𝑉 ComplUSGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
4 | | hashnn0n0nn 13041 |
. . . . . . . . 9
⊢ (((𝑉 ∈ V ∧ 𝑌 ∈ ℕ0)
∧ ((#‘𝑉) = 𝑌 ∧ 𝑁 ∈ 𝑉)) → 𝑌 ∈ ℕ) |
5 | 4 | anassrs 678 |
. . . . . . . 8
⊢ ((((𝑉 ∈ V ∧ 𝑌 ∈ ℕ0)
∧ (#‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) → 𝑌 ∈ ℕ) |
6 | | simplll 794 |
. . . . . . . . . . . 12
⊢ ((((𝑉 ∈ V ∧ (#‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) ∧ 𝑌 ∈ ℕ) → 𝑉 ∈ V) |
7 | | simplr 788 |
. . . . . . . . . . . 12
⊢ ((((𝑉 ∈ V ∧ (#‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) ∧ 𝑌 ∈ ℕ) → 𝑁 ∈ 𝑉) |
8 | | eleq1 2676 |
. . . . . . . . . . . . . . . 16
⊢ (𝑌 = (#‘𝑉) → (𝑌 ∈ ℕ ↔ (#‘𝑉) ∈
ℕ)) |
9 | 8 | eqcoms 2618 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑉) = 𝑌 → (𝑌 ∈ ℕ ↔ (#‘𝑉) ∈
ℕ)) |
10 | | nnm1nn0 11211 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑉) ∈
ℕ → ((#‘𝑉)
− 1) ∈ ℕ0) |
11 | 9, 10 | syl6bi 242 |
. . . . . . . . . . . . . 14
⊢
((#‘𝑉) = 𝑌 → (𝑌 ∈ ℕ → ((#‘𝑉) − 1) ∈
ℕ0)) |
12 | 11 | ad2antlr 759 |
. . . . . . . . . . . . 13
⊢ (((𝑉 ∈ V ∧ (#‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) → (𝑌 ∈ ℕ → ((#‘𝑉) − 1) ∈
ℕ0)) |
13 | 12 | imp 444 |
. . . . . . . . . . . 12
⊢ ((((𝑉 ∈ V ∧ (#‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) ∧ 𝑌 ∈ ℕ) → ((#‘𝑉) − 1) ∈
ℕ0) |
14 | | nncn 10905 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘𝑉) ∈
ℕ → (#‘𝑉)
∈ ℂ) |
15 | | 1cnd 9935 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘𝑉) ∈
ℕ → 1 ∈ ℂ) |
16 | 14, 15 | npcand 10275 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝑉) ∈
ℕ → (((#‘𝑉) − 1) + 1) = (#‘𝑉)) |
17 | 16 | eqcomd 2616 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑉) ∈
ℕ → (#‘𝑉)
= (((#‘𝑉) − 1)
+ 1)) |
18 | 9, 17 | syl6bi 242 |
. . . . . . . . . . . . . 14
⊢
((#‘𝑉) = 𝑌 → (𝑌 ∈ ℕ → (#‘𝑉) = (((#‘𝑉) − 1) + 1))) |
19 | 18 | ad2antlr 759 |
. . . . . . . . . . . . 13
⊢ (((𝑉 ∈ V ∧ (#‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) → (𝑌 ∈ ℕ → (#‘𝑉) = (((#‘𝑉) − 1) + 1))) |
20 | 19 | imp 444 |
. . . . . . . . . . . 12
⊢ ((((𝑉 ∈ V ∧ (#‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) ∧ 𝑌 ∈ ℕ) → (#‘𝑉) = (((#‘𝑉) − 1) + 1)) |
21 | | brfi1indlem 13133 |
. . . . . . . . . . . . 13
⊢ ((𝑉 ∈ V ∧ 𝑁 ∈ 𝑉 ∧ ((#‘𝑉) − 1) ∈ ℕ0)
→ ((#‘𝑉) =
(((#‘𝑉) − 1) +
1) → (#‘(𝑉
∖ {𝑁})) =
((#‘𝑉) −
1))) |
22 | 21 | imp 444 |
. . . . . . . . . . . 12
⊢ (((𝑉 ∈ V ∧ 𝑁 ∈ 𝑉 ∧ ((#‘𝑉) − 1) ∈ ℕ0)
∧ (#‘𝑉) =
(((#‘𝑉) − 1) +
1)) → (#‘(𝑉
∖ {𝑁})) =
((#‘𝑉) −
1)) |
23 | 6, 7, 13, 20, 22 | syl31anc 1321 |
. . . . . . . . . . 11
⊢ ((((𝑉 ∈ V ∧ (#‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) ∧ 𝑌 ∈ ℕ) → (#‘(𝑉 ∖ {𝑁})) = ((#‘𝑉) − 1)) |
24 | | oveq1 6556 |
. . . . . . . . . . . . . 14
⊢
((#‘(𝑉 ∖
{𝑁})) = ((#‘𝑉) − 1) →
((#‘(𝑉 ∖ {𝑁}))C2) = (((#‘𝑉) −
1)C2)) |
25 | 24 | eqeq2d 2620 |
. . . . . . . . . . . . 13
⊢
((#‘(𝑉 ∖
{𝑁})) = ((#‘𝑉) − 1) →
((#‘𝐹) =
((#‘(𝑉 ∖ {𝑁}))C2) ↔ (#‘𝐹) = (((#‘𝑉) − 1)C2))) |
26 | 9 | ad2antlr 759 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑉 ∈ V ∧ (#‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) → (𝑌 ∈ ℕ ↔ (#‘𝑉) ∈
ℕ)) |
27 | | nnnn0 11176 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((#‘𝑉) ∈
ℕ → (#‘𝑉)
∈ ℕ0) |
28 | | hashclb 13011 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑉 ∈ V → (𝑉 ∈ Fin ↔
(#‘𝑉) ∈
ℕ0)) |
29 | 27, 28 | syl5ibrcom 236 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((#‘𝑉) ∈
ℕ → (𝑉 ∈ V
→ 𝑉 ∈
Fin)) |
30 | 29 | impcom 445 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑉 ∈ V ∧ (#‘𝑉) ∈ ℕ) → 𝑉 ∈ Fin) |
31 | | cusgrares.f |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 𝐹 = (𝐸 ↾ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)}) |
32 | 31 | cusgrasizeinds 26004 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑉 ComplUSGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (#‘𝐸) = (((#‘𝑉) − 1) + (#‘𝐹))) |
33 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((#‘𝐹) =
(((#‘𝑉) − 1)C2)
→ (((#‘𝑉)
− 1) + (#‘𝐹)) =
(((#‘𝑉) − 1) +
(((#‘𝑉) −
1)C2))) |
34 | 33 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((#‘𝐹) =
(((#‘𝑉) − 1)C2)
→ ((#‘𝐸) =
(((#‘𝑉) − 1) +
(#‘𝐹)) ↔
(#‘𝐸) =
(((#‘𝑉) − 1) +
(((#‘𝑉) −
1)C2)))) |
35 | 34 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((#‘𝑉) ∈
ℕ ∧ (#‘𝐹) =
(((#‘𝑉) −
1)C2)) → ((#‘𝐸)
= (((#‘𝑉) − 1)
+ (#‘𝐹)) ↔
(#‘𝐸) =
(((#‘𝑉) − 1) +
(((#‘𝑉) −
1)C2)))) |
36 | | bcn2m1 12973 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((#‘𝑉) ∈
ℕ → (((#‘𝑉) − 1) + (((#‘𝑉) − 1)C2)) = ((#‘𝑉)C2)) |
37 | 36 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((#‘𝑉) ∈
ℕ → ((#‘𝐸)
= (((#‘𝑉) − 1)
+ (((#‘𝑉) −
1)C2)) ↔ (#‘𝐸) =
((#‘𝑉)C2))) |
38 | 37 | biimpd 218 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((#‘𝑉) ∈
ℕ → ((#‘𝐸)
= (((#‘𝑉) − 1)
+ (((#‘𝑉) −
1)C2)) → (#‘𝐸) =
((#‘𝑉)C2))) |
39 | 38 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((#‘𝑉) ∈
ℕ ∧ (#‘𝐹) =
(((#‘𝑉) −
1)C2)) → ((#‘𝐸)
= (((#‘𝑉) − 1)
+ (((#‘𝑉) −
1)C2)) → (#‘𝐸) =
((#‘𝑉)C2))) |
40 | 35, 39 | sylbid 229 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((#‘𝑉) ∈
ℕ ∧ (#‘𝐹) =
(((#‘𝑉) −
1)C2)) → ((#‘𝐸)
= (((#‘𝑉) − 1)
+ (#‘𝐹)) →
(#‘𝐸) =
((#‘𝑉)C2))) |
41 | 40 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((#‘𝑉) ∈
ℕ → ((#‘𝐹)
= (((#‘𝑉) −
1)C2) → ((#‘𝐸) =
(((#‘𝑉) − 1) +
(#‘𝐹)) →
(#‘𝐸) =
((#‘𝑉)C2)))) |
42 | 41 | com3r 85 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((#‘𝐸) =
(((#‘𝑉) − 1) +
(#‘𝐹)) →
((#‘𝑉) ∈ ℕ
→ ((#‘𝐹) =
(((#‘𝑉) − 1)C2)
→ (#‘𝐸) =
((#‘𝑉)C2)))) |
43 | 32, 42 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑉 ComplUSGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → ((#‘𝑉) ∈ ℕ → ((#‘𝐹) = (((#‘𝑉) − 1)C2) → (#‘𝐸) = ((#‘𝑉)C2)))) |
44 | 43 | 3exp 1256 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑉 ComplUSGrph 𝐸 → (𝑉 ∈ Fin → (𝑁 ∈ 𝑉 → ((#‘𝑉) ∈ ℕ → ((#‘𝐹) = (((#‘𝑉) − 1)C2) → (#‘𝐸) = ((#‘𝑉)C2)))))) |
45 | 44 | com14 94 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((#‘𝑉) ∈
ℕ → (𝑉 ∈
Fin → (𝑁 ∈ 𝑉 → (𝑉 ComplUSGrph 𝐸 → ((#‘𝐹) = (((#‘𝑉) − 1)C2) → (#‘𝐸) = ((#‘𝑉)C2)))))) |
46 | 45 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑉 ∈ V ∧ (#‘𝑉) ∈ ℕ) → (𝑉 ∈ Fin → (𝑁 ∈ 𝑉 → (𝑉 ComplUSGrph 𝐸 → ((#‘𝐹) = (((#‘𝑉) − 1)C2) → (#‘𝐸) = ((#‘𝑉)C2)))))) |
47 | 30, 46 | mpd 15 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑉 ∈ V ∧ (#‘𝑉) ∈ ℕ) → (𝑁 ∈ 𝑉 → (𝑉 ComplUSGrph 𝐸 → ((#‘𝐹) = (((#‘𝑉) − 1)C2) → (#‘𝐸) = ((#‘𝑉)C2))))) |
48 | 47 | ex 449 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑉 ∈ V → ((#‘𝑉) ∈ ℕ → (𝑁 ∈ 𝑉 → (𝑉 ComplUSGrph 𝐸 → ((#‘𝐹) = (((#‘𝑉) − 1)C2) → (#‘𝐸) = ((#‘𝑉)C2)))))) |
49 | 48 | com23 84 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑉 ∈ V → (𝑁 ∈ 𝑉 → ((#‘𝑉) ∈ ℕ → (𝑉 ComplUSGrph 𝐸 → ((#‘𝐹) = (((#‘𝑉) − 1)C2) → (#‘𝐸) = ((#‘𝑉)C2)))))) |
50 | 49 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑉 ∈ V ∧ (#‘𝑉) = 𝑌) → (𝑁 ∈ 𝑉 → ((#‘𝑉) ∈ ℕ → (𝑉 ComplUSGrph 𝐸 → ((#‘𝐹) = (((#‘𝑉) − 1)C2) → (#‘𝐸) = ((#‘𝑉)C2)))))) |
51 | 50 | imp 444 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑉 ∈ V ∧ (#‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) → ((#‘𝑉) ∈ ℕ → (𝑉 ComplUSGrph 𝐸 → ((#‘𝐹) = (((#‘𝑉) − 1)C2) → (#‘𝐸) = ((#‘𝑉)C2))))) |
52 | 26, 51 | sylbid 229 |
. . . . . . . . . . . . . . 15
⊢ (((𝑉 ∈ V ∧ (#‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) → (𝑌 ∈ ℕ → (𝑉 ComplUSGrph 𝐸 → ((#‘𝐹) = (((#‘𝑉) − 1)C2) → (#‘𝐸) = ((#‘𝑉)C2))))) |
53 | 52 | imp 444 |
. . . . . . . . . . . . . 14
⊢ ((((𝑉 ∈ V ∧ (#‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) ∧ 𝑌 ∈ ℕ) → (𝑉 ComplUSGrph 𝐸 → ((#‘𝐹) = (((#‘𝑉) − 1)C2) → (#‘𝐸) = ((#‘𝑉)C2)))) |
54 | 53 | com13 86 |
. . . . . . . . . . . . 13
⊢
((#‘𝐹) =
(((#‘𝑉) − 1)C2)
→ (𝑉 ComplUSGrph 𝐸 → ((((𝑉 ∈ V ∧ (#‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) ∧ 𝑌 ∈ ℕ) → (#‘𝐸) = ((#‘𝑉)C2)))) |
55 | 25, 54 | syl6bi 242 |
. . . . . . . . . . . 12
⊢
((#‘(𝑉 ∖
{𝑁})) = ((#‘𝑉) − 1) →
((#‘𝐹) =
((#‘(𝑉 ∖ {𝑁}))C2) → (𝑉 ComplUSGrph 𝐸 → ((((𝑉 ∈ V ∧ (#‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) ∧ 𝑌 ∈ ℕ) → (#‘𝐸) = ((#‘𝑉)C2))))) |
56 | 55 | com24 93 |
. . . . . . . . . . 11
⊢
((#‘(𝑉 ∖
{𝑁})) = ((#‘𝑉) − 1) → ((((𝑉 ∈ V ∧ (#‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) ∧ 𝑌 ∈ ℕ) → (𝑉 ComplUSGrph 𝐸 → ((#‘𝐹) = ((#‘(𝑉 ∖ {𝑁}))C2) → (#‘𝐸) = ((#‘𝑉)C2))))) |
57 | 23, 56 | mpcom 37 |
. . . . . . . . . 10
⊢ ((((𝑉 ∈ V ∧ (#‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) ∧ 𝑌 ∈ ℕ) → (𝑉 ComplUSGrph 𝐸 → ((#‘𝐹) = ((#‘(𝑉 ∖ {𝑁}))C2) → (#‘𝐸) = ((#‘𝑉)C2)))) |
58 | 57 | ex 449 |
. . . . . . . . 9
⊢ (((𝑉 ∈ V ∧ (#‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) → (𝑌 ∈ ℕ → (𝑉 ComplUSGrph 𝐸 → ((#‘𝐹) = ((#‘(𝑉 ∖ {𝑁}))C2) → (#‘𝐸) = ((#‘𝑉)C2))))) |
59 | 58 | adantllr 751 |
. . . . . . . 8
⊢ ((((𝑉 ∈ V ∧ 𝑌 ∈ ℕ0)
∧ (#‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) → (𝑌 ∈ ℕ → (𝑉 ComplUSGrph 𝐸 → ((#‘𝐹) = ((#‘(𝑉 ∖ {𝑁}))C2) → (#‘𝐸) = ((#‘𝑉)C2))))) |
60 | 5, 59 | mpd 15 |
. . . . . . 7
⊢ ((((𝑉 ∈ V ∧ 𝑌 ∈ ℕ0)
∧ (#‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) → (𝑉 ComplUSGrph 𝐸 → ((#‘𝐹) = ((#‘(𝑉 ∖ {𝑁}))C2) → (#‘𝐸) = ((#‘𝑉)C2)))) |
61 | 60 | exp41 636 |
. . . . . 6
⊢ (𝑉 ∈ V → (𝑌 ∈ ℕ0
→ ((#‘𝑉) = 𝑌 → (𝑁 ∈ 𝑉 → (𝑉 ComplUSGrph 𝐸 → ((#‘𝐹) = ((#‘(𝑉 ∖ {𝑁}))C2) → (#‘𝐸) = ((#‘𝑉)C2))))))) |
62 | 61 | com25 97 |
. . . . 5
⊢ (𝑉 ∈ V → (𝑉 ComplUSGrph 𝐸 → ((#‘𝑉) = 𝑌 → (𝑁 ∈ 𝑉 → (𝑌 ∈ ℕ0 →
((#‘𝐹) =
((#‘(𝑉 ∖ {𝑁}))C2) → (#‘𝐸) = ((#‘𝑉)C2))))))) |
63 | 62 | adantr 480 |
. . . 4
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑉 ComplUSGrph 𝐸 → ((#‘𝑉) = 𝑌 → (𝑁 ∈ 𝑉 → (𝑌 ∈ ℕ0 →
((#‘𝐹) =
((#‘(𝑉 ∖ {𝑁}))C2) → (#‘𝐸) = ((#‘𝑉)C2))))))) |
64 | 3, 63 | mpcom 37 |
. . 3
⊢ (𝑉 ComplUSGrph 𝐸 → ((#‘𝑉) = 𝑌 → (𝑁 ∈ 𝑉 → (𝑌 ∈ ℕ0 →
((#‘𝐹) =
((#‘(𝑉 ∖ {𝑁}))C2) → (#‘𝐸) = ((#‘𝑉)C2)))))) |
65 | 64 | 3imp 1249 |
. 2
⊢ ((𝑉 ComplUSGrph 𝐸 ∧ (#‘𝑉) = 𝑌 ∧ 𝑁 ∈ 𝑉) → (𝑌 ∈ ℕ0 →
((#‘𝐹) =
((#‘(𝑉 ∖ {𝑁}))C2) → (#‘𝐸) = ((#‘𝑉)C2)))) |
66 | 65 | com12 32 |
1
⊢ (𝑌 ∈ ℕ0
→ ((𝑉 ComplUSGrph
𝐸 ∧ (#‘𝑉) = 𝑌 ∧ 𝑁 ∈ 𝑉) → ((#‘𝐹) = ((#‘(𝑉 ∖ {𝑁}))C2) → (#‘𝐸) = ((#‘𝑉)C2)))) |