Metamath Proof Explorer

Theorem cusgrsize2inds

Description: Induction step in cusgrsize . If the size of the complete graph with n vertices reduced by one vertex is " ( n - 1 ) choose 2", the size of the complete graph with n vertices is " n choose 2". (Contributed by Alexander van der Vekens, 11-Jan-2018) (Revised by AV, 9-Nov-2020)

Ref Expression
Hypotheses cusgrsizeindb0.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
cusgrsizeindb0.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
cusgrsizeinds.f ⊢ 𝐹 = { 𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒 }
Assertion cusgrsize2inds ( 𝑌 ∈ ℕ0 → ( ( 𝐺 ∈ ComplUSGraph ∧ ( ♯ ‘ 𝑉 ) = 𝑌 ∧ 𝑁 ∈ 𝑉 ) → ( ( ♯ ‘ 𝐹 ) = ( ( ♯ ‘ ( 𝑉 ∖ { 𝑁 } ) ) C 2 ) → ( ♯ ‘ 𝐸 ) = ( ( ♯ ‘ 𝑉 ) C 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 cusgrsizeindb0.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 cusgrsizeindb0.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 cusgrsizeinds.f ⊢ 𝐹 = { 𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒 }
4 1 fvexi ⊢ 𝑉 ∈ V
5 hashnn0n0nn ⊢ ( ( ( 𝑉 ∈ V ∧ 𝑌 ∈ ℕ0 ) ∧ ( ( ♯ ‘ 𝑉 ) = 𝑌 ∧ 𝑁 ∈ 𝑉 ) ) → 𝑌 ∈ ℕ )
6 5 anassrs ⊢ ( ( ( ( 𝑉 ∈ V ∧ 𝑌 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑉 ) = 𝑌 ) ∧ 𝑁 ∈ 𝑉 ) → 𝑌 ∈ ℕ )
7 simplll ⊢ ( ( ( ( 𝑉 ∈ V ∧ ( ♯ ‘ 𝑉 ) = 𝑌 ) ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑌 ∈ ℕ ) → 𝑉 ∈ V )
8 simplr ⊢ ( ( ( ( 𝑉 ∈ V ∧ ( ♯ ‘ 𝑉 ) = 𝑌 ) ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑌 ∈ ℕ ) → 𝑁 ∈ 𝑉 )
9 eleq1 ⊢ ( 𝑌 = ( ♯ ‘ 𝑉 ) → ( 𝑌 ∈ ℕ ↔ ( ♯ ‘ 𝑉 ) ∈ ℕ ) )
10 9 eqcoms ⊢ ( ( ♯ ‘ 𝑉 ) = 𝑌 → ( 𝑌 ∈ ℕ ↔ ( ♯ ‘ 𝑉 ) ∈ ℕ ) )
11 nnm1nn0 ⊢ ( ( ♯ ‘ 𝑉 ) ∈ ℕ → ( ( ♯ ‘ 𝑉 ) − 1 ) ∈ ℕ0 )
12 10 11 syl6bi ⊢ ( ( ♯ ‘ 𝑉 ) = 𝑌 → ( 𝑌 ∈ ℕ → ( ( ♯ ‘ 𝑉 ) − 1 ) ∈ ℕ0 ) )
13 12 ad2antlr ⊢ ( ( ( 𝑉 ∈ V ∧ ( ♯ ‘ 𝑉 ) = 𝑌 ) ∧ 𝑁 ∈ 𝑉 ) → ( 𝑌 ∈ ℕ → ( ( ♯ ‘ 𝑉 ) − 1 ) ∈ ℕ0 ) )
14 13 imp ⊢ ( ( ( ( 𝑉 ∈ V ∧ ( ♯ ‘ 𝑉 ) = 𝑌 ) ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑌 ∈ ℕ ) → ( ( ♯ ‘ 𝑉 ) − 1 ) ∈ ℕ0 )
15 nncn ⊢ ( ( ♯ ‘ 𝑉 ) ∈ ℕ → ( ♯ ‘ 𝑉 ) ∈ ℂ )
16 1cnd ⊢ ( ( ♯ ‘ 𝑉 ) ∈ ℕ → 1 ∈ ℂ )
17 15 16 npcand ⊢ ( ( ♯ ‘ 𝑉 ) ∈ ℕ → ( ( ( ♯ ‘ 𝑉 ) − 1 ) + 1 ) = ( ♯ ‘ 𝑉 ) )
18 17 eqcomd ⊢ ( ( ♯ ‘ 𝑉 ) ∈ ℕ → ( ♯ ‘ 𝑉 ) = ( ( ( ♯ ‘ 𝑉 ) − 1 ) + 1 ) )
19 10 18 syl6bi ⊢ ( ( ♯ ‘ 𝑉 ) = 𝑌 → ( 𝑌 ∈ ℕ → ( ♯ ‘ 𝑉 ) = ( ( ( ♯ ‘ 𝑉 ) − 1 ) + 1 ) ) )
20 19 ad2antlr ⊢ ( ( ( 𝑉 ∈ V ∧ ( ♯ ‘ 𝑉 ) = 𝑌 ) ∧ 𝑁 ∈ 𝑉 ) → ( 𝑌 ∈ ℕ → ( ♯ ‘ 𝑉 ) = ( ( ( ♯ ‘ 𝑉 ) − 1 ) + 1 ) ) )
21 20 imp ⊢ ( ( ( ( 𝑉 ∈ V ∧ ( ♯ ‘ 𝑉 ) = 𝑌 ) ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑌 ∈ ℕ ) → ( ♯ ‘ 𝑉 ) = ( ( ( ♯ ‘ 𝑉 ) − 1 ) + 1 ) )
22 hashdifsnp1 ⊢ ( ( 𝑉 ∈ V ∧ 𝑁 ∈ 𝑉 ∧ ( ( ♯ ‘ 𝑉 ) − 1 ) ∈ ℕ0 ) → ( ( ♯ ‘ 𝑉 ) = ( ( ( ♯ ‘ 𝑉 ) − 1 ) + 1 ) → ( ♯ ‘ ( 𝑉 ∖ { 𝑁 } ) ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ) )
23 22 imp ⊢ ( ( ( 𝑉 ∈ V ∧ 𝑁 ∈ 𝑉 ∧ ( ( ♯ ‘ 𝑉 ) − 1 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑉 ) = ( ( ( ♯ ‘ 𝑉 ) − 1 ) + 1 ) ) → ( ♯ ‘ ( 𝑉 ∖ { 𝑁 } ) ) = ( ( ♯ ‘ 𝑉 ) − 1 ) )
24 7 8 14 21 23 syl31anc ⊢ ( ( ( ( 𝑉 ∈ V ∧ ( ♯ ‘ 𝑉 ) = 𝑌 ) ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑌 ∈ ℕ ) → ( ♯ ‘ ( 𝑉 ∖ { 𝑁 } ) ) = ( ( ♯ ‘ 𝑉 ) − 1 ) )
25 oveq1 ⊢ ( ( ♯ ‘ ( 𝑉 ∖ { 𝑁 } ) ) = ( ( ♯ ‘ 𝑉 ) − 1 ) → ( ( ♯ ‘ ( 𝑉 ∖ { 𝑁 } ) ) C 2 ) = ( ( ( ♯ ‘ 𝑉 ) − 1 ) C 2 ) )
26 25 eqeq2d ⊢ ( ( ♯ ‘ ( 𝑉 ∖ { 𝑁 } ) ) = ( ( ♯ ‘ 𝑉 ) − 1 ) → ( ( ♯ ‘ 𝐹 ) = ( ( ♯ ‘ ( 𝑉 ∖ { 𝑁 } ) ) C 2 ) ↔ ( ♯ ‘ 𝐹 ) = ( ( ( ♯ ‘ 𝑉 ) − 1 ) C 2 ) ) )
27 10 ad2antlr ⊢ ( ( ( 𝑉 ∈ V ∧ ( ♯ ‘ 𝑉 ) = 𝑌 ) ∧ 𝑁 ∈ 𝑉 ) → ( 𝑌 ∈ ℕ ↔ ( ♯ ‘ 𝑉 ) ∈ ℕ ) )
28 nnnn0 ⊢ ( ( ♯ ‘ 𝑉 ) ∈ ℕ → ( ♯ ‘ 𝑉 ) ∈ ℕ0 )
29 hashclb ⊢ ( 𝑉 ∈ V → ( 𝑉 ∈ Fin ↔ ( ♯ ‘ 𝑉 ) ∈ ℕ0 ) )
30 28 29 syl5ibrcom ⊢ ( ( ♯ ‘ 𝑉 ) ∈ ℕ → ( 𝑉 ∈ V → 𝑉 ∈ Fin ) )
31 1 2 3 cusgrsizeinds ⊢ ( ( 𝐺 ∈ ComplUSGraph ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉 ) → ( ♯ ‘ 𝐸 ) = ( ( ( ♯ ‘ 𝑉 ) − 1 ) + ( ♯ ‘ 𝐹 ) ) )
32 oveq2 ⊢ ( ( ♯ ‘ 𝐹 ) = ( ( ( ♯ ‘ 𝑉 ) − 1 ) C 2 ) → ( ( ( ♯ ‘ 𝑉 ) − 1 ) + ( ♯ ‘ 𝐹 ) ) = ( ( ( ♯ ‘ 𝑉 ) − 1 ) + ( ( ( ♯ ‘ 𝑉 ) − 1 ) C 2 ) ) )
33 32 eqeq2d ⊢ ( ( ♯ ‘ 𝐹 ) = ( ( ( ♯ ‘ 𝑉 ) − 1 ) C 2 ) → ( ( ♯ ‘ 𝐸 ) = ( ( ( ♯ ‘ 𝑉 ) − 1 ) + ( ♯ ‘ 𝐹 ) ) ↔ ( ♯ ‘ 𝐸 ) = ( ( ( ♯ ‘ 𝑉 ) − 1 ) + ( ( ( ♯ ‘ 𝑉 ) − 1 ) C 2 ) ) ) )
34 33 adantl ⊢ ( ( ( ♯ ‘ 𝑉 ) ∈ ℕ ∧ ( ♯ ‘ 𝐹 ) = ( ( ( ♯ ‘ 𝑉 ) − 1 ) C 2 ) ) → ( ( ♯ ‘ 𝐸 ) = ( ( ( ♯ ‘ 𝑉 ) − 1 ) + ( ♯ ‘ 𝐹 ) ) ↔ ( ♯ ‘ 𝐸 ) = ( ( ( ♯ ‘ 𝑉 ) − 1 ) + ( ( ( ♯ ‘ 𝑉 ) − 1 ) C 2 ) ) ) )
35 bcn2m1 ⊢ ( ( ♯ ‘ 𝑉 ) ∈ ℕ → ( ( ( ♯ ‘ 𝑉 ) − 1 ) + ( ( ( ♯ ‘ 𝑉 ) − 1 ) C 2 ) ) = ( ( ♯ ‘ 𝑉 ) C 2 ) )
36 35 eqeq2d ⊢ ( ( ♯ ‘ 𝑉 ) ∈ ℕ → ( ( ♯ ‘ 𝐸 ) = ( ( ( ♯ ‘ 𝑉 ) − 1 ) + ( ( ( ♯ ‘ 𝑉 ) − 1 ) C 2 ) ) ↔ ( ♯ ‘ 𝐸 ) = ( ( ♯ ‘ 𝑉 ) C 2 ) ) )
37 36 biimpd ⊢ ( ( ♯ ‘ 𝑉 ) ∈ ℕ → ( ( ♯ ‘ 𝐸 ) = ( ( ( ♯ ‘ 𝑉 ) − 1 ) + ( ( ( ♯ ‘ 𝑉 ) − 1 ) C 2 ) ) → ( ♯ ‘ 𝐸 ) = ( ( ♯ ‘ 𝑉 ) C 2 ) ) )
38 37 adantr ⊢ ( ( ( ♯ ‘ 𝑉 ) ∈ ℕ ∧ ( ♯ ‘ 𝐹 ) = ( ( ( ♯ ‘ 𝑉 ) − 1 ) C 2 ) ) → ( ( ♯ ‘ 𝐸 ) = ( ( ( ♯ ‘ 𝑉 ) − 1 ) + ( ( ( ♯ ‘ 𝑉 ) − 1 ) C 2 ) ) → ( ♯ ‘ 𝐸 ) = ( ( ♯ ‘ 𝑉 ) C 2 ) ) )
39 34 38 sylbid ⊢ ( ( ( ♯ ‘ 𝑉 ) ∈ ℕ ∧ ( ♯ ‘ 𝐹 ) = ( ( ( ♯ ‘ 𝑉 ) − 1 ) C 2 ) ) → ( ( ♯ ‘ 𝐸 ) = ( ( ( ♯ ‘ 𝑉 ) − 1 ) + ( ♯ ‘ 𝐹 ) ) → ( ♯ ‘ 𝐸 ) = ( ( ♯ ‘ 𝑉 ) C 2 ) ) )
40 39 ex ⊢ ( ( ♯ ‘ 𝑉 ) ∈ ℕ → ( ( ♯ ‘ 𝐹 ) = ( ( ( ♯ ‘ 𝑉 ) − 1 ) C 2 ) → ( ( ♯ ‘ 𝐸 ) = ( ( ( ♯ ‘ 𝑉 ) − 1 ) + ( ♯ ‘ 𝐹 ) ) → ( ♯ ‘ 𝐸 ) = ( ( ♯ ‘ 𝑉 ) C 2 ) ) ) )
41 40 com3r ⊢ ( ( ♯ ‘ 𝐸 ) = ( ( ( ♯ ‘ 𝑉 ) − 1 ) + ( ♯ ‘ 𝐹 ) ) → ( ( ♯ ‘ 𝑉 ) ∈ ℕ → ( ( ♯ ‘ 𝐹 ) = ( ( ( ♯ ‘ 𝑉 ) − 1 ) C 2 ) → ( ♯ ‘ 𝐸 ) = ( ( ♯ ‘ 𝑉 ) C 2 ) ) ) )
42 31 41 syl ⊢ ( ( 𝐺 ∈ ComplUSGraph ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉 ) → ( ( ♯ ‘ 𝑉 ) ∈ ℕ → ( ( ♯ ‘ 𝐹 ) = ( ( ( ♯ ‘ 𝑉 ) − 1 ) C 2 ) → ( ♯ ‘ 𝐸 ) = ( ( ♯ ‘ 𝑉 ) C 2 ) ) ) )
43 42 3exp ⊢ ( 𝐺 ∈ ComplUSGraph → ( 𝑉 ∈ Fin → ( 𝑁 ∈ 𝑉 → ( ( ♯ ‘ 𝑉 ) ∈ ℕ → ( ( ♯ ‘ 𝐹 ) = ( ( ( ♯ ‘ 𝑉 ) − 1 ) C 2 ) → ( ♯ ‘ 𝐸 ) = ( ( ♯ ‘ 𝑉 ) C 2 ) ) ) ) ) )
44 43 com14 ⊢ ( ( ♯ ‘ 𝑉 ) ∈ ℕ → ( 𝑉 ∈ Fin → ( 𝑁 ∈ 𝑉 → ( 𝐺 ∈ ComplUSGraph → ( ( ♯ ‘ 𝐹 ) = ( ( ( ♯ ‘ 𝑉 ) − 1 ) C 2 ) → ( ♯ ‘ 𝐸 ) = ( ( ♯ ‘ 𝑉 ) C 2 ) ) ) ) ) )
45 30 44 syldc ⊢ ( 𝑉 ∈ V → ( ( ♯ ‘ 𝑉 ) ∈ ℕ → ( 𝑁 ∈ 𝑉 → ( 𝐺 ∈ ComplUSGraph → ( ( ♯ ‘ 𝐹 ) = ( ( ( ♯ ‘ 𝑉 ) − 1 ) C 2 ) → ( ♯ ‘ 𝐸 ) = ( ( ♯ ‘ 𝑉 ) C 2 ) ) ) ) ) )
46 45 com23 ⊢ ( 𝑉 ∈ V → ( 𝑁 ∈ 𝑉 → ( ( ♯ ‘ 𝑉 ) ∈ ℕ → ( 𝐺 ∈ ComplUSGraph → ( ( ♯ ‘ 𝐹 ) = ( ( ( ♯ ‘ 𝑉 ) − 1 ) C 2 ) → ( ♯ ‘ 𝐸 ) = ( ( ♯ ‘ 𝑉 ) C 2 ) ) ) ) ) )
47 46 adantr ⊢ ( ( 𝑉 ∈ V ∧ ( ♯ ‘ 𝑉 ) = 𝑌 ) → ( 𝑁 ∈ 𝑉 → ( ( ♯ ‘ 𝑉 ) ∈ ℕ → ( 𝐺 ∈ ComplUSGraph → ( ( ♯ ‘ 𝐹 ) = ( ( ( ♯ ‘ 𝑉 ) − 1 ) C 2 ) → ( ♯ ‘ 𝐸 ) = ( ( ♯ ‘ 𝑉 ) C 2 ) ) ) ) ) )
48 47 imp ⊢ ( ( ( 𝑉 ∈ V ∧ ( ♯ ‘ 𝑉 ) = 𝑌 ) ∧ 𝑁 ∈ 𝑉 ) → ( ( ♯ ‘ 𝑉 ) ∈ ℕ → ( 𝐺 ∈ ComplUSGraph → ( ( ♯ ‘ 𝐹 ) = ( ( ( ♯ ‘ 𝑉 ) − 1 ) C 2 ) → ( ♯ ‘ 𝐸 ) = ( ( ♯ ‘ 𝑉 ) C 2 ) ) ) ) )
49 27 48 sylbid ⊢ ( ( ( 𝑉 ∈ V ∧ ( ♯ ‘ 𝑉 ) = 𝑌 ) ∧ 𝑁 ∈ 𝑉 ) → ( 𝑌 ∈ ℕ → ( 𝐺 ∈ ComplUSGraph → ( ( ♯ ‘ 𝐹 ) = ( ( ( ♯ ‘ 𝑉 ) − 1 ) C 2 ) → ( ♯ ‘ 𝐸 ) = ( ( ♯ ‘ 𝑉 ) C 2 ) ) ) ) )
50 49 imp ⊢ ( ( ( ( 𝑉 ∈ V ∧ ( ♯ ‘ 𝑉 ) = 𝑌 ) ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑌 ∈ ℕ ) → ( 𝐺 ∈ ComplUSGraph → ( ( ♯ ‘ 𝐹 ) = ( ( ( ♯ ‘ 𝑉 ) − 1 ) C 2 ) → ( ♯ ‘ 𝐸 ) = ( ( ♯ ‘ 𝑉 ) C 2 ) ) ) )
51 50 com13 ⊢ ( ( ♯ ‘ 𝐹 ) = ( ( ( ♯ ‘ 𝑉 ) − 1 ) C 2 ) → ( 𝐺 ∈ ComplUSGraph → ( ( ( ( 𝑉 ∈ V ∧ ( ♯ ‘ 𝑉 ) = 𝑌 ) ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑌 ∈ ℕ ) → ( ♯ ‘ 𝐸 ) = ( ( ♯ ‘ 𝑉 ) C 2 ) ) ) )
52 26 51 syl6bi ⊢ ( ( ♯ ‘ ( 𝑉 ∖ { 𝑁 } ) ) = ( ( ♯ ‘ 𝑉 ) − 1 ) → ( ( ♯ ‘ 𝐹 ) = ( ( ♯ ‘ ( 𝑉 ∖ { 𝑁 } ) ) C 2 ) → ( 𝐺 ∈ ComplUSGraph → ( ( ( ( 𝑉 ∈ V ∧ ( ♯ ‘ 𝑉 ) = 𝑌 ) ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑌 ∈ ℕ ) → ( ♯ ‘ 𝐸 ) = ( ( ♯ ‘ 𝑉 ) C 2 ) ) ) ) )
53 52 com24 ⊢ ( ( ♯ ‘ ( 𝑉 ∖ { 𝑁 } ) ) = ( ( ♯ ‘ 𝑉 ) − 1 ) → ( ( ( ( 𝑉 ∈ V ∧ ( ♯ ‘ 𝑉 ) = 𝑌 ) ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑌 ∈ ℕ ) → ( 𝐺 ∈ ComplUSGraph → ( ( ♯ ‘ 𝐹 ) = ( ( ♯ ‘ ( 𝑉 ∖ { 𝑁 } ) ) C 2 ) → ( ♯ ‘ 𝐸 ) = ( ( ♯ ‘ 𝑉 ) C 2 ) ) ) ) )
54 24 53 mpcom ⊢ ( ( ( ( 𝑉 ∈ V ∧ ( ♯ ‘ 𝑉 ) = 𝑌 ) ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑌 ∈ ℕ ) → ( 𝐺 ∈ ComplUSGraph → ( ( ♯ ‘ 𝐹 ) = ( ( ♯ ‘ ( 𝑉 ∖ { 𝑁 } ) ) C 2 ) → ( ♯ ‘ 𝐸 ) = ( ( ♯ ‘ 𝑉 ) C 2 ) ) ) )
55 54 ex ⊢ ( ( ( 𝑉 ∈ V ∧ ( ♯ ‘ 𝑉 ) = 𝑌 ) ∧ 𝑁 ∈ 𝑉 ) → ( 𝑌 ∈ ℕ → ( 𝐺 ∈ ComplUSGraph → ( ( ♯ ‘ 𝐹 ) = ( ( ♯ ‘ ( 𝑉 ∖ { 𝑁 } ) ) C 2 ) → ( ♯ ‘ 𝐸 ) = ( ( ♯ ‘ 𝑉 ) C 2 ) ) ) ) )
56 55 adantllr ⊢ ( ( ( ( 𝑉 ∈ V ∧ 𝑌 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑉 ) = 𝑌 ) ∧ 𝑁 ∈ 𝑉 ) → ( 𝑌 ∈ ℕ → ( 𝐺 ∈ ComplUSGraph → ( ( ♯ ‘ 𝐹 ) = ( ( ♯ ‘ ( 𝑉 ∖ { 𝑁 } ) ) C 2 ) → ( ♯ ‘ 𝐸 ) = ( ( ♯ ‘ 𝑉 ) C 2 ) ) ) ) )
57 6 56 mpd ⊢ ( ( ( ( 𝑉 ∈ V ∧ 𝑌 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑉 ) = 𝑌 ) ∧ 𝑁 ∈ 𝑉 ) → ( 𝐺 ∈ ComplUSGraph → ( ( ♯ ‘ 𝐹 ) = ( ( ♯ ‘ ( 𝑉 ∖ { 𝑁 } ) ) C 2 ) → ( ♯ ‘ 𝐸 ) = ( ( ♯ ‘ 𝑉 ) C 2 ) ) ) )
58 57 exp41 ⊢ ( 𝑉 ∈ V → ( 𝑌 ∈ ℕ0 → ( ( ♯ ‘ 𝑉 ) = 𝑌 → ( 𝑁 ∈ 𝑉 → ( 𝐺 ∈ ComplUSGraph → ( ( ♯ ‘ 𝐹 ) = ( ( ♯ ‘ ( 𝑉 ∖ { 𝑁 } ) ) C 2 ) → ( ♯ ‘ 𝐸 ) = ( ( ♯ ‘ 𝑉 ) C 2 ) ) ) ) ) ) )
59 58 com25 ⊢ ( 𝑉 ∈ V → ( 𝐺 ∈ ComplUSGraph → ( ( ♯ ‘ 𝑉 ) = 𝑌 → ( 𝑁 ∈ 𝑉 → ( 𝑌 ∈ ℕ0 → ( ( ♯ ‘ 𝐹 ) = ( ( ♯ ‘ ( 𝑉 ∖ { 𝑁 } ) ) C 2 ) → ( ♯ ‘ 𝐸 ) = ( ( ♯ ‘ 𝑉 ) C 2 ) ) ) ) ) ) )
60 4 59 ax-mp ⊢ ( 𝐺 ∈ ComplUSGraph → ( ( ♯ ‘ 𝑉 ) = 𝑌 → ( 𝑁 ∈ 𝑉 → ( 𝑌 ∈ ℕ0 → ( ( ♯ ‘ 𝐹 ) = ( ( ♯ ‘ ( 𝑉 ∖ { 𝑁 } ) ) C 2 ) → ( ♯ ‘ 𝐸 ) = ( ( ♯ ‘ 𝑉 ) C 2 ) ) ) ) ) )
61 60 3imp ⊢ ( ( 𝐺 ∈ ComplUSGraph ∧ ( ♯ ‘ 𝑉 ) = 𝑌 ∧ 𝑁 ∈ 𝑉 ) → ( 𝑌 ∈ ℕ0 → ( ( ♯ ‘ 𝐹 ) = ( ( ♯ ‘ ( 𝑉 ∖ { 𝑁 } ) ) C 2 ) → ( ♯ ‘ 𝐸 ) = ( ( ♯ ‘ 𝑉 ) C 2 ) ) ) )
62 61 com12 ⊢ ( 𝑌 ∈ ℕ0 → ( ( 𝐺 ∈ ComplUSGraph ∧ ( ♯ ‘ 𝑉 ) = 𝑌 ∧ 𝑁 ∈ 𝑉 ) → ( ( ♯ ‘ 𝐹 ) = ( ( ♯ ‘ ( 𝑉 ∖ { 𝑁 } ) ) C 2 ) → ( ♯ ‘ 𝐸 ) = ( ( ♯ ‘ 𝑉 ) C 2 ) ) ) )