Theorem cusgrsize2inds 40668

Description: Induction step in cusgrasize 25769. 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		fvex 6095	. . . . 5 ⊢ (Vtx‘𝐺) ∈ V
3	1, 2	eqeltri 2680	. . . 4 ⊢ 𝑉 ∈ V
4		hashnn0n0nn 12990	. . . . . . . 8 ⊢ (((𝑉 ∈ V ∧ 𝑌 ∈ ℕ0) ∧ ((#‘𝑉) = 𝑌 ∧ 𝑁 ∈ 𝑉)) → 𝑌 ∈ ℕ)
5	4	anassrs 677	. . . . . . 7 ⊢ ((((𝑉 ∈ V ∧ 𝑌 ∈ ℕ0) ∧ (#‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) → 𝑌 ∈ ℕ)
6		simplll 793	. . . . . . . . . . 11 ⊢ ((((𝑉 ∈ V ∧ (#‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) ∧ 𝑌 ∈ ℕ) → 𝑉 ∈ V)
7		simplr 787	. . . . . . . . . . 11 ⊢ ((((𝑉 ∈ V ∧ (#‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) ∧ 𝑌 ∈ ℕ) → 𝑁 ∈ 𝑉)
8		eleq1 2672	. . . . . . . . . . . . . . 15 ⊢ (𝑌 = (#‘𝑉) → (𝑌 ∈ ℕ ↔ (#‘𝑉) ∈ ℕ))
9	8	eqcoms 2614	. . . . . . . . . . . . . 14 ⊢ ((#‘𝑉) = 𝑌 → (𝑌 ∈ ℕ ↔ (#‘𝑉) ∈ ℕ))
10		nnm1nn0 11178	. . . . . . . . . . . . . 14 ⊢ ((#‘𝑉) ∈ ℕ → ((#‘𝑉) − 1) ∈ ℕ0)
11	9, 10	syl6bi 241	. . . . . . . . . . . . 13 ⊢ ((#‘𝑉) = 𝑌 → (𝑌 ∈ ℕ → ((#‘𝑉) − 1) ∈ ℕ0))
12	11	ad2antlr 758	. . . . . . . . . . . 12 ⊢ (((𝑉 ∈ V ∧ (#‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) → (𝑌 ∈ ℕ → ((#‘𝑉) − 1) ∈ ℕ0))
13	12	imp 443	. . . . . . . . . . 11 ⊢ ((((𝑉 ∈ V ∧ (#‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) ∧ 𝑌 ∈ ℕ) → ((#‘𝑉) − 1) ∈ ℕ0)
14		nncn 10872	. . . . . . . . . . . . . . . 16 ⊢ ((#‘𝑉) ∈ ℕ → (#‘𝑉) ∈ ℂ)
15		1cnd 9909	. . . . . . . . . . . . . . . 16 ⊢ ((#‘𝑉) ∈ ℕ → 1 ∈ ℂ)
16	14, 15	npcand 10244	. . . . . . . . . . . . . . 15 ⊢ ((#‘𝑉) ∈ ℕ → (((#‘𝑉) − 1) + 1) = (#‘𝑉))
17	16	eqcomd 2612	. . . . . . . . . . . . . 14 ⊢ ((#‘𝑉) ∈ ℕ → (#‘𝑉) = (((#‘𝑉) − 1) + 1))
18	9, 17	syl6bi 241	. . . . . . . . . . . . 13 ⊢ ((#‘𝑉) = 𝑌 → (𝑌 ∈ ℕ → (#‘𝑉) = (((#‘𝑉) − 1) + 1)))
19	18	ad2antlr 758	. . . . . . . . . . . 12 ⊢ (((𝑉 ∈ V ∧ (#‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) → (𝑌 ∈ ℕ → (#‘𝑉) = (((#‘𝑉) − 1) + 1)))
20	19	imp 443	. . . . . . . . . . 11 ⊢ ((((𝑉 ∈ V ∧ (#‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) ∧ 𝑌 ∈ ℕ) → (#‘𝑉) = (((#‘𝑉) − 1) + 1))
21		brfi1indlem 13076	. . . . . . . . . . . 12 ⊢ ((𝑉 ∈ V ∧ 𝑁 ∈ 𝑉 ∧ ((#‘𝑉) − 1) ∈ ℕ0) → ((#‘𝑉) = (((#‘𝑉) − 1) + 1) → (#‘(𝑉 ∖ {𝑁})) = ((#‘𝑉) − 1)))
22	21	imp 443	. . . . . . . . . . 11 ⊢ (((𝑉 ∈ V ∧ 𝑁 ∈ 𝑉 ∧ ((#‘𝑉) − 1) ∈ ℕ0) ∧ (#‘𝑉) = (((#‘𝑉) − 1) + 1)) → (#‘(𝑉 ∖ {𝑁})) = ((#‘𝑉) − 1))
23	6, 7, 13, 20, 22	syl31anc 1320	. . . . . . . . . 10 ⊢ ((((𝑉 ∈ V ∧ (#‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) ∧ 𝑌 ∈ ℕ) → (#‘(𝑉 ∖ {𝑁})) = ((#‘𝑉) − 1))
24		oveq1 6531	. . . . . . . . . . . . 13 ⊢ ((#‘(𝑉 ∖ {𝑁})) = ((#‘𝑉) − 1) → ((#‘(𝑉 ∖ {𝑁}))C2) = (((#‘𝑉) − 1)C2))
25	24	eqeq2d 2616	. . . . . . . . . . . 12 ⊢ ((#‘(𝑉 ∖ {𝑁})) = ((#‘𝑉) − 1) → ((#‘𝐹) = ((#‘(𝑉 ∖ {𝑁}))C2) ↔ (#‘𝐹) = (((#‘𝑉) − 1)C2)))
26	9	ad2antlr 758	. . . . . . . . . . . . . . 15 ⊢ (((𝑉 ∈ V ∧ (#‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) → (𝑌 ∈ ℕ ↔ (#‘𝑉) ∈ ℕ))
27		nnnn0 11143	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((#‘𝑉) ∈ ℕ → (#‘𝑉) ∈ ℕ0)
28		hashclb 12960	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑉 ∈ V → (𝑉 ∈ Fin ↔ (#‘𝑉) ∈ ℕ0))
29	27, 28	syl5ibrcom 235	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((#‘𝑉) ∈ ℕ → (𝑉 ∈ V → 𝑉 ∈ Fin))
30	29	impcom 444	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑉 ∈ V ∧ (#‘𝑉) ∈ ℕ) → 𝑉 ∈ Fin)
31		cusgrsizeindb0.e	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝐸 = (Edg‘𝐺)
32		cusgrsizeinds.f	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒}
33	1, 31, 32	cusgrsizeinds 40667	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐺 ∈ ComplUSGraph ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (#‘𝐸) = (((#‘𝑉) − 1) + (#‘𝐹)))
34		oveq2 6532	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((#‘𝐹) = (((#‘𝑉) − 1)C2) → (((#‘𝑉) − 1) + (#‘𝐹)) = (((#‘𝑉) − 1) + (((#‘𝑉) − 1)C2)))
35	34	eqeq2d 2616	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((#‘𝐹) = (((#‘𝑉) − 1)C2) → ((#‘𝐸) = (((#‘𝑉) − 1) + (#‘𝐹)) ↔ (#‘𝐸) = (((#‘𝑉) − 1) + (((#‘𝑉) − 1)C2))))
36	35	adantl 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((#‘𝑉) ∈ ℕ ∧ (#‘𝐹) = (((#‘𝑉) − 1)C2)) → ((#‘𝐸) = (((#‘𝑉) − 1) + (#‘𝐹)) ↔ (#‘𝐸) = (((#‘𝑉) − 1) + (((#‘𝑉) − 1)C2))))
37		bcn2m1 12925	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((#‘𝑉) ∈ ℕ → (((#‘𝑉) − 1) + (((#‘𝑉) − 1)C2)) = ((#‘𝑉)C2))
38	37	eqeq2d 2616	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((#‘𝑉) ∈ ℕ → ((#‘𝐸) = (((#‘𝑉) − 1) + (((#‘𝑉) − 1)C2)) ↔ (#‘𝐸) = ((#‘𝑉)C2)))
39	38	biimpd 217	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((#‘𝑉) ∈ ℕ → ((#‘𝐸) = (((#‘𝑉) − 1) + (((#‘𝑉) − 1)C2)) → (#‘𝐸) = ((#‘𝑉)C2)))
40	39	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((#‘𝑉) ∈ ℕ ∧ (#‘𝐹) = (((#‘𝑉) − 1)C2)) → ((#‘𝐸) = (((#‘𝑉) − 1) + (((#‘𝑉) − 1)C2)) → (#‘𝐸) = ((#‘𝑉)C2)))
41	36, 40	sylbid 228	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((#‘𝑉) ∈ ℕ ∧ (#‘𝐹) = (((#‘𝑉) − 1)C2)) → ((#‘𝐸) = (((#‘𝑉) − 1) + (#‘𝐹)) → (#‘𝐸) = ((#‘𝑉)C2)))
42	41	ex 448	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((#‘𝑉) ∈ ℕ → ((#‘𝐹) = (((#‘𝑉) − 1)C2) → ((#‘𝐸) = (((#‘𝑉) − 1) + (#‘𝐹)) → (#‘𝐸) = ((#‘𝑉)C2))))
43	42	com3r 84	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((#‘𝐸) = (((#‘𝑉) − 1) + (#‘𝐹)) → ((#‘𝑉) ∈ ℕ → ((#‘𝐹) = (((#‘𝑉) − 1)C2) → (#‘𝐸) = ((#‘𝑉)C2))))
44	33, 43	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐺 ∈ ComplUSGraph ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → ((#‘𝑉) ∈ ℕ → ((#‘𝐹) = (((#‘𝑉) − 1)C2) → (#‘𝐸) = ((#‘𝑉)C2))))
45	44	3exp 1255	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐺 ∈ ComplUSGraph → (𝑉 ∈ Fin → (𝑁 ∈ 𝑉 → ((#‘𝑉) ∈ ℕ → ((#‘𝐹) = (((#‘𝑉) − 1)C2) → (#‘𝐸) = ((#‘𝑉)C2))))))
46	45	com14 93	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((#‘𝑉) ∈ ℕ → (𝑉 ∈ Fin → (𝑁 ∈ 𝑉 → (𝐺 ∈ ComplUSGraph → ((#‘𝐹) = (((#‘𝑉) − 1)C2) → (#‘𝐸) = ((#‘𝑉)C2))))))
47	46	adantl 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑉 ∈ V ∧ (#‘𝑉) ∈ ℕ) → (𝑉 ∈ Fin → (𝑁 ∈ 𝑉 → (𝐺 ∈ ComplUSGraph → ((#‘𝐹) = (((#‘𝑉) − 1)C2) → (#‘𝐸) = ((#‘𝑉)C2))))))
48	30, 47	mpd 15	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑉 ∈ V ∧ (#‘𝑉) ∈ ℕ) → (𝑁 ∈ 𝑉 → (𝐺 ∈ ComplUSGraph → ((#‘𝐹) = (((#‘𝑉) − 1)C2) → (#‘𝐸) = ((#‘𝑉)C2)))))
49	48	ex 448	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑉 ∈ V → ((#‘𝑉) ∈ ℕ → (𝑁 ∈ 𝑉 → (𝐺 ∈ ComplUSGraph → ((#‘𝐹) = (((#‘𝑉) − 1)C2) → (#‘𝐸) = ((#‘𝑉)C2))))))
50	49	com23 83	. . . . . . . . . . . . . . . . 17 ⊢ (𝑉 ∈ V → (𝑁 ∈ 𝑉 → ((#‘𝑉) ∈ ℕ → (𝐺 ∈ ComplUSGraph → ((#‘𝐹) = (((#‘𝑉) − 1)C2) → (#‘𝐸) = ((#‘𝑉)C2))))))
51	50	adantr 479	. . . . . . . . . . . . . . . 16 ⊢ ((𝑉 ∈ V ∧ (#‘𝑉) = 𝑌) → (𝑁 ∈ 𝑉 → ((#‘𝑉) ∈ ℕ → (𝐺 ∈ ComplUSGraph → ((#‘𝐹) = (((#‘𝑉) − 1)C2) → (#‘𝐸) = ((#‘𝑉)C2))))))
52	51	imp 443	. . . . . . . . . . . . . . 15 ⊢ (((𝑉 ∈ V ∧ (#‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) → ((#‘𝑉) ∈ ℕ → (𝐺 ∈ ComplUSGraph → ((#‘𝐹) = (((#‘𝑉) − 1)C2) → (#‘𝐸) = ((#‘𝑉)C2)))))
53	26, 52	sylbid 228	. . . . . . . . . . . . . 14 ⊢ (((𝑉 ∈ V ∧ (#‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) → (𝑌 ∈ ℕ → (𝐺 ∈ ComplUSGraph → ((#‘𝐹) = (((#‘𝑉) − 1)C2) → (#‘𝐸) = ((#‘𝑉)C2)))))
54	53	imp 443	. . . . . . . . . . . . 13 ⊢ ((((𝑉 ∈ V ∧ (#‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) ∧ 𝑌 ∈ ℕ) → (𝐺 ∈ ComplUSGraph → ((#‘𝐹) = (((#‘𝑉) − 1)C2) → (#‘𝐸) = ((#‘𝑉)C2))))
55	54	com13 85	. . . . . . . . . . . 12 ⊢ ((#‘𝐹) = (((#‘𝑉) − 1)C2) → (𝐺 ∈ ComplUSGraph → ((((𝑉 ∈ V ∧ (#‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) ∧ 𝑌 ∈ ℕ) → (#‘𝐸) = ((#‘𝑉)C2))))
56	25, 55	syl6bi 241	. . . . . . . . . . 11 ⊢ ((#‘(𝑉 ∖ {𝑁})) = ((#‘𝑉) − 1) → ((#‘𝐹) = ((#‘(𝑉 ∖ {𝑁}))C2) → (𝐺 ∈ ComplUSGraph → ((((𝑉 ∈ V ∧ (#‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) ∧ 𝑌 ∈ ℕ) → (#‘𝐸) = ((#‘𝑉)C2)))))
57	56	com24 92	. . . . . . . . . 10 ⊢ ((#‘(𝑉 ∖ {𝑁})) = ((#‘𝑉) − 1) → ((((𝑉 ∈ V ∧ (#‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) ∧ 𝑌 ∈ ℕ) → (𝐺 ∈ ComplUSGraph → ((#‘𝐹) = ((#‘(𝑉 ∖ {𝑁}))C2) → (#‘𝐸) = ((#‘𝑉)C2)))))
58	23, 57	mpcom 37	. . . . . . . . 9 ⊢ ((((𝑉 ∈ V ∧ (#‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) ∧ 𝑌 ∈ ℕ) → (𝐺 ∈ ComplUSGraph → ((#‘𝐹) = ((#‘(𝑉 ∖ {𝑁}))C2) → (#‘𝐸) = ((#‘𝑉)C2))))
59	58	ex 448	. . . . . . . 8 ⊢ (((𝑉 ∈ V ∧ (#‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) → (𝑌 ∈ ℕ → (𝐺 ∈ ComplUSGraph → ((#‘𝐹) = ((#‘(𝑉 ∖ {𝑁}))C2) → (#‘𝐸) = ((#‘𝑉)C2)))))
60	59	adantllr 750	. . . . . . 7 ⊢ ((((𝑉 ∈ V ∧ 𝑌 ∈ ℕ0) ∧ (#‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) → (𝑌 ∈ ℕ → (𝐺 ∈ ComplUSGraph → ((#‘𝐹) = ((#‘(𝑉 ∖ {𝑁}))C2) → (#‘𝐸) = ((#‘𝑉)C2)))))
61	5, 60	mpd 15	. . . . . 6 ⊢ ((((𝑉 ∈ V ∧ 𝑌 ∈ ℕ0) ∧ (#‘𝑉) = 𝑌) ∧ 𝑁 ∈ 𝑉) → (𝐺 ∈ ComplUSGraph → ((#‘𝐹) = ((#‘(𝑉 ∖ {𝑁}))C2) → (#‘𝐸) = ((#‘𝑉)C2))))
62	61	exp41 635	. . . . 5 ⊢ (𝑉 ∈ V → (𝑌 ∈ ℕ0 → ((#‘𝑉) = 𝑌 → (𝑁 ∈ 𝑉 → (𝐺 ∈ ComplUSGraph → ((#‘𝐹) = ((#‘(𝑉 ∖ {𝑁}))C2) → (#‘𝐸) = ((#‘𝑉)C2)))))))
63	62	com25 96	. . . 4 ⊢ (𝑉 ∈ V → (𝐺 ∈ ComplUSGraph → ((#‘𝑉) = 𝑌 → (𝑁 ∈ 𝑉 → (𝑌 ∈ ℕ0 → ((#‘𝐹) = ((#‘(𝑉 ∖ {𝑁}))C2) → (#‘𝐸) = ((#‘𝑉)C2)))))))
64	3, 63	ax-mp 5	. . 3 ⊢ (𝐺 ∈ ComplUSGraph → ((#‘𝑉) = 𝑌 → (𝑁 ∈ 𝑉 → (𝑌 ∈ ℕ0 → ((#‘𝐹) = ((#‘(𝑉 ∖ {𝑁}))C2) → (#‘𝐸) = ((#‘𝑉)C2))))))
65	64	3imp 1248	. 2 ⊢ ((𝐺 ∈ ComplUSGraph ∧ (#‘𝑉) = 𝑌 ∧ 𝑁 ∈ 𝑉) → (𝑌 ∈ ℕ0 → ((#‘𝐹) = ((#‘(𝑉 ∖ {𝑁}))C2) → (#‘𝐸) = ((#‘𝑉)C2))))
66	65	com12 32	1 ⊢ (𝑌 ∈ ℕ0 → ((𝐺 ∈ ComplUSGraph ∧ (#‘𝑉) = 𝑌 ∧ 𝑁 ∈ 𝑉) → ((#‘𝐹) = ((#‘(𝑉 ∖ {𝑁}))C2) → (#‘𝐸) = ((#‘𝑉)C2))))

Syntax hints:   → wi 4   ↔ wb 194   ∧ wa 382   ∧ w3a 1030   = wceq 1474   ∈ wcel 1976   ∉ wnel 2777  {crab 2896  Vcvv 3169   ∖ cdif 3533  {csn 4121  ‘cfv 5787  (class class class)co 6524  Fincfn 7815  1c1 9790   + caddc 9792   − cmin 10114  ℕcn 10864  2c2 10914  ℕ₀cn0 11136  Ccbc 12903  #chash 12931  Vtxcvtx 40228  Edgcedga 40350  ComplUSGraphccusgr 40552

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-rep 4690  ax-sep 4700  ax-nul 4709  ax-pow 4761  ax-pr 4825  ax-un 6821  ax-cnex 9845  ax-resscn 9846  ax-1cn 9847  ax-icn 9848  ax-addcl 9849  ax-addrcl 9850  ax-mulcl 9851  ax-mulrcl 9852  ax-mulcom 9853  ax-addass 9854  ax-mulass 9855  ax-distr 9856  ax-i2m1 9857  ax-1ne0 9858  ax-1rid 9859  ax-rnegex 9860  ax-rrecex 9861  ax-cnre 9862  ax-pre-lttri 9863  ax-pre-lttrn 9864  ax-pre-ltadd 9865  ax-pre-mulgt0 9866

This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2458  df-mo 2459  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ne 2778  df-nel 2779  df-ral 2897  df-rex 2898  df-reu 2899  df-rmo 2900  df-rab 2901  df-v 3171  df-sbc 3399  df-csb 3496  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-pss 3552  df-nul 3871  df-if 4033  df-pw 4106  df-sn 4122  df-pr 4124  df-tp 4126  df-op 4128  df-uni 4364  df-int 4402  df-iun 4448  df-br 4575  df-opab 4635  df-mpt 4636  df-tr 4672  df-eprel 4936  df-id 4940  df-po 4946  df-so 4947  df-fr 4984  df-we 4986  df-xp 5031  df-rel 5032  df-cnv 5033  df-co 5034  df-dm 5035  df-rn 5036  df-res 5037  df-ima 5038  df-pred 5580  df-ord 5626  df-on 5627  df-lim 5628  df-suc 5629  df-iota 5751  df-fun 5789  df-fn 5790  df-f 5791  df-f1 5792  df-fo 5793  df-f1o 5794  df-fv 5795  df-riota 6486  df-ov 6527  df-oprab 6528  df-mpt2 6529  df-om 6932  df-1st 7033  df-2nd 7034  df-wrecs 7268  df-recs 7329  df-rdg 7367  df-1o 7421  df-2o 7422  df-oadd 7425  df-er 7603  df-en 7816  df-dom 7817  df-sdom 7818  df-fin 7819  df-card 8622  df-cda 8847  df-pnf 9929  df-mnf 9930  df-xr 9931  df-ltxr 9932  df-le 9933  df-sub 10116  df-neg 10117  df-div 10531  df-nn 10865  df-2 10923  df-n0 11137  df-z 11208  df-uz 11517  df-rp 11662  df-fz 12150  df-seq 12616  df-fac 12875  df-bc 12904  df-hash 12932  df-vtx 40230  df-iedg 40231  df-uhgr 40279  df-upgr 40307  df-umgr 40308  df-edga 40351  df-uspgr 40379  df-usgr 40380  df-fusgr 40535  df-nbgr 40553  df-uvtxa 40555  df-cplgr 40556  df-cusgr 40557

This theorem is referenced by:  cusgrsize  40669