Metamath Proof Explorer

Theorem cusgrsize

Description: The size of a finite complete simple graph with n vertices ( n e. NN0 ) is ( n _C 2 ) (" n choose 2") resp. ( ( ( n - 1 ) * n ) / 2 ) , see definition in section I.1 of Bollobas p. 3 . (Contributed by Alexander van der Vekens, 11-Jan-2018) (Revised by AV, 10-Nov-2020)

Ref Expression
Hypotheses cusgrsizeindb0.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
cusgrsizeindb0.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion cusgrsize ( ( 𝐺 ∈ ComplUSGraph ∧ 𝑉 ∈ Fin ) → ( ♯ ‘ 𝐸 ) = ( ( ♯ ‘ 𝑉 ) C 2 ) )

Proof

Step Hyp Ref Expression
1 cusgrsizeindb0.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 cusgrsizeindb0.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 edgval ⊢ ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 )
4 2 3 eqtri ⊢ 𝐸 = ran ( iEdg ‘ 𝐺 )
5 4 a1i ⊢ ( ( 𝐺 ∈ ComplUSGraph ∧ 𝑉 ∈ Fin ) → 𝐸 = ran ( iEdg ‘ 𝐺 ) )
6 5 fveq2d ⊢ ( ( 𝐺 ∈ ComplUSGraph ∧ 𝑉 ∈ Fin ) → ( ♯ ‘ 𝐸 ) = ( ♯ ‘ ran ( iEdg ‘ 𝐺 ) ) )
7 1 opeq1i ⊢ ⟨ 𝑉 , ( iEdg ‘ 𝐺 ) ⟩ = ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩
8 cusgrop ⊢ ( 𝐺 ∈ ComplUSGraph → ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ∈ ComplUSGraph )
9 7 8 eqeltrid ⊢ ( 𝐺 ∈ ComplUSGraph → ⟨ 𝑉 , ( iEdg ‘ 𝐺 ) ⟩ ∈ ComplUSGraph )
10 fvex ⊢ ( iEdg ‘ 𝐺 ) ∈ V
11 fvex ⊢ ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) ∈ V
12 rabexg ⊢ ( ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) ∈ V → { 𝑐 ∈ ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) ∣ 𝑛 ∉ 𝑐 } ∈ V )
13 12 resiexd ⊢ ( ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) ∈ V → ( I ↾ { 𝑐 ∈ ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) ∣ 𝑛 ∉ 𝑐 } ) ∈ V )
14 11 13 ax-mp ⊢ ( I ↾ { 𝑐 ∈ ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) ∣ 𝑛 ∉ 𝑐 } ) ∈ V
15 rneq ⊢ ( 𝑒 = ( iEdg ‘ 𝐺 ) → ran 𝑒 = ran ( iEdg ‘ 𝐺 ) )
16 15 fveq2d ⊢ ( 𝑒 = ( iEdg ‘ 𝐺 ) → ( ♯ ‘ ran 𝑒 ) = ( ♯ ‘ ran ( iEdg ‘ 𝐺 ) ) )
17 fveq2 ⊢ ( 𝑣 = 𝑉 → ( ♯ ‘ 𝑣 ) = ( ♯ ‘ 𝑉 ) )
18 17 oveq1d ⊢ ( 𝑣 = 𝑉 → ( ( ♯ ‘ 𝑣 ) C 2 ) = ( ( ♯ ‘ 𝑉 ) C 2 ) )
19 16 18 eqeqan12rd ⊢ ( ( 𝑣 = 𝑉 ∧ 𝑒 = ( iEdg ‘ 𝐺 ) ) → ( ( ♯ ‘ ran 𝑒 ) = ( ( ♯ ‘ 𝑣 ) C 2 ) ↔ ( ♯ ‘ ran ( iEdg ‘ 𝐺 ) ) = ( ( ♯ ‘ 𝑉 ) C 2 ) ) )
20 rneq ⊢ ( 𝑒 = 𝑓 → ran 𝑒 = ran 𝑓 )
21 20 fveq2d ⊢ ( 𝑒 = 𝑓 → ( ♯ ‘ ran 𝑒 ) = ( ♯ ‘ ran 𝑓 ) )
22 fveq2 ⊢ ( 𝑣 = 𝑤 → ( ♯ ‘ 𝑣 ) = ( ♯ ‘ 𝑤 ) )
23 22 oveq1d ⊢ ( 𝑣 = 𝑤 → ( ( ♯ ‘ 𝑣 ) C 2 ) = ( ( ♯ ‘ 𝑤 ) C 2 ) )
24 21 23 eqeqan12rd ⊢ ( ( 𝑣 = 𝑤 ∧ 𝑒 = 𝑓 ) → ( ( ♯ ‘ ran 𝑒 ) = ( ( ♯ ‘ 𝑣 ) C 2 ) ↔ ( ♯ ‘ ran 𝑓 ) = ( ( ♯ ‘ 𝑤 ) C 2 ) ) )
25 vex ⊢ 𝑣 ∈ V
26 vex ⊢ 𝑒 ∈ V
27 25 26 opvtxfvi ⊢ ( Vtx ‘ ⟨ 𝑣 , 𝑒 ⟩ ) = 𝑣
28 27 eqcomi ⊢ 𝑣 = ( Vtx ‘ ⟨ 𝑣 , 𝑒 ⟩ )
29 eqid ⊢ ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) = ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ )
30 eqid ⊢ { 𝑐 ∈ ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) ∣ 𝑛 ∉ 𝑐 } = { 𝑐 ∈ ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) ∣ 𝑛 ∉ 𝑐 }
31 eqid ⊢ ⟨ ( 𝑣 ∖ { 𝑛 } ) , ( I ↾ { 𝑐 ∈ ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) ∣ 𝑛 ∉ 𝑐 } ) ⟩ = ⟨ ( 𝑣 ∖ { 𝑛 } ) , ( I ↾ { 𝑐 ∈ ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) ∣ 𝑛 ∉ 𝑐 } ) ⟩
32 28 29 30 31 cusgrres ⊢ ( ( ⟨ 𝑣 , 𝑒 ⟩ ∈ ComplUSGraph ∧ 𝑛 ∈ 𝑣 ) → ⟨ ( 𝑣 ∖ { 𝑛 } ) , ( I ↾ { 𝑐 ∈ ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) ∣ 𝑛 ∉ 𝑐 } ) ⟩ ∈ ComplUSGraph )
33 rneq ⊢ ( 𝑓 = ( I ↾ { 𝑐 ∈ ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) ∣ 𝑛 ∉ 𝑐 } ) → ran 𝑓 = ran ( I ↾ { 𝑐 ∈ ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) ∣ 𝑛 ∉ 𝑐 } ) )
34 33 fveq2d ⊢ ( 𝑓 = ( I ↾ { 𝑐 ∈ ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) ∣ 𝑛 ∉ 𝑐 } ) → ( ♯ ‘ ran 𝑓 ) = ( ♯ ‘ ran ( I ↾ { 𝑐 ∈ ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) ∣ 𝑛 ∉ 𝑐 } ) ) )
35 34 adantl ⊢ ( ( 𝑤 = ( 𝑣 ∖ { 𝑛 } ) ∧ 𝑓 = ( I ↾ { 𝑐 ∈ ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) ∣ 𝑛 ∉ 𝑐 } ) ) → ( ♯ ‘ ran 𝑓 ) = ( ♯ ‘ ran ( I ↾ { 𝑐 ∈ ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) ∣ 𝑛 ∉ 𝑐 } ) ) )
36 fveq2 ⊢ ( 𝑤 = ( 𝑣 ∖ { 𝑛 } ) → ( ♯ ‘ 𝑤 ) = ( ♯ ‘ ( 𝑣 ∖ { 𝑛 } ) ) )
37 36 adantr ⊢ ( ( 𝑤 = ( 𝑣 ∖ { 𝑛 } ) ∧ 𝑓 = ( I ↾ { 𝑐 ∈ ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) ∣ 𝑛 ∉ 𝑐 } ) ) → ( ♯ ‘ 𝑤 ) = ( ♯ ‘ ( 𝑣 ∖ { 𝑛 } ) ) )
38 37 oveq1d ⊢ ( ( 𝑤 = ( 𝑣 ∖ { 𝑛 } ) ∧ 𝑓 = ( I ↾ { 𝑐 ∈ ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) ∣ 𝑛 ∉ 𝑐 } ) ) → ( ( ♯ ‘ 𝑤 ) C 2 ) = ( ( ♯ ‘ ( 𝑣 ∖ { 𝑛 } ) ) C 2 ) )
39 35 38 eqeq12d ⊢ ( ( 𝑤 = ( 𝑣 ∖ { 𝑛 } ) ∧ 𝑓 = ( I ↾ { 𝑐 ∈ ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) ∣ 𝑛 ∉ 𝑐 } ) ) → ( ( ♯ ‘ ran 𝑓 ) = ( ( ♯ ‘ 𝑤 ) C 2 ) ↔ ( ♯ ‘ ran ( I ↾ { 𝑐 ∈ ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) ∣ 𝑛 ∉ 𝑐 } ) ) = ( ( ♯ ‘ ( 𝑣 ∖ { 𝑛 } ) ) C 2 ) ) )
40 edgopval ⊢ ( ( 𝑣 ∈ V ∧ 𝑒 ∈ V ) → ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) = ran 𝑒 )
41 40 el2v ⊢ ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) = ran 𝑒
42 41 a1i ⊢ ( ( ⟨ 𝑣 , 𝑒 ⟩ ∈ ComplUSGraph ∧ ( ♯ ‘ 𝑣 ) = 0 ) → ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) = ran 𝑒 )
43 42 eqcomd ⊢ ( ( ⟨ 𝑣 , 𝑒 ⟩ ∈ ComplUSGraph ∧ ( ♯ ‘ 𝑣 ) = 0 ) → ran 𝑒 = ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) )
44 43 fveq2d ⊢ ( ( ⟨ 𝑣 , 𝑒 ⟩ ∈ ComplUSGraph ∧ ( ♯ ‘ 𝑣 ) = 0 ) → ( ♯ ‘ ran 𝑒 ) = ( ♯ ‘ ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) ) )
45 cusgrusgr ⊢ ( ⟨ 𝑣 , 𝑒 ⟩ ∈ ComplUSGraph → ⟨ 𝑣 , 𝑒 ⟩ ∈ USGraph )
46 usgruhgr ⊢ ( ⟨ 𝑣 , 𝑒 ⟩ ∈ USGraph → ⟨ 𝑣 , 𝑒 ⟩ ∈ UHGraph )
47 45 46 syl ⊢ ( ⟨ 𝑣 , 𝑒 ⟩ ∈ ComplUSGraph → ⟨ 𝑣 , 𝑒 ⟩ ∈ UHGraph )
48 28 29 cusgrsizeindb0 ⊢ ( ( ⟨ 𝑣 , 𝑒 ⟩ ∈ UHGraph ∧ ( ♯ ‘ 𝑣 ) = 0 ) → ( ♯ ‘ ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) ) = ( ( ♯ ‘ 𝑣 ) C 2 ) )
49 47 48 sylan ⊢ ( ( ⟨ 𝑣 , 𝑒 ⟩ ∈ ComplUSGraph ∧ ( ♯ ‘ 𝑣 ) = 0 ) → ( ♯ ‘ ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) ) = ( ( ♯ ‘ 𝑣 ) C 2 ) )
50 44 49 eqtrd ⊢ ( ( ⟨ 𝑣 , 𝑒 ⟩ ∈ ComplUSGraph ∧ ( ♯ ‘ 𝑣 ) = 0 ) → ( ♯ ‘ ran 𝑒 ) = ( ( ♯ ‘ 𝑣 ) C 2 ) )
51 rnresi ⊢ ran ( I ↾ { 𝑐 ∈ ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) ∣ 𝑛 ∉ 𝑐 } ) = { 𝑐 ∈ ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) ∣ 𝑛 ∉ 𝑐 }
52 51 fveq2i ⊢ ( ♯ ‘ ran ( I ↾ { 𝑐 ∈ ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) ∣ 𝑛 ∉ 𝑐 } ) ) = ( ♯ ‘ { 𝑐 ∈ ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) ∣ 𝑛 ∉ 𝑐 } )
53 41 a1i ⊢ ( ( ( 𝑦 + 1 ) ∈ ℕ0 ∧ ( ⟨ 𝑣 , 𝑒 ⟩ ∈ ComplUSGraph ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ∧ 𝑛 ∈ 𝑣 ) ) → ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) = ran 𝑒 )
54 53 rabeqdv ⊢ ( ( ( 𝑦 + 1 ) ∈ ℕ0 ∧ ( ⟨ 𝑣 , 𝑒 ⟩ ∈ ComplUSGraph ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ∧ 𝑛 ∈ 𝑣 ) ) → { 𝑐 ∈ ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) ∣ 𝑛 ∉ 𝑐 } = { 𝑐 ∈ ran 𝑒 ∣ 𝑛 ∉ 𝑐 } )
55 54 fveq2d ⊢ ( ( ( 𝑦 + 1 ) ∈ ℕ0 ∧ ( ⟨ 𝑣 , 𝑒 ⟩ ∈ ComplUSGraph ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ∧ 𝑛 ∈ 𝑣 ) ) → ( ♯ ‘ { 𝑐 ∈ ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) ∣ 𝑛 ∉ 𝑐 } ) = ( ♯ ‘ { 𝑐 ∈ ran 𝑒 ∣ 𝑛 ∉ 𝑐 } ) )
56 52 55 syl5eq ⊢ ( ( ( 𝑦 + 1 ) ∈ ℕ0 ∧ ( ⟨ 𝑣 , 𝑒 ⟩ ∈ ComplUSGraph ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ∧ 𝑛 ∈ 𝑣 ) ) → ( ♯ ‘ ran ( I ↾ { 𝑐 ∈ ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) ∣ 𝑛 ∉ 𝑐 } ) ) = ( ♯ ‘ { 𝑐 ∈ ran 𝑒 ∣ 𝑛 ∉ 𝑐 } ) )
57 56 eqeq1d ⊢ ( ( ( 𝑦 + 1 ) ∈ ℕ0 ∧ ( ⟨ 𝑣 , 𝑒 ⟩ ∈ ComplUSGraph ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ∧ 𝑛 ∈ 𝑣 ) ) → ( ( ♯ ‘ ran ( I ↾ { 𝑐 ∈ ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) ∣ 𝑛 ∉ 𝑐 } ) ) = ( ( ♯ ‘ ( 𝑣 ∖ { 𝑛 } ) ) C 2 ) ↔ ( ♯ ‘ { 𝑐 ∈ ran 𝑒 ∣ 𝑛 ∉ 𝑐 } ) = ( ( ♯ ‘ ( 𝑣 ∖ { 𝑛 } ) ) C 2 ) ) )
58 57 biimpd ⊢ ( ( ( 𝑦 + 1 ) ∈ ℕ0 ∧ ( ⟨ 𝑣 , 𝑒 ⟩ ∈ ComplUSGraph ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ∧ 𝑛 ∈ 𝑣 ) ) → ( ( ♯ ‘ ran ( I ↾ { 𝑐 ∈ ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) ∣ 𝑛 ∉ 𝑐 } ) ) = ( ( ♯ ‘ ( 𝑣 ∖ { 𝑛 } ) ) C 2 ) → ( ♯ ‘ { 𝑐 ∈ ran 𝑒 ∣ 𝑛 ∉ 𝑐 } ) = ( ( ♯ ‘ ( 𝑣 ∖ { 𝑛 } ) ) C 2 ) ) )
59 58 imdistani ⊢ ( ( ( ( 𝑦 + 1 ) ∈ ℕ0 ∧ ( ⟨ 𝑣 , 𝑒 ⟩ ∈ ComplUSGraph ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ∧ 𝑛 ∈ 𝑣 ) ) ∧ ( ♯ ‘ ran ( I ↾ { 𝑐 ∈ ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) ∣ 𝑛 ∉ 𝑐 } ) ) = ( ( ♯ ‘ ( 𝑣 ∖ { 𝑛 } ) ) C 2 ) ) → ( ( ( 𝑦 + 1 ) ∈ ℕ0 ∧ ( ⟨ 𝑣 , 𝑒 ⟩ ∈ ComplUSGraph ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ∧ 𝑛 ∈ 𝑣 ) ) ∧ ( ♯ ‘ { 𝑐 ∈ ran 𝑒 ∣ 𝑛 ∉ 𝑐 } ) = ( ( ♯ ‘ ( 𝑣 ∖ { 𝑛 } ) ) C 2 ) ) )
60 41 eqcomi ⊢ ran 𝑒 = ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ )
61 eqid ⊢ { 𝑐 ∈ ran 𝑒 ∣ 𝑛 ∉ 𝑐 } = { 𝑐 ∈ ran 𝑒 ∣ 𝑛 ∉ 𝑐 }
62 28 60 61 cusgrsize2inds ⊢ ( ( 𝑦 + 1 ) ∈ ℕ0 → ( ( ⟨ 𝑣 , 𝑒 ⟩ ∈ ComplUSGraph ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ∧ 𝑛 ∈ 𝑣 ) → ( ( ♯ ‘ { 𝑐 ∈ ran 𝑒 ∣ 𝑛 ∉ 𝑐 } ) = ( ( ♯ ‘ ( 𝑣 ∖ { 𝑛 } ) ) C 2 ) → ( ♯ ‘ ran 𝑒 ) = ( ( ♯ ‘ 𝑣 ) C 2 ) ) ) )
63 62 imp31 ⊢ ( ( ( ( 𝑦 + 1 ) ∈ ℕ0 ∧ ( ⟨ 𝑣 , 𝑒 ⟩ ∈ ComplUSGraph ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ∧ 𝑛 ∈ 𝑣 ) ) ∧ ( ♯ ‘ { 𝑐 ∈ ran 𝑒 ∣ 𝑛 ∉ 𝑐 } ) = ( ( ♯ ‘ ( 𝑣 ∖ { 𝑛 } ) ) C 2 ) ) → ( ♯ ‘ ran 𝑒 ) = ( ( ♯ ‘ 𝑣 ) C 2 ) )
64 59 63 syl ⊢ ( ( ( ( 𝑦 + 1 ) ∈ ℕ0 ∧ ( ⟨ 𝑣 , 𝑒 ⟩ ∈ ComplUSGraph ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ∧ 𝑛 ∈ 𝑣 ) ) ∧ ( ♯ ‘ ran ( I ↾ { 𝑐 ∈ ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) ∣ 𝑛 ∉ 𝑐 } ) ) = ( ( ♯ ‘ ( 𝑣 ∖ { 𝑛 } ) ) C 2 ) ) → ( ♯ ‘ ran 𝑒 ) = ( ( ♯ ‘ 𝑣 ) C 2 ) )
65 10 14 19 24 32 39 50 64 opfi1ind ⊢ ( ( ⟨ 𝑉 , ( iEdg ‘ 𝐺 ) ⟩ ∈ ComplUSGraph ∧ 𝑉 ∈ Fin ) → ( ♯ ‘ ran ( iEdg ‘ 𝐺 ) ) = ( ( ♯ ‘ 𝑉 ) C 2 ) )
66 9 65 sylan ⊢ ( ( 𝐺 ∈ ComplUSGraph ∧ 𝑉 ∈ Fin ) → ( ♯ ‘ ran ( iEdg ‘ 𝐺 ) ) = ( ( ♯ ‘ 𝑉 ) C 2 ) )
67 6 66 eqtrd ⊢ ( ( 𝐺 ∈ ComplUSGraph ∧ 𝑉 ∈ Fin ) → ( ♯ ‘ 𝐸 ) = ( ( ♯ ‘ 𝑉 ) C 2 ) )