Theorem cusgrsize2inds 26953

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

Hypotheses

Ref	Expression
cusgrsizeindb0.v	⊢ 𝑉 = (Vtx‘𝐺)
cusgrsizeindb0.e	⊢ 𝐸 = (Edg‘𝐺)
cusgrsizeinds.f	⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒}

Assertion

Ref	Expression
cusgrsize2inds	⊢ (𝑌 ∈ ℕ0 → ((𝐺 ∈ ComplUSGraph ∧ (♯‘𝑉) = 𝑌 ∧ 𝑁 ∈ 𝑉) → ((♯‘𝐹) = ((♯‘(𝑉 ∖ {𝑁}))C2) → (♯‘𝐸) = ((♯‘𝑉)C2))))

Distinct variable groups:   𝑒,𝐸   𝑒,𝐺   𝑒,𝑁   𝑒,𝑉

Allowed substitution hints:   𝐹(𝑒)   𝑌(𝑒)

Proof of Theorem cusgrsize2inds

Step	Hyp	Ref	Expression
1		cusgrsizeindb0.v	. . . . 5 ⊢ 𝑉 = (Vtx‘𝐺)
2	1	fvexi 6510	. . . 4 ⊢ 𝑉 ∈ V
3		hashnn0n0nn 13563	. . . . . . . 8 ⊢ (((𝑉 ∈ V ∧ 𝑌 ∈ ℕ0) ∧ ((♯‘𝑉) = 𝑌 ∧ 𝑁 ∈ 𝑉)) → 𝑌 ∈ ℕ)
4	3	anassrs 460	. . . . . . 7 ⊢ ((((𝑉 ∈ V ∧ 𝑌 ∈ ℕ0) ∧ (♯‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) → 𝑌 ∈ ℕ)
5		simplll 763	. . . . . . . . . . 11 ⊢ ((((𝑉 ∈ V ∧ (♯‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) ∧ 𝑌 ∈ ℕ) → 𝑉 ∈ V)
6		simplr 757	. . . . . . . . . . 11 ⊢ ((((𝑉 ∈ V ∧ (♯‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) ∧ 𝑌 ∈ ℕ) → 𝑁 ∈ 𝑉)
7		eleq1 2846	. . . . . . . . . . . . . . 15 ⊢ (𝑌 = (♯‘𝑉) → (𝑌 ∈ ℕ ↔ (♯‘𝑉) ∈ ℕ))
8	7	eqcoms 2779	. . . . . . . . . . . . . 14 ⊢ ((♯‘𝑉) = 𝑌 → (𝑌 ∈ ℕ ↔ (♯‘𝑉) ∈ ℕ))
9		nnm1nn0 11748	. . . . . . . . . . . . . 14 ⊢ ((♯‘𝑉) ∈ ℕ → ((♯‘𝑉) − 1) ∈ ℕ0)
10	8, 9	syl6bi 245	. . . . . . . . . . . . 13 ⊢ ((♯‘𝑉) = 𝑌 → (𝑌 ∈ ℕ → ((♯‘𝑉) − 1) ∈ ℕ0))
11	10	ad2antlr 715	. . . . . . . . . . . 12 ⊢ (((𝑉 ∈ V ∧ (♯‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) → (𝑌 ∈ ℕ → ((♯‘𝑉) − 1) ∈ ℕ0))
12	11	imp 398	. . . . . . . . . . 11 ⊢ ((((𝑉 ∈ V ∧ (♯‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) ∧ 𝑌 ∈ ℕ) → ((♯‘𝑉) − 1) ∈ ℕ0)
13		nncn 11446	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘𝑉) ∈ ℕ → (♯‘𝑉) ∈ ℂ)
14		1cnd 10432	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘𝑉) ∈ ℕ → 1 ∈ ℂ)
15	13, 14	npcand 10800	. . . . . . . . . . . . . . 15 ⊢ ((♯‘𝑉) ∈ ℕ → (((♯‘𝑉) − 1) + 1) = (♯‘𝑉))
16	15	eqcomd 2777	. . . . . . . . . . . . . 14 ⊢ ((♯‘𝑉) ∈ ℕ → (♯‘𝑉) = (((♯‘𝑉) − 1) + 1))
17	8, 16	syl6bi 245	. . . . . . . . . . . . 13 ⊢ ((♯‘𝑉) = 𝑌 → (𝑌 ∈ ℕ → (♯‘𝑉) = (((♯‘𝑉) − 1) + 1)))
18	17	ad2antlr 715	. . . . . . . . . . . 12 ⊢ (((𝑉 ∈ V ∧ (♯‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) → (𝑌 ∈ ℕ → (♯‘𝑉) = (((♯‘𝑉) − 1) + 1)))
19	18	imp 398	. . . . . . . . . . 11 ⊢ ((((𝑉 ∈ V ∧ (♯‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) ∧ 𝑌 ∈ ℕ) → (♯‘𝑉) = (((♯‘𝑉) − 1) + 1))
20		hashdifsnp1 13663	. . . . . . . . . . . 12 ⊢ ((𝑉 ∈ V ∧ 𝑁 ∈ 𝑉 ∧ ((♯‘𝑉) − 1) ∈ ℕ0) → ((♯‘𝑉) = (((♯‘𝑉) − 1) + 1) → (♯‘(𝑉 ∖ {𝑁})) = ((♯‘𝑉) − 1)))
21	20	imp 398	. . . . . . . . . . 11 ⊢ (((𝑉 ∈ V ∧ 𝑁 ∈ 𝑉 ∧ ((♯‘𝑉) − 1) ∈ ℕ0) ∧ (♯‘𝑉) = (((♯‘𝑉) − 1) + 1)) → (♯‘(𝑉 ∖ {𝑁})) = ((♯‘𝑉) − 1))
22	5, 6, 12, 19, 21	syl31anc 1354	. . . . . . . . . 10 ⊢ ((((𝑉 ∈ V ∧ (♯‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) ∧ 𝑌 ∈ ℕ) → (♯‘(𝑉 ∖ {𝑁})) = ((♯‘𝑉) − 1))
23		oveq1 6981	. . . . . . . . . . . . 13 ⊢ ((♯‘(𝑉 ∖ {𝑁})) = ((♯‘𝑉) − 1) → ((♯‘(𝑉 ∖ {𝑁}))C2) = (((♯‘𝑉) − 1)C2))
24	23	eqeq2d 2781	. . . . . . . . . . . 12 ⊢ ((♯‘(𝑉 ∖ {𝑁})) = ((♯‘𝑉) − 1) → ((♯‘𝐹) = ((♯‘(𝑉 ∖ {𝑁}))C2) ↔ (♯‘𝐹) = (((♯‘𝑉) − 1)C2)))
25	8	ad2antlr 715	. . . . . . . . . . . . . . 15 ⊢ (((𝑉 ∈ V ∧ (♯‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) → (𝑌 ∈ ℕ ↔ (♯‘𝑉) ∈ ℕ))
26		nnnn0 11713	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((♯‘𝑉) ∈ ℕ → (♯‘𝑉) ∈ ℕ0)
27		hashclb 13532	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑉 ∈ V → (𝑉 ∈ Fin ↔ (♯‘𝑉) ∈ ℕ0))
28	26, 27	syl5ibrcom 239	. . . . . . . . . . . . . . . . . . 19 ⊢ ((♯‘𝑉) ∈ ℕ → (𝑉 ∈ V → 𝑉 ∈ Fin))
29		cusgrsizeindb0.e	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝐸 = (Edg‘𝐺)
30		cusgrsizeinds.f	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒}
31	1, 29, 30	cusgrsizeinds 26952	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐺 ∈ ComplUSGraph ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (♯‘𝐸) = (((♯‘𝑉) − 1) + (♯‘𝐹)))
32		oveq2 6982	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((♯‘𝐹) = (((♯‘𝑉) − 1)C2) → (((♯‘𝑉) − 1) + (♯‘𝐹)) = (((♯‘𝑉) − 1) + (((♯‘𝑉) − 1)C2)))
33	32	eqeq2d 2781	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((♯‘𝐹) = (((♯‘𝑉) − 1)C2) → ((♯‘𝐸) = (((♯‘𝑉) − 1) + (♯‘𝐹)) ↔ (♯‘𝐸) = (((♯‘𝑉) − 1) + (((♯‘𝑉) − 1)C2))))
34	33	adantl 474	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((♯‘𝑉) ∈ ℕ ∧ (♯‘𝐹) = (((♯‘𝑉) − 1)C2)) → ((♯‘𝐸) = (((♯‘𝑉) − 1) + (♯‘𝐹)) ↔ (♯‘𝐸) = (((♯‘𝑉) − 1) + (((♯‘𝑉) − 1)C2))))
35		bcn2m1 13497	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((♯‘𝑉) ∈ ℕ → (((♯‘𝑉) − 1) + (((♯‘𝑉) − 1)C2)) = ((♯‘𝑉)C2))
36	35	eqeq2d 2781	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((♯‘𝑉) ∈ ℕ → ((♯‘𝐸) = (((♯‘𝑉) − 1) + (((♯‘𝑉) − 1)C2)) ↔ (♯‘𝐸) = ((♯‘𝑉)C2)))
37	36	biimpd 221	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((♯‘𝑉) ∈ ℕ → ((♯‘𝐸) = (((♯‘𝑉) − 1) + (((♯‘𝑉) − 1)C2)) → (♯‘𝐸) = ((♯‘𝑉)C2)))
38	37	adantr 473	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((♯‘𝑉) ∈ ℕ ∧ (♯‘𝐹) = (((♯‘𝑉) − 1)C2)) → ((♯‘𝐸) = (((♯‘𝑉) − 1) + (((♯‘𝑉) − 1)C2)) → (♯‘𝐸) = ((♯‘𝑉)C2)))
39	34, 38	sylbid 232	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((♯‘𝑉) ∈ ℕ ∧ (♯‘𝐹) = (((♯‘𝑉) − 1)C2)) → ((♯‘𝐸) = (((♯‘𝑉) − 1) + (♯‘𝐹)) → (♯‘𝐸) = ((♯‘𝑉)C2)))
40	39	ex 405	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((♯‘𝑉) ∈ ℕ → ((♯‘𝐹) = (((♯‘𝑉) − 1)C2) → ((♯‘𝐸) = (((♯‘𝑉) − 1) + (♯‘𝐹)) → (♯‘𝐸) = ((♯‘𝑉)C2))))
41	40	com3r 87	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((♯‘𝐸) = (((♯‘𝑉) − 1) + (♯‘𝐹)) → ((♯‘𝑉) ∈ ℕ → ((♯‘𝐹) = (((♯‘𝑉) − 1)C2) → (♯‘𝐸) = ((♯‘𝑉)C2))))
42	31, 41	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐺 ∈ ComplUSGraph ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → ((♯‘𝑉) ∈ ℕ → ((♯‘𝐹) = (((♯‘𝑉) − 1)C2) → (♯‘𝐸) = ((♯‘𝑉)C2))))
43	42	3exp 1100	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐺 ∈ ComplUSGraph → (𝑉 ∈ Fin → (𝑁 ∈ 𝑉 → ((♯‘𝑉) ∈ ℕ → ((♯‘𝐹) = (((♯‘𝑉) − 1)C2) → (♯‘𝐸) = ((♯‘𝑉)C2))))))
44	43	com14 96	. . . . . . . . . . . . . . . . . . 19 ⊢ ((♯‘𝑉) ∈ ℕ → (𝑉 ∈ Fin → (𝑁 ∈ 𝑉 → (𝐺 ∈ ComplUSGraph → ((♯‘𝐹) = (((♯‘𝑉) − 1)C2) → (♯‘𝐸) = ((♯‘𝑉)C2))))))
45	28, 44	syldc 48	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑉 ∈ V → ((♯‘𝑉) ∈ ℕ → (𝑁 ∈ 𝑉 → (𝐺 ∈ ComplUSGraph → ((♯‘𝐹) = (((♯‘𝑉) − 1)C2) → (♯‘𝐸) = ((♯‘𝑉)C2))))))
46	45	com23 86	. . . . . . . . . . . . . . . . 17 ⊢ (𝑉 ∈ V → (𝑁 ∈ 𝑉 → ((♯‘𝑉) ∈ ℕ → (𝐺 ∈ ComplUSGraph → ((♯‘𝐹) = (((♯‘𝑉) − 1)C2) → (♯‘𝐸) = ((♯‘𝑉)C2))))))
47	46	adantr 473	. . . . . . . . . . . . . . . 16 ⊢ ((𝑉 ∈ V ∧ (♯‘𝑉) = 𝑌) → (𝑁 ∈ 𝑉 → ((♯‘𝑉) ∈ ℕ → (𝐺 ∈ ComplUSGraph → ((♯‘𝐹) = (((♯‘𝑉) − 1)C2) → (♯‘𝐸) = ((♯‘𝑉)C2))))))
48	47	imp 398	. . . . . . . . . . . . . . 15 ⊢ (((𝑉 ∈ V ∧ (♯‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) → ((♯‘𝑉) ∈ ℕ → (𝐺 ∈ ComplUSGraph → ((♯‘𝐹) = (((♯‘𝑉) − 1)C2) → (♯‘𝐸) = ((♯‘𝑉)C2)))))
49	25, 48	sylbid 232	. . . . . . . . . . . . . 14 ⊢ (((𝑉 ∈ V ∧ (♯‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) → (𝑌 ∈ ℕ → (𝐺 ∈ ComplUSGraph → ((♯‘𝐹) = (((♯‘𝑉) − 1)C2) → (♯‘𝐸) = ((♯‘𝑉)C2)))))
50	49	imp 398	. . . . . . . . . . . . 13 ⊢ ((((𝑉 ∈ V ∧ (♯‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) ∧ 𝑌 ∈ ℕ) → (𝐺 ∈ ComplUSGraph → ((♯‘𝐹) = (((♯‘𝑉) − 1)C2) → (♯‘𝐸) = ((♯‘𝑉)C2))))
51	50	com13 88	. . . . . . . . . . . 12 ⊢ ((♯‘𝐹) = (((♯‘𝑉) − 1)C2) → (𝐺 ∈ ComplUSGraph → ((((𝑉 ∈ V ∧ (♯‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) ∧ 𝑌 ∈ ℕ) → (♯‘𝐸) = ((♯‘𝑉)C2))))
52	24, 51	syl6bi 245	. . . . . . . . . . 11 ⊢ ((♯‘(𝑉 ∖ {𝑁})) = ((♯‘𝑉) − 1) → ((♯‘𝐹) = ((♯‘(𝑉 ∖ {𝑁}))C2) → (𝐺 ∈ ComplUSGraph → ((((𝑉 ∈ V ∧ (♯‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) ∧ 𝑌 ∈ ℕ) → (♯‘𝐸) = ((♯‘𝑉)C2)))))
53	52	com24 95	. . . . . . . . . 10 ⊢ ((♯‘(𝑉 ∖ {𝑁})) = ((♯‘𝑉) − 1) → ((((𝑉 ∈ V ∧ (♯‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) ∧ 𝑌 ∈ ℕ) → (𝐺 ∈ ComplUSGraph → ((♯‘𝐹) = ((♯‘(𝑉 ∖ {𝑁}))C2) → (♯‘𝐸) = ((♯‘𝑉)C2)))))
54	22, 53	mpcom 38	. . . . . . . . 9 ⊢ ((((𝑉 ∈ V ∧ (♯‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) ∧ 𝑌 ∈ ℕ) → (𝐺 ∈ ComplUSGraph → ((♯‘𝐹) = ((♯‘(𝑉 ∖ {𝑁}))C2) → (♯‘𝐸) = ((♯‘𝑉)C2))))
55	54	ex 405	. . . . . . . 8 ⊢ (((𝑉 ∈ V ∧ (♯‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) → (𝑌 ∈ ℕ → (𝐺 ∈ ComplUSGraph → ((♯‘𝐹) = ((♯‘(𝑉 ∖ {𝑁}))C2) → (♯‘𝐸) = ((♯‘𝑉)C2)))))
56	55	adantllr 707	. . . . . . 7 ⊢ ((((𝑉 ∈ V ∧ 𝑌 ∈ ℕ0) ∧ (♯‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) → (𝑌 ∈ ℕ → (𝐺 ∈ ComplUSGraph → ((♯‘𝐹) = ((♯‘(𝑉 ∖ {𝑁}))C2) → (♯‘𝐸) = ((♯‘𝑉)C2)))))
57	4, 56	mpd 15	. . . . . 6 ⊢ ((((𝑉 ∈ V ∧ 𝑌 ∈ ℕ0) ∧ (♯‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) → (𝐺 ∈ ComplUSGraph → ((♯‘𝐹) = ((♯‘(𝑉 ∖ {𝑁}))C2) → (♯‘𝐸) = ((♯‘𝑉)C2))))
58	57	exp41 427	. . . . 5 ⊢ (𝑉 ∈ V → (𝑌 ∈ ℕ0 → ((♯‘𝑉) = 𝑌 → (𝑁 ∈ 𝑉 → (𝐺 ∈ ComplUSGraph → ((♯‘𝐹) = ((♯‘(𝑉 ∖ {𝑁}))C2) → (♯‘𝐸) = ((♯‘𝑉)C2)))))))
59	58	com25 99	. . . 4 ⊢ (𝑉 ∈ V → (𝐺 ∈ ComplUSGraph → ((♯‘𝑉) = 𝑌 → (𝑁 ∈ 𝑉 → (𝑌 ∈ ℕ0 → ((♯‘𝐹) = ((♯‘(𝑉 ∖ {𝑁}))C2) → (♯‘𝐸) = ((♯‘𝑉)C2)))))))
60	2, 59	ax-mp 5	. . 3 ⊢ (𝐺 ∈ ComplUSGraph → ((♯‘𝑉) = 𝑌 → (𝑁 ∈ 𝑉 → (𝑌 ∈ ℕ0 → ((♯‘𝐹) = ((♯‘(𝑉 ∖ {𝑁}))C2) → (♯‘𝐸) = ((♯‘𝑉)C2))))))
61	60	3imp 1092	. 2 ⊢ ((𝐺 ∈ ComplUSGraph ∧ (♯‘𝑉) = 𝑌 ∧ 𝑁 ∈ 𝑉) → (𝑌 ∈ ℕ0 → ((♯‘𝐹) = ((♯‘(𝑉 ∖ {𝑁}))C2) → (♯‘𝐸) = ((♯‘𝑉)C2))))
62	61	com12 32	1 ⊢ (𝑌 ∈ ℕ0 → ((𝐺 ∈ ComplUSGraph ∧ (♯‘𝑉) = 𝑌 ∧ 𝑁 ∈ 𝑉) → ((♯‘𝐹) = ((♯‘(𝑉 ∖ {𝑁}))C2) → (♯‘𝐸) = ((♯‘𝑉)C2))))

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 387   ∧ w3a 1069   = wceq 1508   ∈ wcel 2051   ∉ wnel 3066  {crab 3085  Vcvv 3408   ∖ cdif 3819  {csn 4435  ‘cfv 6185  (class class class)co 6974  Fincfn 8304  1c1 10334   + caddc 10336   − cmin 10668  ℕcn 11437  2c2 11493  ℕ₀cn0 11705  Ccbc 13475  ♯chash 13503  Vtxcvtx 26499  Edgcedg 26550  ComplUSGraphccusgr 26910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2743  ax-rep 5045  ax-sep 5056  ax-nul 5063  ax-pow 5115  ax-pr 5182  ax-un 7277  ax-cnex 10389  ax-resscn 10390  ax-1cn 10391  ax-icn 10392  ax-addcl 10393  ax-addrcl 10394  ax-mulcl 10395  ax-mulrcl 10396  ax-mulcom 10397  ax-addass 10398  ax-mulass 10399  ax-distr 10400  ax-i2m1 10401  ax-1ne0 10402  ax-1rid 10403  ax-rnegex 10404  ax-rrecex 10405  ax-cnre 10406  ax-pre-lttri 10407  ax-pre-lttrn 10408  ax-pre-ltadd 10409  ax-pre-mulgt0 10410

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3or 1070  df-3an 1071  df-tru 1511  df-fal 1521  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2548  df-eu 2585  df-clab 2752  df-cleq 2764  df-clel 2839  df-nfc 2911  df-ne 2961  df-nel 3067  df-ral 3086  df-rex 3087  df-reu 3088  df-rmo 3089  df-rab 3090  df-v 3410  df-sbc 3675  df-csb 3780  df-dif 3825  df-un 3827  df-in 3829  df-ss 3836  df-pss 3838  df-nul 4173  df-if 4345  df-pw 4418  df-sn 4436  df-pr 4438  df-tp 4440  df-op 4442  df-uni 4709  df-int 4746  df-iun 4790  df-br 4926  df-opab 4988  df-mpt 5005  df-tr 5027  df-id 5308  df-eprel 5313  df-po 5322  df-so 5323  df-fr 5362  df-we 5364  df-xp 5409  df-rel 5410  df-cnv 5411  df-co 5412  df-dm 5413  df-rn 5414  df-res 5415  df-ima 5416  df-pred 5983  df-ord 6029  df-on 6030  df-lim 6031  df-suc 6032  df-iota 6149  df-fun 6187  df-fn 6188  df-f 6189  df-f1 6190  df-fo 6191  df-f1o 6192  df-fv 6193  df-riota 6935  df-ov 6977  df-oprab 6978  df-mpo 6979  df-om 7395  df-1st 7499  df-2nd 7500  df-wrecs 7748  df-recs 7810  df-rdg 7848  df-1o 7903  df-2o 7904  df-oadd 7907  df-er 8087  df-en 8305  df-dom 8306  df-sdom 8307  df-fin 8308  df-dju 9122  df-card 9160  df-pnf 10474  df-mnf 10475  df-xr 10476  df-ltxr 10477  df-le 10478  df-sub 10670  df-neg 10671  df-div 11097  df-nn 11438  df-2 11501  df-n0 11706  df-xnn0 11778  df-z 11792  df-uz 12057  df-rp 12203  df-fz 12707  df-seq 13183  df-fac 13447  df-bc 13476  df-hash 13504  df-vtx 26501  df-iedg 26502  df-edg 26551  df-uhgr 26561  df-upgr 26585  df-umgr 26586  df-uspgr 26653  df-usgr 26654  df-fusgr 26817  df-nbgr 26833  df-uvtx 26886  df-cplgr 26911  df-cusgr 26912

This theorem is referenced by:  cusgrsize  26954