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 29005

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 3431	. . . . . . . 8 ⊢ {𝑥 ∈ dom (iEdg‘𝑈) ∣ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)} = {𝑥 ∣ (𝑥 ∈ dom (iEdg‘𝑈) ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))}
2		vtxdun.u	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (iEdg‘𝑈) = (𝐼 ∪ 𝐽))
3	2	dmeqd 5904	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom (iEdg‘𝑈) = dom (𝐼 ∪ 𝐽))
4		dmun 5909	. . . . . . . . . . . . . 14 ⊢ dom (𝐼 ∪ 𝐽) = (dom 𝐼 ∪ dom 𝐽)
5	3, 4	eqtrdi 2786	. . . . . . . . . . . . 13 ⊢ (𝜑 → dom (iEdg‘𝑈) = (dom 𝐼 ∪ dom 𝐽))
6	5	eleq2d 2817	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑥 ∈ dom (iEdg‘𝑈) ↔ 𝑥 ∈ (dom 𝐼 ∪ dom 𝐽)))
7		elun 4147	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (dom 𝐼 ∪ dom 𝐽) ↔ (𝑥 ∈ dom 𝐼 ∨ 𝑥 ∈ dom 𝐽))
8	6, 7	bitrdi 286	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ dom (iEdg‘𝑈) ↔ (𝑥 ∈ dom 𝐼 ∨ 𝑥 ∈ dom 𝐽)))
9	8	anbi1d 628	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑥 ∈ dom (iEdg‘𝑈) ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)) ↔ ((𝑥 ∈ dom 𝐼 ∨ 𝑥 ∈ dom 𝐽) ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))))
10		andir 1005	. . . . . . . . . 10 ⊢ (((𝑥 ∈ dom 𝐼 ∨ 𝑥 ∈ dom 𝐽) ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)) ↔ ((𝑥 ∈ dom 𝐼 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)) ∨ (𝑥 ∈ dom 𝐽 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))))
11	9, 10	bitrdi 286	. . . . . . . . 9 ⊢ (𝜑 → ((𝑥 ∈ dom (iEdg‘𝑈) ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)) ↔ ((𝑥 ∈ dom 𝐼 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)) ∨ (𝑥 ∈ dom 𝐽 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)))))
12	11	abbidv 2799	. . . . . . . 8 ⊢ (𝜑 → {𝑥 ∣ (𝑥 ∈ dom (iEdg‘𝑈) ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))} = {𝑥 ∣ ((𝑥 ∈ dom 𝐼 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)) ∨ (𝑥 ∈ dom 𝐽 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)))})
13	1, 12	eqtrid 2782	. . . . . . 7 ⊢ (𝜑 → {𝑥 ∈ dom (iEdg‘𝑈) ∣ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)} = {𝑥 ∣ ((𝑥 ∈ dom 𝐼 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)) ∨ (𝑥 ∈ dom 𝐽 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)))})
14		unab 4297	. . . . . . . . 9 ⊢ ({𝑥 ∣ (𝑥 ∈ dom 𝐼 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))} ∪ {𝑥 ∣ (𝑥 ∈ dom 𝐽 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))}) = {𝑥 ∣ ((𝑥 ∈ dom 𝐼 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)) ∨ (𝑥 ∈ dom 𝐽 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)))}
15	14	eqcomi 2739	. . . . . . . 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 3431	. . . . . . . . 9 ⊢ {𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)} = {𝑥 ∣ (𝑥 ∈ dom 𝐼 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))}
18	2	fveq1d 6892	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((iEdg‘𝑈)‘𝑥) = ((𝐼 ∪ 𝐽)‘𝑥))
19	18	adantr 479	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐼) → ((iEdg‘𝑈)‘𝑥) = ((𝐼 ∪ 𝐽)‘𝑥))
20		vtxdun.fi	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → Fun 𝐼)
21	20	funfnd 6578	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐼 Fn dom 𝐼)
22	21	adantr 479	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐼) → 𝐼 Fn dom 𝐼)
23		vtxdun.fj	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → Fun 𝐽)
24	23	funfnd 6578	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐽 Fn dom 𝐽)
25	24	adantr 479	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐼) → 𝐽 Fn dom 𝐽)
26		vtxdun.d	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (dom 𝐼 ∩ dom 𝐽) = ∅)
27	26	anim1i 613	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐼) → ((dom 𝐼 ∩ dom 𝐽) = ∅ ∧ 𝑥 ∈ dom 𝐼))
28		fvun1 6981	. . . . . . . . . . . . 13 ⊢ ((𝐼 Fn dom 𝐼 ∧ 𝐽 Fn dom 𝐽 ∧ ((dom 𝐼 ∩ dom 𝐽) = ∅ ∧ 𝑥 ∈ dom 𝐼)) → ((𝐼 ∪ 𝐽)‘𝑥) = (𝐼‘𝑥))
29	22, 25, 27, 28	syl3anc 1369	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐼) → ((𝐼 ∪ 𝐽)‘𝑥) = (𝐼‘𝑥))
30	19, 29	eqtrd 2770	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐼) → ((iEdg‘𝑈)‘𝑥) = (𝐼‘𝑥))
31	30	eleq2d 2817	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐼) → (𝑁 ∈ ((iEdg‘𝑈)‘𝑥) ↔ 𝑁 ∈ (𝐼‘𝑥)))
32	31	rabbidva 3437	. . . . . . . . 9 ⊢ (𝜑 → {𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)} = {𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)})
33	17, 32	eqtr3id 2784	. . . . . . . 8 ⊢ (𝜑 → {𝑥 ∣ (𝑥 ∈ dom 𝐼 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))} = {𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)})
34		df-rab 3431	. . . . . . . . 9 ⊢ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)} = {𝑥 ∣ (𝑥 ∈ dom 𝐽 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))}
35	18	adantr 479	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐽) → ((iEdg‘𝑈)‘𝑥) = ((𝐼 ∪ 𝐽)‘𝑥))
36	21	adantr 479	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐽) → 𝐼 Fn dom 𝐼)
37	24	adantr 479	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐽) → 𝐽 Fn dom 𝐽)
38	26	anim1i 613	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐽) → ((dom 𝐼 ∩ dom 𝐽) = ∅ ∧ 𝑥 ∈ dom 𝐽))
39		fvun2 6982	. . . . . . . . . . . . 13 ⊢ ((𝐼 Fn dom 𝐼 ∧ 𝐽 Fn dom 𝐽 ∧ ((dom 𝐼 ∩ dom 𝐽) = ∅ ∧ 𝑥 ∈ dom 𝐽)) → ((𝐼 ∪ 𝐽)‘𝑥) = (𝐽‘𝑥))
40	36, 37, 38, 39	syl3anc 1369	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐽) → ((𝐼 ∪ 𝐽)‘𝑥) = (𝐽‘𝑥))
41	35, 40	eqtrd 2770	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐽) → ((iEdg‘𝑈)‘𝑥) = (𝐽‘𝑥))
42	41	eleq2d 2817	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐽) → (𝑁 ∈ ((iEdg‘𝑈)‘𝑥) ↔ 𝑁 ∈ (𝐽‘𝑥)))
43	42	rabbidva 3437	. . . . . . . . 9 ⊢ (𝜑 → {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)} = {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)})
44	34, 43	eqtr3id 2784	. . . . . . . 8 ⊢ (𝜑 → {𝑥 ∣ (𝑥 ∈ dom 𝐽 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))} = {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)})
45	33, 44	uneq12d 4163	. . . . . . 7 ⊢ (𝜑 → ({𝑥 ∣ (𝑥 ∈ dom 𝐼 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))} ∪ {𝑥 ∣ (𝑥 ∈ dom 𝐽 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))}) = ({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∪ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}))
46	13, 16, 45	3eqtrd 2774	. . . . . 6 ⊢ (𝜑 → {𝑥 ∈ dom (iEdg‘𝑈) ∣ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)} = ({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∪ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}))
47	46	fveq2d 6894	. . . . 5 ⊢ (𝜑 → (♯‘{𝑥 ∈ dom (iEdg‘𝑈) ∣ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)}) = (♯‘({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∪ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)})))
48		vtxdun.i	. . . . . . . . . 10 ⊢ 𝐼 = (iEdg‘𝐺)
49	48	fvexi 6904	. . . . . . . . 9 ⊢ 𝐼 ∈ V
50	49	dmex 7904	. . . . . . . 8 ⊢ dom 𝐼 ∈ V
51	50	rabex 5331	. . . . . . 7 ⊢ {𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∈ V
52	51	a1i 11	. . . . . 6 ⊢ (𝜑 → {𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∈ V)
53		vtxdun.j	. . . . . . . . . 10 ⊢ 𝐽 = (iEdg‘𝐻)
54	53	fvexi 6904	. . . . . . . . 9 ⊢ 𝐽 ∈ V
55	54	dmex 7904	. . . . . . . 8 ⊢ dom 𝐽 ∈ V
56	55	rabex 5331	. . . . . . 7 ⊢ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)} ∈ V
57	56	a1i 11	. . . . . 6 ⊢ (𝜑 → {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)} ∈ V)
58		ssrab2 4076	. . . . . . . . 9 ⊢ {𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ⊆ dom 𝐼
59		ssrab2 4076	. . . . . . . . 9 ⊢ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)} ⊆ dom 𝐽
60		ss2in 4235	. . . . . . . . 9 ⊢ (({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ⊆ dom 𝐼 ∧ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)} ⊆ dom 𝐽) → ({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∩ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) ⊆ (dom 𝐼 ∩ dom 𝐽))
61	58, 59, 60	mp2an 688	. . . . . . . 8 ⊢ ({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∩ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) ⊆ (dom 𝐼 ∩ dom 𝐽)
62	61, 26	sseqtrid 4033	. . . . . . 7 ⊢ (𝜑 → ({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∩ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) ⊆ ∅)
63		ss0 4397	. . . . . . 7 ⊢ (({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∩ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) ⊆ ∅ → ({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∩ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) = ∅)
64	62, 63	syl 17	. . . . . 6 ⊢ (𝜑 → ({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∩ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) = ∅)
65		hashunx 14350	. . . . . 6 ⊢ (({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∈ V ∧ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)} ∈ V ∧ ({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∩ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) = ∅) → (♯‘({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∪ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)})) = ((♯‘{𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) +_𝑒 (♯‘{𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)})))
66	52, 57, 64, 65	syl3anc 1369	. . . . 5 ⊢ (𝜑 → (♯‘({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∪ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)})) = ((♯‘{𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) +_𝑒 (♯‘{𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)})))
67	47, 66	eqtrd 2770	. . . 4 ⊢ (𝜑 → (♯‘{𝑥 ∈ dom (iEdg‘𝑈) ∣ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)}) = ((♯‘{𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) +_𝑒 (♯‘{𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)})))
68		df-rab 3431	. . . . . . . 8 ⊢ {𝑥 ∈ dom (iEdg‘𝑈) ∣ ((iEdg‘𝑈)‘𝑥) = {𝑁}} = {𝑥 ∣ (𝑥 ∈ dom (iEdg‘𝑈) ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})}
69	8	anbi1d 628	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑥 ∈ dom (iEdg‘𝑈) ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}) ↔ ((𝑥 ∈ dom 𝐼 ∨ 𝑥 ∈ dom 𝐽) ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})))
70		andir 1005	. . . . . . . . . 10 ⊢ (((𝑥 ∈ dom 𝐼 ∨ 𝑥 ∈ dom 𝐽) ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}) ↔ ((𝑥 ∈ dom 𝐼 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}) ∨ (𝑥 ∈ dom 𝐽 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})))
71	69, 70	bitrdi 286	. . . . . . . . 9 ⊢ (𝜑 → ((𝑥 ∈ dom (iEdg‘𝑈) ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}) ↔ ((𝑥 ∈ dom 𝐼 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}) ∨ (𝑥 ∈ dom 𝐽 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}))))
72	71	abbidv 2799	. . . . . . . 8 ⊢ (𝜑 → {𝑥 ∣ (𝑥 ∈ dom (iEdg‘𝑈) ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})} = {𝑥 ∣ ((𝑥 ∈ dom 𝐼 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}) ∨ (𝑥 ∈ dom 𝐽 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}))})
73	68, 72	eqtrid 2782	. . . . . . 7 ⊢ (𝜑 → {𝑥 ∈ dom (iEdg‘𝑈) ∣ ((iEdg‘𝑈)‘𝑥) = {𝑁}} = {𝑥 ∣ ((𝑥 ∈ dom 𝐼 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}) ∨ (𝑥 ∈ dom 𝐽 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}))})
74		unab 4297	. . . . . . . . 9 ⊢ ({𝑥 ∣ (𝑥 ∈ dom 𝐼 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})} ∪ {𝑥 ∣ (𝑥 ∈ dom 𝐽 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})}) = {𝑥 ∣ ((𝑥 ∈ dom 𝐼 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}) ∨ (𝑥 ∈ dom 𝐽 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}))}
75	74	eqcomi 2739	. . . . . . . 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 3431	. . . . . . . . 9 ⊢ {𝑥 ∈ dom 𝐼 ∣ ((iEdg‘𝑈)‘𝑥) = {𝑁}} = {𝑥 ∣ (𝑥 ∈ dom 𝐼 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})}
78	30	eqeq1d 2732	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐼) → (((iEdg‘𝑈)‘𝑥) = {𝑁} ↔ (𝐼‘𝑥) = {𝑁}))
79	78	rabbidva 3437	. . . . . . . . 9 ⊢ (𝜑 → {𝑥 ∈ dom 𝐼 ∣ ((iEdg‘𝑈)‘𝑥) = {𝑁}} = {𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}})
80	77, 79	eqtr3id 2784	. . . . . . . 8 ⊢ (𝜑 → {𝑥 ∣ (𝑥 ∈ dom 𝐼 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})} = {𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}})
81		df-rab 3431	. . . . . . . . 9 ⊢ {𝑥 ∈ dom 𝐽 ∣ ((iEdg‘𝑈)‘𝑥) = {𝑁}} = {𝑥 ∣ (𝑥 ∈ dom 𝐽 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})}
82	41	eqeq1d 2732	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐽) → (((iEdg‘𝑈)‘𝑥) = {𝑁} ↔ (𝐽‘𝑥) = {𝑁}))
83	82	rabbidva 3437	. . . . . . . . 9 ⊢ (𝜑 → {𝑥 ∈ dom 𝐽 ∣ ((iEdg‘𝑈)‘𝑥) = {𝑁}} = {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}})
84	81, 83	eqtr3id 2784	. . . . . . . 8 ⊢ (𝜑 → {𝑥 ∣ (𝑥 ∈ dom 𝐽 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})} = {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}})
85	80, 84	uneq12d 4163	. . . . . . 7 ⊢ (𝜑 → ({𝑥 ∣ (𝑥 ∈ dom 𝐼 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})} ∪ {𝑥 ∣ (𝑥 ∈ dom 𝐽 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})}) = ({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∪ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}))
86	73, 76, 85	3eqtrd 2774	. . . . . 6 ⊢ (𝜑 → {𝑥 ∈ dom (iEdg‘𝑈) ∣ ((iEdg‘𝑈)‘𝑥) = {𝑁}} = ({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∪ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}))
87	86	fveq2d 6894	. . . . 5 ⊢ (𝜑 → (♯‘{𝑥 ∈ dom (iEdg‘𝑈) ∣ ((iEdg‘𝑈)‘𝑥) = {𝑁}}) = (♯‘({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∪ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}})))
88	50	rabex 5331	. . . . . . 7 ⊢ {𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∈ V
89	88	a1i 11	. . . . . 6 ⊢ (𝜑 → {𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∈ V)
90	55	rabex 5331	. . . . . . 7 ⊢ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}} ∈ V
91	90	a1i 11	. . . . . 6 ⊢ (𝜑 → {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}} ∈ V)
92		ssrab2 4076	. . . . . . . . 9 ⊢ {𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ⊆ dom 𝐼
93		ssrab2 4076	. . . . . . . . 9 ⊢ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}} ⊆ dom 𝐽
94		ss2in 4235	. . . . . . . . 9 ⊢ (({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ⊆ dom 𝐼 ∧ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}} ⊆ dom 𝐽) → ({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∩ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}) ⊆ (dom 𝐼 ∩ dom 𝐽))
95	92, 93, 94	mp2an 688	. . . . . . . 8 ⊢ ({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∩ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}) ⊆ (dom 𝐼 ∩ dom 𝐽)
96	95, 26	sseqtrid 4033	. . . . . . 7 ⊢ (𝜑 → ({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∩ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}) ⊆ ∅)
97		ss0 4397	. . . . . . 7 ⊢ (({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∩ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}) ⊆ ∅ → ({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∩ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}) = ∅)
98	96, 97	syl 17	. . . . . 6 ⊢ (𝜑 → ({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∩ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}) = ∅)
99		hashunx 14350	. . . . . 6 ⊢ (({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∈ V ∧ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}} ∈ V ∧ ({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∩ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}) = ∅) → (♯‘({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∪ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}})) = ((♯‘{𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}}) +_𝑒 (♯‘{𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}})))
100	89, 91, 98, 99	syl3anc 1369	. . . . 5 ⊢ (𝜑 → (♯‘({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∪ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}})) = ((♯‘{𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}}) +_𝑒 (♯‘{𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}})))
101	87, 100	eqtrd 2770	. . . 4 ⊢ (𝜑 → (♯‘{𝑥 ∈ dom (iEdg‘𝑈) ∣ ((iEdg‘𝑈)‘𝑥) = {𝑁}}) = ((♯‘{𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}}) +_𝑒 (♯‘{𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}})))
102	67, 101	oveq12d 7429	. . 3 ⊢ (𝜑 → ((♯‘{𝑥 ∈ dom (iEdg‘𝑈) ∣ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)}) +_𝑒 (♯‘{𝑥 ∈ dom (iEdg‘𝑈) ∣ ((iEdg‘𝑈)‘𝑥) = {𝑁}})) = (((♯‘{𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) +_𝑒 (♯‘{𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)})) +_𝑒 ((♯‘{𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}}) +_𝑒 (♯‘{𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}))))
103		hashxnn0 14303	. . . . 5 ⊢ ({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∈ V → (♯‘{𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) ∈ ℕ₀^*)
104	52, 103	syl 17	. . . 4 ⊢ (𝜑 → (♯‘{𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) ∈ ℕ₀^*)
105		hashxnn0 14303	. . . . 5 ⊢ ({𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)} ∈ V → (♯‘{𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) ∈ ℕ₀^*)
106	57, 105	syl 17	. . . 4 ⊢ (𝜑 → (♯‘{𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) ∈ ℕ₀^*)
107		hashxnn0 14303	. . . . 5 ⊢ ({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∈ V → (♯‘{𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}}) ∈ ℕ₀^*)
108	89, 107	syl 17	. . . 4 ⊢ (𝜑 → (♯‘{𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}}) ∈ ℕ₀^*)
109		hashxnn0 14303	. . . . 5 ⊢ ({𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}} ∈ V → (♯‘{𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}) ∈ ℕ₀^*)
110	91, 109	syl 17	. . . 4 ⊢ (𝜑 → (♯‘{𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}) ∈ ℕ₀^*)
111	104, 106, 108, 110	xnn0add4d 13287	. . 3 ⊢ (𝜑 → (((♯‘{𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) +_𝑒 (♯‘{𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)})) +_𝑒 ((♯‘{𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}}) +_𝑒 (♯‘{𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}))) = (((♯‘{𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) +_𝑒 (♯‘{𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}})) +_𝑒 ((♯‘{𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) +_𝑒 (♯‘{𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}))))
112	102, 111	eqtrd 2770	. 2 ⊢ (𝜑 → ((♯‘{𝑥 ∈ dom (iEdg‘𝑈) ∣ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)}) +_𝑒 (♯‘{𝑥 ∈ dom (iEdg‘𝑈) ∣ ((iEdg‘𝑈)‘𝑥) = {𝑁}})) = (((♯‘{𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) +_𝑒 (♯‘{𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}})) +_𝑒 ((♯‘{𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) +_𝑒 (♯‘{𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}))))
113		vtxdun.n	. . . 4 ⊢ (𝜑 → 𝑁 ∈ 𝑉)
114		vtxdun.vu	. . . 4 ⊢ (𝜑 → (Vtx‘𝑈) = 𝑉)
115	113, 114	eleqtrrd 2834	. . 3 ⊢ (𝜑 → 𝑁 ∈ (Vtx‘𝑈))
116		eqid 2730	. . . 4 ⊢ (Vtx‘𝑈) = (Vtx‘𝑈)
117		eqid 2730	. . . 4 ⊢ (iEdg‘𝑈) = (iEdg‘𝑈)
118		eqid 2730	. . . 4 ⊢ dom (iEdg‘𝑈) = dom (iEdg‘𝑈)
119	116, 117, 118	vtxdgval 28992	. . 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 2730	. . . . 5 ⊢ dom 𝐼 = dom 𝐼
123	121, 48, 122	vtxdgval 28992	. . . 4 ⊢ (𝑁 ∈ 𝑉 → ((VtxDeg‘𝐺)‘𝑁) = ((♯‘{𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) +_𝑒 (♯‘{𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}})))
124	113, 123	syl 17	. . 3 ⊢ (𝜑 → ((VtxDeg‘𝐺)‘𝑁) = ((♯‘{𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) +_𝑒 (♯‘{𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}})))
125		vtxdun.vh	. . . . 5 ⊢ (𝜑 → (Vtx‘𝐻) = 𝑉)
126	113, 125	eleqtrrd 2834	. . . 4 ⊢ (𝜑 → 𝑁 ∈ (Vtx‘𝐻))
127		eqid 2730	. . . . 5 ⊢ (Vtx‘𝐻) = (Vtx‘𝐻)
128		eqid 2730	. . . . 5 ⊢ dom 𝐽 = dom 𝐽
129	127, 53, 128	vtxdgval 28992	. . . 4 ⊢ (𝑁 ∈ (Vtx‘𝐻) → ((VtxDeg‘𝐻)‘𝑁) = ((♯‘{𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) +_𝑒 (♯‘{𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}})))
130	126, 129	syl 17	. . 3 ⊢ (𝜑 → ((VtxDeg‘𝐻)‘𝑁) = ((♯‘{𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) +_𝑒 (♯‘{𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}})))
131	124, 130	oveq12d 7429	. 2 ⊢ (𝜑 → (((VtxDeg‘𝐺)‘𝑁) +_𝑒 ((VtxDeg‘𝐻)‘𝑁)) = (((♯‘{𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) +_𝑒 (♯‘{𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}})) +_𝑒 ((♯‘{𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) +_𝑒 (♯‘{𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}))))
132	112, 120, 131	3eqtr4d 2780	1 ⊢ (𝜑 → ((VtxDeg‘𝑈)‘𝑁) = (((VtxDeg‘𝐺)‘𝑁) +_𝑒 ((VtxDeg‘𝐻)‘𝑁)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 394 ∨ wo 843 = wceq 1539 ∈ wcel 2104 {cab 2707 {crab 3430 Vcvv 3472 ∪ cun 3945 ∩ cin 3946 ⊆ wss 3947 ∅c0 4321 {csn 4627 dom cdm 5675 Fun wfun 6536 Fn wfn 6537 ‘cfv 6542 (class class class)co 7411 ℕ₀^*cxnn0 12548 +_𝑒 cxad 13094 ♯chash 14294 Vtxcvtx 28523 iEdgciedg 28524 VtxDegcvtxdg 28989

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2701 ax-rep 5284 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7727 ax-cnex 11168 ax-resscn 11169 ax-1cn 11170 ax-icn 11171 ax-addcl 11172 ax-addrcl 11173 ax-mulcl 11174 ax-mulrcl 11175 ax-mulcom 11176 ax-addass 11177 ax-mulass 11178 ax-distr 11179 ax-i2m1 11180 ax-1ne0 11181 ax-1rid 11182 ax-rnegex 11183 ax-rrecex 11184 ax-cnre 11185 ax-pre-lttri 11186 ax-pre-lttrn 11187 ax-pre-ltadd 11188 ax-pre-mulgt0 11189

This theorem depends on definitions: df-bi 206 df-an 395 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2532 df-eu 2561 df-clab 2708 df-cleq 2722 df-clel 2808 df-nfc 2883 df-ne 2939 df-nel 3045 df-ral 3060 df-rex 3069 df-reu 3375 df-rab 3431 df-v 3474 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3966 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-int 4950 df-iun 4998 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5573 df-eprel 5579 df-po 5587 df-so 5588 df-fr 5630 df-we 5632 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-pred 6299 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6494 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-riota 7367 df-ov 7414 df-oprab 7415 df-mpo 7416 df-om 7858 df-1st 7977 df-2nd 7978 df-frecs 8268 df-wrecs 8299 df-recs 8373 df-rdg 8412 df-1o 8468 df-oadd 8472 df-er 8705 df-en 8942 df-dom 8943 df-sdom 8944 df-fin 8945 df-dju 9898 df-card 9936 df-pnf 11254 df-mnf 11255 df-xr 11256 df-ltxr 11257 df-le 11258 df-sub 11450 df-neg 11451 df-nn 12217 df-n0 12477 df-xnn0 12549 df-z 12563 df-uz 12827 df-xadd 13097 df-hash 14295 df-vtxdg 28990

This theorem is referenced by: vtxdfiun 29006 vtxduhgrun 29007 p1evtxdeqlem 29036

W3C validator