vtxdun - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > vtxdun		Structured version Visualization version GIF version

Theorem vtxdun 29462

Description: The degree of a vertex in the union of two graphs on the same vertex set is the sum of the degrees of the vertex in each graph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 21-Dec-2017.) (Revised by AV, 19-Feb-2021.)

**Hypotheses**
Ref	Expression
vtxdun.i	⊢ 𝐼 = (iEdg‘𝐺)
vtxdun.j	⊢ 𝐽 = (iEdg‘𝐻)
vtxdun.vg	⊢ 𝑉 = (Vtx‘𝐺)
vtxdun.vh	⊢ (𝜑 → (Vtx‘𝐻) = 𝑉)
vtxdun.vu	⊢ (𝜑 → (Vtx‘𝑈) = 𝑉)
vtxdun.d	⊢ (𝜑 → (dom 𝐼 ∩ dom 𝐽) = ∅)
vtxdun.fi	⊢ (𝜑 → Fun 𝐼)
vtxdun.fj	⊢ (𝜑 → Fun 𝐽)
vtxdun.n	⊢ (𝜑 → 𝑁 ∈ 𝑉)
vtxdun.u	⊢ (𝜑 → (iEdg‘𝑈) = (𝐼 ∪ 𝐽))

**Assertion**
Ref	Expression
vtxdun	⊢ (𝜑 → ((VtxDeg‘𝑈)‘𝑁) = (((VtxDeg‘𝐺)‘𝑁) +_𝑒 ((VtxDeg‘𝐻)‘𝑁)))

Proof of Theorem vtxdun Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-rab 3397	. . . . . . . 8 ⊢ {𝑥 ∈ dom (iEdg‘𝑈) ∣ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)} = {𝑥 ∣ (𝑥 ∈ dom (iEdg‘𝑈) ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))}
2		vtxdun.u	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (iEdg‘𝑈) = (𝐼 ∪ 𝐽))
3	2	dmeqd 5849	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom (iEdg‘𝑈) = dom (𝐼 ∪ 𝐽))
4		dmun 5854	. . . . . . . . . . . . . 14 ⊢ dom (𝐼 ∪ 𝐽) = (dom 𝐼 ∪ dom 𝐽)
5	3, 4	eqtrdi 2784	. . . . . . . . . . . . 13 ⊢ (𝜑 → dom (iEdg‘𝑈) = (dom 𝐼 ∪ dom 𝐽))
6	5	eleq2d 2819	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑥 ∈ dom (iEdg‘𝑈) ↔ 𝑥 ∈ (dom 𝐼 ∪ dom 𝐽)))
7		elun 4102	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (dom 𝐼 ∪ dom 𝐽) ↔ (𝑥 ∈ dom 𝐼 ∨ 𝑥 ∈ dom 𝐽))
8	6, 7	bitrdi 287	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ dom (iEdg‘𝑈) ↔ (𝑥 ∈ dom 𝐼 ∨ 𝑥 ∈ dom 𝐽)))
9	8	anbi1d 631	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑥 ∈ dom (iEdg‘𝑈) ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)) ↔ ((𝑥 ∈ dom 𝐼 ∨ 𝑥 ∈ dom 𝐽) ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))))
10		andir 1010	. . . . . . . . . 10 ⊢ (((𝑥 ∈ dom 𝐼 ∨ 𝑥 ∈ dom 𝐽) ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)) ↔ ((𝑥 ∈ dom 𝐼 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)) ∨ (𝑥 ∈ dom 𝐽 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))))
11	9, 10	bitrdi 287	. . . . . . . . 9 ⊢ (𝜑 → ((𝑥 ∈ dom (iEdg‘𝑈) ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)) ↔ ((𝑥 ∈ dom 𝐼 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)) ∨ (𝑥 ∈ dom 𝐽 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)))))
12	11	abbidv 2799	. . . . . . . 8 ⊢ (𝜑 → {𝑥 ∣ (𝑥 ∈ dom (iEdg‘𝑈) ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))} = {𝑥 ∣ ((𝑥 ∈ dom 𝐼 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)) ∨ (𝑥 ∈ dom 𝐽 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)))})
13	1, 12	eqtrid 2780	. . . . . . 7 ⊢ (𝜑 → {𝑥 ∈ dom (iEdg‘𝑈) ∣ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)} = {𝑥 ∣ ((𝑥 ∈ dom 𝐼 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)) ∨ (𝑥 ∈ dom 𝐽 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)))})
14		unab 4257	. . . . . . . . 9 ⊢ ({𝑥 ∣ (𝑥 ∈ dom 𝐼 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))} ∪ {𝑥 ∣ (𝑥 ∈ dom 𝐽 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))}) = {𝑥 ∣ ((𝑥 ∈ dom 𝐼 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)) ∨ (𝑥 ∈ dom 𝐽 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)))}
15	14	eqcomi 2742	. . . . . . . 8 ⊢ {𝑥 ∣ ((𝑥 ∈ dom 𝐼 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)) ∨ (𝑥 ∈ dom 𝐽 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)))} = ({𝑥 ∣ (𝑥 ∈ dom 𝐼 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))} ∪ {𝑥 ∣ (𝑥 ∈ dom 𝐽 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))})
16	15	a1i 11	. . . . . . 7 ⊢ (𝜑 → {𝑥 ∣ ((𝑥 ∈ dom 𝐼 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)) ∨ (𝑥 ∈ dom 𝐽 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)))} = ({𝑥 ∣ (𝑥 ∈ dom 𝐼 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))} ∪ {𝑥 ∣ (𝑥 ∈ dom 𝐽 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))}))
17		df-rab 3397	. . . . . . . . 9 ⊢ {𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)} = {𝑥 ∣ (𝑥 ∈ dom 𝐼 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))}
18	2	fveq1d 6830	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((iEdg‘𝑈)‘𝑥) = ((𝐼 ∪ 𝐽)‘𝑥))
19	18	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐼) → ((iEdg‘𝑈)‘𝑥) = ((𝐼 ∪ 𝐽)‘𝑥))
20		vtxdun.fi	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → Fun 𝐼)
21	20	funfnd 6517	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐼 Fn dom 𝐼)
22	21	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐼) → 𝐼 Fn dom 𝐼)
23		vtxdun.fj	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → Fun 𝐽)
24	23	funfnd 6517	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐽 Fn dom 𝐽)
25	24	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐼) → 𝐽 Fn dom 𝐽)
26		vtxdun.d	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (dom 𝐼 ∩ dom 𝐽) = ∅)
27	26	anim1i 615	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐼) → ((dom 𝐼 ∩ dom 𝐽) = ∅ ∧ 𝑥 ∈ dom 𝐼))
28		fvun1 6919	. . . . . . . . . . . . 13 ⊢ ((𝐼 Fn dom 𝐼 ∧ 𝐽 Fn dom 𝐽 ∧ ((dom 𝐼 ∩ dom 𝐽) = ∅ ∧ 𝑥 ∈ dom 𝐼)) → ((𝐼 ∪ 𝐽)‘𝑥) = (𝐼‘𝑥))
29	22, 25, 27, 28	syl3anc 1373	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐼) → ((𝐼 ∪ 𝐽)‘𝑥) = (𝐼‘𝑥))
30	19, 29	eqtrd 2768	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐼) → ((iEdg‘𝑈)‘𝑥) = (𝐼‘𝑥))
31	30	eleq2d 2819	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐼) → (𝑁 ∈ ((iEdg‘𝑈)‘𝑥) ↔ 𝑁 ∈ (𝐼‘𝑥)))
32	31	rabbidva 3402	. . . . . . . . 9 ⊢ (𝜑 → {𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)} = {𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)})
33	17, 32	eqtr3id 2782	. . . . . . . 8 ⊢ (𝜑 → {𝑥 ∣ (𝑥 ∈ dom 𝐼 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))} = {𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)})
34		df-rab 3397	. . . . . . . . 9 ⊢ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)} = {𝑥 ∣ (𝑥 ∈ dom 𝐽 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))}
35	18	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐽) → ((iEdg‘𝑈)‘𝑥) = ((𝐼 ∪ 𝐽)‘𝑥))
36	21	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐽) → 𝐼 Fn dom 𝐼)
37	24	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐽) → 𝐽 Fn dom 𝐽)
38	26	anim1i 615	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐽) → ((dom 𝐼 ∩ dom 𝐽) = ∅ ∧ 𝑥 ∈ dom 𝐽))
39		fvun2 6920	. . . . . . . . . . . . 13 ⊢ ((𝐼 Fn dom 𝐼 ∧ 𝐽 Fn dom 𝐽 ∧ ((dom 𝐼 ∩ dom 𝐽) = ∅ ∧ 𝑥 ∈ dom 𝐽)) → ((𝐼 ∪ 𝐽)‘𝑥) = (𝐽‘𝑥))
40	36, 37, 38, 39	syl3anc 1373	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐽) → ((𝐼 ∪ 𝐽)‘𝑥) = (𝐽‘𝑥))
41	35, 40	eqtrd 2768	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐽) → ((iEdg‘𝑈)‘𝑥) = (𝐽‘𝑥))
42	41	eleq2d 2819	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐽) → (𝑁 ∈ ((iEdg‘𝑈)‘𝑥) ↔ 𝑁 ∈ (𝐽‘𝑥)))
43	42	rabbidva 3402	. . . . . . . . 9 ⊢ (𝜑 → {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)} = {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)})
44	34, 43	eqtr3id 2782	. . . . . . . 8 ⊢ (𝜑 → {𝑥 ∣ (𝑥 ∈ dom 𝐽 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))} = {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)})
45	33, 44	uneq12d 4118	. . . . . . 7 ⊢ (𝜑 → ({𝑥 ∣ (𝑥 ∈ dom 𝐼 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))} ∪ {𝑥 ∣ (𝑥 ∈ dom 𝐽 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))}) = ({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∪ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}))
46	13, 16, 45	3eqtrd 2772	. . . . . 6 ⊢ (𝜑 → {𝑥 ∈ dom (iEdg‘𝑈) ∣ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)} = ({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∪ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}))
47	46	fveq2d 6832	. . . . 5 ⊢ (𝜑 → (♯‘{𝑥 ∈ dom (iEdg‘𝑈) ∣ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)}) = (♯‘({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∪ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)})))
48		vtxdun.i	. . . . . . . . . 10 ⊢ 𝐼 = (iEdg‘𝐺)
49	48	fvexi 6842	. . . . . . . . 9 ⊢ 𝐼 ∈ V
50	49	dmex 7845	. . . . . . . 8 ⊢ dom 𝐼 ∈ V
51	50	rabex 5279	. . . . . . 7 ⊢ {𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∈ V
52	51	a1i 11	. . . . . 6 ⊢ (𝜑 → {𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∈ V)
53		vtxdun.j	. . . . . . . . . 10 ⊢ 𝐽 = (iEdg‘𝐻)
54	53	fvexi 6842	. . . . . . . . 9 ⊢ 𝐽 ∈ V
55	54	dmex 7845	. . . . . . . 8 ⊢ dom 𝐽 ∈ V
56	55	rabex 5279	. . . . . . 7 ⊢ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)} ∈ V
57	56	a1i 11	. . . . . 6 ⊢ (𝜑 → {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)} ∈ V)
58		ssrab2 4029	. . . . . . . . 9 ⊢ {𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ⊆ dom 𝐼
59		ssrab2 4029	. . . . . . . . 9 ⊢ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)} ⊆ dom 𝐽
60		ss2in 4194	. . . . . . . . 9 ⊢ (({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ⊆ dom 𝐼 ∧ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)} ⊆ dom 𝐽) → ({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∩ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) ⊆ (dom 𝐼 ∩ dom 𝐽))
61	58, 59, 60	mp2an 692	. . . . . . . 8 ⊢ ({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∩ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) ⊆ (dom 𝐼 ∩ dom 𝐽)
62	61, 26	sseqtrid 3973	. . . . . . 7 ⊢ (𝜑 → ({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∩ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) ⊆ ∅)
63		ss0 4351	. . . . . . 7 ⊢ (({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∩ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) ⊆ ∅ → ({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∩ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) = ∅)
64	62, 63	syl 17	. . . . . 6 ⊢ (𝜑 → ({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∩ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) = ∅)
65		hashunx 14295	. . . . . 6 ⊢ (({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∈ V ∧ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)} ∈ V ∧ ({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∩ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) = ∅) → (♯‘({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∪ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)})) = ((♯‘{𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) +_𝑒 (♯‘{𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)})))
66	52, 57, 64, 65	syl3anc 1373	. . . . 5 ⊢ (𝜑 → (♯‘({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∪ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)})) = ((♯‘{𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) +_𝑒 (♯‘{𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)})))
67	47, 66	eqtrd 2768	. . . 4 ⊢ (𝜑 → (♯‘{𝑥 ∈ dom (iEdg‘𝑈) ∣ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)}) = ((♯‘{𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) +_𝑒 (♯‘{𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)})))
68		df-rab 3397	. . . . . . . 8 ⊢ {𝑥 ∈ dom (iEdg‘𝑈) ∣ ((iEdg‘𝑈)‘𝑥) = {𝑁}} = {𝑥 ∣ (𝑥 ∈ dom (iEdg‘𝑈) ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})}
69	8	anbi1d 631	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑥 ∈ dom (iEdg‘𝑈) ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}) ↔ ((𝑥 ∈ dom 𝐼 ∨ 𝑥 ∈ dom 𝐽) ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})))
70		andir 1010	. . . . . . . . . 10 ⊢ (((𝑥 ∈ dom 𝐼 ∨ 𝑥 ∈ dom 𝐽) ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}) ↔ ((𝑥 ∈ dom 𝐼 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}) ∨ (𝑥 ∈ dom 𝐽 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})))
71	69, 70	bitrdi 287	. . . . . . . . 9 ⊢ (𝜑 → ((𝑥 ∈ dom (iEdg‘𝑈) ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}) ↔ ((𝑥 ∈ dom 𝐼 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}) ∨ (𝑥 ∈ dom 𝐽 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}))))
72	71	abbidv 2799	. . . . . . . 8 ⊢ (𝜑 → {𝑥 ∣ (𝑥 ∈ dom (iEdg‘𝑈) ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})} = {𝑥 ∣ ((𝑥 ∈ dom 𝐼 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}) ∨ (𝑥 ∈ dom 𝐽 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}))})
73	68, 72	eqtrid 2780	. . . . . . 7 ⊢ (𝜑 → {𝑥 ∈ dom (iEdg‘𝑈) ∣ ((iEdg‘𝑈)‘𝑥) = {𝑁}} = {𝑥 ∣ ((𝑥 ∈ dom 𝐼 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}) ∨ (𝑥 ∈ dom 𝐽 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}))})
74		unab 4257	. . . . . . . . 9 ⊢ ({𝑥 ∣ (𝑥 ∈ dom 𝐼 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})} ∪ {𝑥 ∣ (𝑥 ∈ dom 𝐽 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})}) = {𝑥 ∣ ((𝑥 ∈ dom 𝐼 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}) ∨ (𝑥 ∈ dom 𝐽 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}))}
75	74	eqcomi 2742	. . . . . . . 8 ⊢ {𝑥 ∣ ((𝑥 ∈ dom 𝐼 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}) ∨ (𝑥 ∈ dom 𝐽 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}))} = ({𝑥 ∣ (𝑥 ∈ dom 𝐼 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})} ∪ {𝑥 ∣ (𝑥 ∈ dom 𝐽 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})})
76	75	a1i 11	. . . . . . 7 ⊢ (𝜑 → {𝑥 ∣ ((𝑥 ∈ dom 𝐼 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}) ∨ (𝑥 ∈ dom 𝐽 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}))} = ({𝑥 ∣ (𝑥 ∈ dom 𝐼 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})} ∪ {𝑥 ∣ (𝑥 ∈ dom 𝐽 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})}))
77		df-rab 3397	. . . . . . . . 9 ⊢ {𝑥 ∈ dom 𝐼 ∣ ((iEdg‘𝑈)‘𝑥) = {𝑁}} = {𝑥 ∣ (𝑥 ∈ dom 𝐼 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})}
78	30	eqeq1d 2735	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐼) → (((iEdg‘𝑈)‘𝑥) = {𝑁} ↔ (𝐼‘𝑥) = {𝑁}))
79	78	rabbidva 3402	. . . . . . . . 9 ⊢ (𝜑 → {𝑥 ∈ dom 𝐼 ∣ ((iEdg‘𝑈)‘𝑥) = {𝑁}} = {𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}})
80	77, 79	eqtr3id 2782	. . . . . . . 8 ⊢ (𝜑 → {𝑥 ∣ (𝑥 ∈ dom 𝐼 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})} = {𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}})
81		df-rab 3397	. . . . . . . . 9 ⊢ {𝑥 ∈ dom 𝐽 ∣ ((iEdg‘𝑈)‘𝑥) = {𝑁}} = {𝑥 ∣ (𝑥 ∈ dom 𝐽 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})}
82	41	eqeq1d 2735	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐽) → (((iEdg‘𝑈)‘𝑥) = {𝑁} ↔ (𝐽‘𝑥) = {𝑁}))
83	82	rabbidva 3402	. . . . . . . . 9 ⊢ (𝜑 → {𝑥 ∈ dom 𝐽 ∣ ((iEdg‘𝑈)‘𝑥) = {𝑁}} = {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}})
84	81, 83	eqtr3id 2782	. . . . . . . 8 ⊢ (𝜑 → {𝑥 ∣ (𝑥 ∈ dom 𝐽 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})} = {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}})
85	80, 84	uneq12d 4118	. . . . . . 7 ⊢ (𝜑 → ({𝑥 ∣ (𝑥 ∈ dom 𝐼 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})} ∪ {𝑥 ∣ (𝑥 ∈ dom 𝐽 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})}) = ({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∪ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}))
86	73, 76, 85	3eqtrd 2772	. . . . . 6 ⊢ (𝜑 → {𝑥 ∈ dom (iEdg‘𝑈) ∣ ((iEdg‘𝑈)‘𝑥) = {𝑁}} = ({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∪ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}))
87	86	fveq2d 6832	. . . . 5 ⊢ (𝜑 → (♯‘{𝑥 ∈ dom (iEdg‘𝑈) ∣ ((iEdg‘𝑈)‘𝑥) = {𝑁}}) = (♯‘({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∪ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}})))
88	50	rabex 5279	. . . . . . 7 ⊢ {𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∈ V
89	88	a1i 11	. . . . . 6 ⊢ (𝜑 → {𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∈ V)
90	55	rabex 5279	. . . . . . 7 ⊢ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}} ∈ V
91	90	a1i 11	. . . . . 6 ⊢ (𝜑 → {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}} ∈ V)
92		ssrab2 4029	. . . . . . . . 9 ⊢ {𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ⊆ dom 𝐼
93		ssrab2 4029	. . . . . . . . 9 ⊢ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}} ⊆ dom 𝐽
94		ss2in 4194	. . . . . . . . 9 ⊢ (({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ⊆ dom 𝐼 ∧ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}} ⊆ dom 𝐽) → ({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∩ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}) ⊆ (dom 𝐼 ∩ dom 𝐽))
95	92, 93, 94	mp2an 692	. . . . . . . 8 ⊢ ({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∩ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}) ⊆ (dom 𝐼 ∩ dom 𝐽)
96	95, 26	sseqtrid 3973	. . . . . . 7 ⊢ (𝜑 → ({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∩ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}) ⊆ ∅)
97		ss0 4351	. . . . . . 7 ⊢ (({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∩ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}) ⊆ ∅ → ({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∩ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}) = ∅)
98	96, 97	syl 17	. . . . . 6 ⊢ (𝜑 → ({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∩ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}) = ∅)
99		hashunx 14295	. . . . . 6 ⊢ (({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∈ V ∧ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}} ∈ V ∧ ({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∩ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}) = ∅) → (♯‘({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∪ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}})) = ((♯‘{𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}}) +_𝑒 (♯‘{𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}})))
100	89, 91, 98, 99	syl3anc 1373	. . . . 5 ⊢ (𝜑 → (♯‘({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∪ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}})) = ((♯‘{𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}}) +_𝑒 (♯‘{𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}})))
101	87, 100	eqtrd 2768	. . . 4 ⊢ (𝜑 → (♯‘{𝑥 ∈ dom (iEdg‘𝑈) ∣ ((iEdg‘𝑈)‘𝑥) = {𝑁}}) = ((♯‘{𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}}) +_𝑒 (♯‘{𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}})))
102	67, 101	oveq12d 7370	. . 3 ⊢ (𝜑 → ((♯‘{𝑥 ∈ dom (iEdg‘𝑈) ∣ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)}) +_𝑒 (♯‘{𝑥 ∈ dom (iEdg‘𝑈) ∣ ((iEdg‘𝑈)‘𝑥) = {𝑁}})) = (((♯‘{𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) +_𝑒 (♯‘{𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)})) +_𝑒 ((♯‘{𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}}) +_𝑒 (♯‘{𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}))))
103		hashxnn0 14248	. . . . 5 ⊢ ({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∈ V → (♯‘{𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) ∈ ℕ₀^*)
104	52, 103	syl 17	. . . 4 ⊢ (𝜑 → (♯‘{𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) ∈ ℕ₀^*)
105		hashxnn0 14248	. . . . 5 ⊢ ({𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)} ∈ V → (♯‘{𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) ∈ ℕ₀^*)
106	57, 105	syl 17	. . . 4 ⊢ (𝜑 → (♯‘{𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) ∈ ℕ₀^*)
107		hashxnn0 14248	. . . . 5 ⊢ ({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∈ V → (♯‘{𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}}) ∈ ℕ₀^*)
108	89, 107	syl 17	. . . 4 ⊢ (𝜑 → (♯‘{𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}}) ∈ ℕ₀^*)
109		hashxnn0 14248	. . . . 5 ⊢ ({𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}} ∈ V → (♯‘{𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}) ∈ ℕ₀^*)
110	91, 109	syl 17	. . . 4 ⊢ (𝜑 → (♯‘{𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}) ∈ ℕ₀^*)
111	104, 106, 108, 110	xnn0add4d 13205	. . 3 ⊢ (𝜑 → (((♯‘{𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) +_𝑒 (♯‘{𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)})) +_𝑒 ((♯‘{𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}}) +_𝑒 (♯‘{𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}))) = (((♯‘{𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) +_𝑒 (♯‘{𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}})) +_𝑒 ((♯‘{𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) +_𝑒 (♯‘{𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}))))
112	102, 111	eqtrd 2768	. 2 ⊢ (𝜑 → ((♯‘{𝑥 ∈ dom (iEdg‘𝑈) ∣ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)}) +_𝑒 (♯‘{𝑥 ∈ dom (iEdg‘𝑈) ∣ ((iEdg‘𝑈)‘𝑥) = {𝑁}})) = (((♯‘{𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) +_𝑒 (♯‘{𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}})) +_𝑒 ((♯‘{𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) +_𝑒 (♯‘{𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}))))
113		vtxdun.n	. . . 4 ⊢ (𝜑 → 𝑁 ∈ 𝑉)
114		vtxdun.vu	. . . 4 ⊢ (𝜑 → (Vtx‘𝑈) = 𝑉)
115	113, 114	eleqtrrd 2836	. . 3 ⊢ (𝜑 → 𝑁 ∈ (Vtx‘𝑈))
116		eqid 2733	. . . 4 ⊢ (Vtx‘𝑈) = (Vtx‘𝑈)
117		eqid 2733	. . . 4 ⊢ (iEdg‘𝑈) = (iEdg‘𝑈)
118		eqid 2733	. . . 4 ⊢ dom (iEdg‘𝑈) = dom (iEdg‘𝑈)
119	116, 117, 118	vtxdgval 29449	. . 3 ⊢ (𝑁 ∈ (Vtx‘𝑈) → ((VtxDeg‘𝑈)‘𝑁) = ((♯‘{𝑥 ∈ dom (iEdg‘𝑈) ∣ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)}) +_𝑒 (♯‘{𝑥 ∈ dom (iEdg‘𝑈) ∣ ((iEdg‘𝑈)‘𝑥) = {𝑁}})))
120	115, 119	syl 17	. 2 ⊢ (𝜑 → ((VtxDeg‘𝑈)‘𝑁) = ((♯‘{𝑥 ∈ dom (iEdg‘𝑈) ∣ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)}) +_𝑒 (♯‘{𝑥 ∈ dom (iEdg‘𝑈) ∣ ((iEdg‘𝑈)‘𝑥) = {𝑁}})))
121		vtxdun.vg	. . . . 5 ⊢ 𝑉 = (Vtx‘𝐺)
122		eqid 2733	. . . . 5 ⊢ dom 𝐼 = dom 𝐼
123	121, 48, 122	vtxdgval 29449	. . . 4 ⊢ (𝑁 ∈ 𝑉 → ((VtxDeg‘𝐺)‘𝑁) = ((♯‘{𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) +_𝑒 (♯‘{𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}})))
124	113, 123	syl 17	. . 3 ⊢ (𝜑 → ((VtxDeg‘𝐺)‘𝑁) = ((♯‘{𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) +_𝑒 (♯‘{𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}})))
125		vtxdun.vh	. . . . 5 ⊢ (𝜑 → (Vtx‘𝐻) = 𝑉)
126	113, 125	eleqtrrd 2836	. . . 4 ⊢ (𝜑 → 𝑁 ∈ (Vtx‘𝐻))
127		eqid 2733	. . . . 5 ⊢ (Vtx‘𝐻) = (Vtx‘𝐻)
128		eqid 2733	. . . . 5 ⊢ dom 𝐽 = dom 𝐽
129	127, 53, 128	vtxdgval 29449	. . . 4 ⊢ (𝑁 ∈ (Vtx‘𝐻) → ((VtxDeg‘𝐻)‘𝑁) = ((♯‘{𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) +_𝑒 (♯‘{𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}})))
130	126, 129	syl 17	. . 3 ⊢ (𝜑 → ((VtxDeg‘𝐻)‘𝑁) = ((♯‘{𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) +_𝑒 (♯‘{𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}})))
131	124, 130	oveq12d 7370	. 2 ⊢ (𝜑 → (((VtxDeg‘𝐺)‘𝑁) +_𝑒 ((VtxDeg‘𝐻)‘𝑁)) = (((♯‘{𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) +_𝑒 (♯‘{𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}})) +_𝑒 ((♯‘{𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) +_𝑒 (♯‘{𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}))))
132	112, 120, 131	3eqtr4d 2778	1 ⊢ (𝜑 → ((VtxDeg‘𝑈)‘𝑁) = (((VtxDeg‘𝐺)‘𝑁) +_𝑒 ((VtxDeg‘𝐻)‘𝑁)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∨ wo 847 = wceq 1541 ∈ wcel 2113 {cab 2711 {crab 3396 Vcvv 3437 ∪ cun 3896 ∩ cin 3897 ⊆ wss 3898 ∅c0 4282 {csn 4575 dom cdm 5619 Fun wfun 6480 Fn wfn 6481 ‘cfv 6486 (class class class)co 7352 ℕ₀^*cxnn0 12461 +_𝑒 cxad 13011 ♯chash 14239 Vtxcvtx 28976 iEdgciedg 28977 VtxDegcvtxdg 29446

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2182 ax-ext 2705 ax-rep 5219 ax-sep 5236 ax-nul 5246 ax-pow 5305 ax-pr 5372 ax-un 7674 ax-cnex 11069 ax-resscn 11070 ax-1cn 11071 ax-icn 11072 ax-addcl 11073 ax-addrcl 11074 ax-mulcl 11075 ax-mulrcl 11076 ax-mulcom 11077 ax-addass 11078 ax-mulass 11079 ax-distr 11080 ax-i2m1 11081 ax-1ne0 11082 ax-1rid 11083 ax-rnegex 11084 ax-rrecex 11085 ax-cnre 11086 ax-pre-lttri 11087 ax-pre-lttrn 11088 ax-pre-ltadd 11089 ax-pre-mulgt0 11090

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2725 df-clel 2808 df-nfc 2882 df-ne 2930 df-nel 3034 df-ral 3049 df-rex 3058 df-reu 3348 df-rab 3397 df-v 3439 df-sbc 3738 df-csb 3847 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-pss 3918 df-nul 4283 df-if 4475 df-pw 4551 df-sn 4576 df-pr 4578 df-op 4582 df-uni 4859 df-int 4898 df-iun 4943 df-br 5094 df-opab 5156 df-mpt 5175 df-tr 5201 df-id 5514 df-eprel 5519 df-po 5527 df-so 5528 df-fr 5572 df-we 5574 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-pred 6253 df-ord 6314 df-on 6315 df-lim 6316 df-suc 6317 df-iota 6442 df-fun 6488 df-fn 6489 df-f 6490 df-f1 6491 df-fo 6492 df-f1o 6493 df-fv 6494 df-riota 7309 df-ov 7355 df-oprab 7356 df-mpo 7357 df-om 7803 df-1st 7927 df-2nd 7928 df-frecs 8217 df-wrecs 8248 df-recs 8297 df-rdg 8335 df-1o 8391 df-oadd 8395 df-er 8628 df-en 8876 df-dom 8877 df-sdom 8878 df-fin 8879 df-dju 9801 df-card 9839 df-pnf 11155 df-mnf 11156 df-xr 11157 df-ltxr 11158 df-le 11159 df-sub 11353 df-neg 11354 df-nn 12133 df-n0 12389 df-xnn0 12462 df-z 12476 df-uz 12739 df-xadd 13014 df-hash 14240 df-vtxdg 29447

This theorem is referenced by: vtxdfiun 29463 vtxduhgrun 29464 p1evtxdeqlem 29493

W3C validator