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	$⊢ V = Vtx (G)$
	cusgrsizeindb0.e	$⊢ E = Edg (G)$
Assertion	cusgrsize	$⊢ (G \in ComplUSGraph \land V \in Fin) \to \|E\| = (\binom{\|V\|}{2})$

Proof

Step	Hyp	Ref	Expression
1		cusgrsizeindb0.v	$⊢ V = Vtx (G)$
2		cusgrsizeindb0.e	$⊢ E = Edg (G)$
3		edgval	$⊢ Edg (G) = ran iEdg (G)$
4	2 3	eqtri	$⊢ E = ran iEdg (G)$
5	4	a1i	$⊢ (G \in ComplUSGraph \land V \in Fin) \to E = ran iEdg (G)$
6	5	fveq2d	$⊢ (G \in ComplUSGraph \land V \in Fin) \to \|E\| = \|ran iEdg (G)\|$
7	1	opeq1i	$⊢ ⟨V, iEdg (G)⟩ = ⟨Vtx (G), iEdg (G)⟩$
8		cusgrop	$⊢ G \in ComplUSGraph \to ⟨Vtx (G), iEdg (G)⟩ \in ComplUSGraph$
9	7 8	eqeltrid	$⊢ G \in ComplUSGraph \to ⟨V, iEdg (G)⟩ \in ComplUSGraph$
10		fvex	$⊢ iEdg (G) \in V$
11		fvex	$⊢ Edg (⟨v, e⟩) \in V$
12		rabexg	$⊢ Edg (⟨v, e⟩) \in V \to \{c \in Edg (⟨v, e⟩) \| n \notin c\} \in V$
13	12	resiexd	$⊢ Edg (⟨v, e⟩) \in V \to {I ↾}_{\{c \in Edg (⟨v, e⟩) \| n \notin c\}} \in V$
14	11 13	ax-mp	$⊢ {I ↾}_{\{c \in Edg (⟨v, e⟩) \| n \notin c\}} \in V$
15		rneq	$⊢ e = iEdg (G) \to ran e = ran iEdg (G)$
16	15	fveq2d	$⊢ e = iEdg (G) \to \|ran e\| = \|ran iEdg (G)\|$
17		fveq2	$⊢ v = V \to \|v\| = \|V\|$
18	17	oveq1d	$⊢ v = V \to (\binom{\|v\|}{2}) = (\binom{\|V\|}{2})$
19	16 18	eqeqan12rd	$⊢ (v = V \land e = iEdg (G)) \to (\|ran e\| = (\binom{\|v\|}{2}) \leftrightarrow \|ran iEdg (G)\| = (\binom{\|V\|}{2}))$
20		rneq	$⊢ e = f \to ran e = ran f$
21	20	fveq2d	$⊢ e = f \to \|ran e\| = \|ran f\|$
22		fveq2	$⊢ v = w \to \|v\| = \|w\|$
23	22	oveq1d	$⊢ v = w \to (\binom{\|v\|}{2}) = (\binom{\|w\|}{2})$
24	21 23	eqeqan12rd	$⊢ (v = w \land e = f) \to (\|ran e\| = (\binom{\|v\|}{2}) \leftrightarrow \|ran f\| = (\binom{\|w\|}{2}))$
25		vex	$⊢ v \in V$
26		vex	$⊢ e \in V$
27	25 26	opvtxfvi	$⊢ Vtx (⟨v, e⟩) = v$
28	27	eqcomi	$⊢ v = Vtx (⟨v, e⟩)$
29		eqid	$⊢ Edg (⟨v, e⟩) = Edg (⟨v, e⟩)$
30		eqid	$⊢ \{c \in Edg (⟨v, e⟩) \| n \notin c\} = \{c \in Edg (⟨v, e⟩) \| n \notin c\}$
31		eqid	$⊢ ⟨v ∖ \{n\}, {I ↾}_{\{c \in Edg (⟨v, e⟩) \| n \notin c\}}⟩ = ⟨v ∖ \{n\}, {I ↾}_{\{c \in Edg (⟨v, e⟩) \| n \notin c\}}⟩$
32	28 29 30 31	cusgrres	$⊢ (⟨v, e⟩ \in ComplUSGraph \land n \in v) \to ⟨v ∖ \{n\}, {I ↾}_{\{c \in Edg (⟨v, e⟩) \| n \notin c\}}⟩ \in ComplUSGraph$
33		rneq	$⊢ f = {I ↾}_{\{c \in Edg (⟨v, e⟩) \| n \notin c\}} \to ran f = ran ({I ↾}_{\{c \in Edg (⟨v, e⟩) \| n \notin c\}})$
34	33	fveq2d	$⊢ f = {I ↾}_{\{c \in Edg (⟨v, e⟩) \| n \notin c\}} \to \|ran f\| = \|ran ({I ↾}_{\{c \in Edg (⟨v, e⟩) \| n \notin c\}})\|$
35	34	adantl	$⊢ (w = v ∖ \{n\} \land f = {I ↾}_{\{c \in Edg (⟨v, e⟩) \| n \notin c\}}) \to \|ran f\| = \|ran ({I ↾}_{\{c \in Edg (⟨v, e⟩) \| n \notin c\}})\|$
36		fveq2	$⊢ w = v ∖ \{n\} \to \|w\| = \|v ∖ \{n\}\|$
37	36	adantr	$⊢ (w = v ∖ \{n\} \land f = {I ↾}_{\{c \in Edg (⟨v, e⟩) \| n \notin c\}}) \to \|w\| = \|v ∖ \{n\}\|$
38	37	oveq1d	$⊢ (w = v ∖ \{n\} \land f = {I ↾}_{\{c \in Edg (⟨v, e⟩) \| n \notin c\}}) \to (\binom{\|w\|}{2}) = (\binom{\|v ∖ \{n\}\|}{2})$
39	35 38	eqeq12d	$⊢ (w = v ∖ \{n\} \land f = {I ↾}_{\{c \in Edg (⟨v, e⟩) \| n \notin c\}}) \to (\|ran f\| = (\binom{\|w\|}{2}) \leftrightarrow \|ran ({I ↾}_{\{c \in Edg (⟨v, e⟩) \| n \notin c\}})\| = (\binom{\|v ∖ \{n\}\|}{2}))$
40		edgopval	$⊢ (v \in V \land e \in V) \to Edg (⟨v, e⟩) = ran e$
41	40	el2v	$⊢ Edg (⟨v, e⟩) = ran e$
42	41	a1i	$⊢ (⟨v, e⟩ \in ComplUSGraph \land \|v\| = 0) \to Edg (⟨v, e⟩) = ran e$
43	42	eqcomd	$⊢ (⟨v, e⟩ \in ComplUSGraph \land \|v\| = 0) \to ran e = Edg (⟨v, e⟩)$
44	43	fveq2d	$⊢ (⟨v, e⟩ \in ComplUSGraph \land \|v\| = 0) \to \|ran e\| = \|Edg (⟨v, e⟩)\|$
45		cusgrusgr	$⊢ ⟨v, e⟩ \in ComplUSGraph \to ⟨v, e⟩ \in USGraph$
46		usgruhgr	$⊢ ⟨v, e⟩ \in USGraph \to ⟨v, e⟩ \in UHGraph$
47	45 46	syl	$⊢ ⟨v, e⟩ \in ComplUSGraph \to ⟨v, e⟩ \in UHGraph$
48	28 29	cusgrsizeindb0	$⊢ (⟨v, e⟩ \in UHGraph \land \|v\| = 0) \to \|Edg (⟨v, e⟩)\| = (\binom{\|v\|}{2})$
49	47 48	sylan	$⊢ (⟨v, e⟩ \in ComplUSGraph \land \|v\| = 0) \to \|Edg (⟨v, e⟩)\| = (\binom{\|v\|}{2})$
50	44 49	eqtrd	$⊢ (⟨v, e⟩ \in ComplUSGraph \land \|v\| = 0) \to \|ran e\| = (\binom{\|v\|}{2})$
51		rnresi	$⊢ ran ({I ↾}_{\{c \in Edg (⟨v, e⟩) \| n \notin c\}}) = \{c \in Edg (⟨v, e⟩) \| n \notin c\}$
52	51	fveq2i	$⊢ \|ran ({I ↾}_{\{c \in Edg (⟨v, e⟩) \| n \notin c\}})\| = \|\{c \in Edg (⟨v, e⟩) \| n \notin c\}\|$
53	41	a1i	$⊢ (y + 1 \in ℕ_{0} \land (⟨v, e⟩ \in ComplUSGraph \land \|v\| = y + 1 \land n \in v)) \to Edg (⟨v, e⟩) = ran e$
54	53	rabeqdv	$⊢ (y + 1 \in ℕ_{0} \land (⟨v, e⟩ \in ComplUSGraph \land \|v\| = y + 1 \land n \in v)) \to \{c \in Edg (⟨v, e⟩) \| n \notin c\} = \{c \in ran e \| n \notin c\}$
55	54	fveq2d	$⊢ (y + 1 \in ℕ_{0} \land (⟨v, e⟩ \in ComplUSGraph \land \|v\| = y + 1 \land n \in v)) \to \|\{c \in Edg (⟨v, e⟩) \| n \notin c\}\| = \|\{c \in ran e \| n \notin c\}\|$
56	52 55	syl5eq	$⊢ (y + 1 \in ℕ_{0} \land (⟨v, e⟩ \in ComplUSGraph \land \|v\| = y + 1 \land n \in v)) \to \|ran ({I ↾}_{\{c \in Edg (⟨v, e⟩) \| n \notin c\}})\| = \|\{c \in ran e \| n \notin c\}\|$
57	56	eqeq1d	$⊢ (y + 1 \in ℕ_{0} \land (⟨v, e⟩ \in ComplUSGraph \land \|v\| = y + 1 \land n \in v)) \to (\|ran ({I ↾}_{\{c \in Edg (⟨v, e⟩) \| n \notin c\}})\| = (\binom{\|v ∖ \{n\}\|}{2}) \leftrightarrow \|\{c \in ran e \| n \notin c\}\| = (\binom{\|v ∖ \{n\}\|}{2}))$
58	57	biimpd	$⊢ (y + 1 \in ℕ_{0} \land (⟨v, e⟩ \in ComplUSGraph \land \|v\| = y + 1 \land n \in v)) \to (\|ran ({I ↾}_{\{c \in Edg (⟨v, e⟩) \| n \notin c\}})\| = (\binom{\|v ∖ \{n\}\|}{2}) \to \|\{c \in ran e \| n \notin c\}\| = (\binom{\|v ∖ \{n\}\|}{2}))$
59	58	imdistani	$⊢ ((y + 1 \in ℕ_{0} \land (⟨v, e⟩ \in ComplUSGraph \land \|v\| = y + 1 \land n \in v)) \land \|ran ({I ↾}_{\{c \in Edg (⟨v, e⟩) \| n \notin c\}})\| = (\binom{\|v ∖ \{n\}\|}{2})) \to ((y + 1 \in ℕ_{0} \land (⟨v, e⟩ \in ComplUSGraph \land \|v\| = y + 1 \land n \in v)) \land \|\{c \in ran e \| n \notin c\}\| = (\binom{\|v ∖ \{n\}\|}{2}))$
60	41	eqcomi	$⊢ ran e = Edg (⟨v, e⟩)$
61		eqid	$⊢ \{c \in ran e \| n \notin c\} = \{c \in ran e \| n \notin c\}$
62	28 60 61	cusgrsize2inds	$⊢ y + 1 \in ℕ_{0} \to ((⟨v, e⟩ \in ComplUSGraph \land \|v\| = y + 1 \land n \in v) \to (\|\{c \in ran e \| n \notin c\}\| = (\binom{\|v ∖ \{n\}\|}{2}) \to \|ran e\| = (\binom{\|v\|}{2})))$
63	62	imp31	$⊢ ((y + 1 \in ℕ_{0} \land (⟨v, e⟩ \in ComplUSGraph \land \|v\| = y + 1 \land n \in v)) \land \|\{c \in ran e \| n \notin c\}\| = (\binom{\|v ∖ \{n\}\|}{2})) \to \|ran e\| = (\binom{\|v\|}{2})$
64	59 63	syl	$⊢ ((y + 1 \in ℕ_{0} \land (⟨v, e⟩ \in ComplUSGraph \land \|v\| = y + 1 \land n \in v)) \land \|ran ({I ↾}_{\{c \in Edg (⟨v, e⟩) \| n \notin c\}})\| = (\binom{\|v ∖ \{n\}\|}{2})) \to \|ran e\| = (\binom{\|v\|}{2})$
65	10 14 19 24 32 39 50 64	opfi1ind	$⊢ (⟨V, iEdg (G)⟩ \in ComplUSGraph \land V \in Fin) \to \|ran iEdg (G)\| = (\binom{\|V\|}{2})$
66	9 65	sylan	$⊢ (G \in ComplUSGraph \land V \in Fin) \to \|ran iEdg (G)\| = (\binom{\|V\|}{2})$
67	6 66	eqtrd	$⊢ (G \in ComplUSGraph \land V \in Fin) \to \|E\| = (\binom{\|V\|}{2})$

Metamath Proof Explorer

Theorem cusgrsize

Proof