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 29282

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 3428	. . . . . . . 8 ⊢ {𝑥 ∈ dom (iEdg‘𝑈) ∣ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)} = {𝑥 ∣ (𝑥 ∈ dom (iEdg‘𝑈) ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))}
2		vtxdun.u	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (iEdg‘𝑈) = (𝐼 ∪ 𝐽))
3	2	dmeqd 5902	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom (iEdg‘𝑈) = dom (𝐼 ∪ 𝐽))
4		dmun 5907	. . . . . . . . . . . . . 14 ⊢ dom (𝐼 ∪ 𝐽) = (dom 𝐼 ∪ dom 𝐽)
5	3, 4	eqtrdi 2783	. . . . . . . . . . . . 13 ⊢ (𝜑 → dom (iEdg‘𝑈) = (dom 𝐼 ∪ dom 𝐽))
6	5	eleq2d 2814	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑥 ∈ dom (iEdg‘𝑈) ↔ 𝑥 ∈ (dom 𝐼 ∪ dom 𝐽)))
7		elun 4144	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (dom 𝐼 ∪ dom 𝐽) ↔ (𝑥 ∈ dom 𝐼 ∨ 𝑥 ∈ dom 𝐽))
8	6, 7	bitrdi 287	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ dom (iEdg‘𝑈) ↔ (𝑥 ∈ dom 𝐼 ∨ 𝑥 ∈ dom 𝐽)))
9	8	anbi1d 629	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑥 ∈ dom (iEdg‘𝑈) ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)) ↔ ((𝑥 ∈ dom 𝐼 ∨ 𝑥 ∈ dom 𝐽) ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))))
10		andir 1007	. . . . . . . . . 10 ⊢ (((𝑥 ∈ dom 𝐼 ∨ 𝑥 ∈ dom 𝐽) ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)) ↔ ((𝑥 ∈ dom 𝐼 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)) ∨ (𝑥 ∈ dom 𝐽 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))))
11	9, 10	bitrdi 287	. . . . . . . . 9 ⊢ (𝜑 → ((𝑥 ∈ dom (iEdg‘𝑈) ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)) ↔ ((𝑥 ∈ dom 𝐼 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)) ∨ (𝑥 ∈ dom 𝐽 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)))))
12	11	abbidv 2796	. . . . . . . 8 ⊢ (𝜑 → {𝑥 ∣ (𝑥 ∈ dom (iEdg‘𝑈) ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))} = {𝑥 ∣ ((𝑥 ∈ dom 𝐼 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)) ∨ (𝑥 ∈ dom 𝐽 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)))})
13	1, 12	eqtrid 2779	. . . . . . 7 ⊢ (𝜑 → {𝑥 ∈ dom (iEdg‘𝑈) ∣ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)} = {𝑥 ∣ ((𝑥 ∈ dom 𝐼 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)) ∨ (𝑥 ∈ dom 𝐽 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)))})
14		unab 4294	. . . . . . . . 9 ⊢ ({𝑥 ∣ (𝑥 ∈ dom 𝐼 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))} ∪ {𝑥 ∣ (𝑥 ∈ dom 𝐽 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))}) = {𝑥 ∣ ((𝑥 ∈ dom 𝐼 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)) ∨ (𝑥 ∈ dom 𝐽 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)))}
15	14	eqcomi 2736	. . . . . . . 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 3428	. . . . . . . . 9 ⊢ {𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)} = {𝑥 ∣ (𝑥 ∈ dom 𝐼 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))}
18	2	fveq1d 6893	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((iEdg‘𝑈)‘𝑥) = ((𝐼 ∪ 𝐽)‘𝑥))
19	18	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐼) → ((iEdg‘𝑈)‘𝑥) = ((𝐼 ∪ 𝐽)‘𝑥))
20		vtxdun.fi	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → Fun 𝐼)
21	20	funfnd 6578	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐼 Fn dom 𝐼)
22	21	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐼) → 𝐼 Fn dom 𝐼)
23		vtxdun.fj	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → Fun 𝐽)
24	23	funfnd 6578	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐽 Fn dom 𝐽)
25	24	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐼) → 𝐽 Fn dom 𝐽)
26		vtxdun.d	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (dom 𝐼 ∩ dom 𝐽) = ∅)
27	26	anim1i 614	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐼) → ((dom 𝐼 ∩ dom 𝐽) = ∅ ∧ 𝑥 ∈ dom 𝐼))
28		fvun1 6983	. . . . . . . . . . . . 13 ⊢ ((𝐼 Fn dom 𝐼 ∧ 𝐽 Fn dom 𝐽 ∧ ((dom 𝐼 ∩ dom 𝐽) = ∅ ∧ 𝑥 ∈ dom 𝐼)) → ((𝐼 ∪ 𝐽)‘𝑥) = (𝐼‘𝑥))
29	22, 25, 27, 28	syl3anc 1369	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐼) → ((𝐼 ∪ 𝐽)‘𝑥) = (𝐼‘𝑥))
30	19, 29	eqtrd 2767	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐼) → ((iEdg‘𝑈)‘𝑥) = (𝐼‘𝑥))
31	30	eleq2d 2814	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐼) → (𝑁 ∈ ((iEdg‘𝑈)‘𝑥) ↔ 𝑁 ∈ (𝐼‘𝑥)))
32	31	rabbidva 3434	. . . . . . . . 9 ⊢ (𝜑 → {𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)} = {𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)})
33	17, 32	eqtr3id 2781	. . . . . . . 8 ⊢ (𝜑 → {𝑥 ∣ (𝑥 ∈ dom 𝐼 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))} = {𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)})
34		df-rab 3428	. . . . . . . . 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 614	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐽) → ((dom 𝐼 ∩ dom 𝐽) = ∅ ∧ 𝑥 ∈ dom 𝐽))
39		fvun2 6984	. . . . . . . . . . . . 13 ⊢ ((𝐼 Fn dom 𝐼 ∧ 𝐽 Fn dom 𝐽 ∧ ((dom 𝐼 ∩ dom 𝐽) = ∅ ∧ 𝑥 ∈ dom 𝐽)) → ((𝐼 ∪ 𝐽)‘𝑥) = (𝐽‘𝑥))
40	36, 37, 38, 39	syl3anc 1369	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐽) → ((𝐼 ∪ 𝐽)‘𝑥) = (𝐽‘𝑥))
41	35, 40	eqtrd 2767	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐽) → ((iEdg‘𝑈)‘𝑥) = (𝐽‘𝑥))
42	41	eleq2d 2814	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐽) → (𝑁 ∈ ((iEdg‘𝑈)‘𝑥) ↔ 𝑁 ∈ (𝐽‘𝑥)))
43	42	rabbidva 3434	. . . . . . . . 9 ⊢ (𝜑 → {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)} = {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)})
44	34, 43	eqtr3id 2781	. . . . . . . 8 ⊢ (𝜑 → {𝑥 ∣ (𝑥 ∈ dom 𝐽 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))} = {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)})
45	33, 44	uneq12d 4160	. . . . . . 7 ⊢ (𝜑 → ({𝑥 ∣ (𝑥 ∈ dom 𝐼 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))} ∪ {𝑥 ∣ (𝑥 ∈ dom 𝐽 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))}) = ({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∪ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}))
46	13, 16, 45	3eqtrd 2771	. . . . . 6 ⊢ (𝜑 → {𝑥 ∈ dom (iEdg‘𝑈) ∣ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)} = ({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∪ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}))
47	46	fveq2d 6895	. . . . 5 ⊢ (𝜑 → (♯‘{𝑥 ∈ dom (iEdg‘𝑈) ∣ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)}) = (♯‘({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∪ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)})))
48		vtxdun.i	. . . . . . . . . 10 ⊢ 𝐼 = (iEdg‘𝐺)
49	48	fvexi 6905	. . . . . . . . 9 ⊢ 𝐼 ∈ V
50	49	dmex 7911	. . . . . . . 8 ⊢ dom 𝐼 ∈ V
51	50	rabex 5328	. . . . . . 7 ⊢ {𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∈ V
52	51	a1i 11	. . . . . 6 ⊢ (𝜑 → {𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∈ V)
53		vtxdun.j	. . . . . . . . . 10 ⊢ 𝐽 = (iEdg‘𝐻)
54	53	fvexi 6905	. . . . . . . . 9 ⊢ 𝐽 ∈ V
55	54	dmex 7911	. . . . . . . 8 ⊢ dom 𝐽 ∈ V
56	55	rabex 5328	. . . . . . 7 ⊢ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)} ∈ V
57	56	a1i 11	. . . . . 6 ⊢ (𝜑 → {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)} ∈ V)
58		ssrab2 4073	. . . . . . . . 9 ⊢ {𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ⊆ dom 𝐼
59		ssrab2 4073	. . . . . . . . 9 ⊢ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)} ⊆ dom 𝐽
60		ss2in 4232	. . . . . . . . 9 ⊢ (({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ⊆ dom 𝐼 ∧ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)} ⊆ dom 𝐽) → ({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∩ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) ⊆ (dom 𝐼 ∩ dom 𝐽))
61	58, 59, 60	mp2an 691	. . . . . . . 8 ⊢ ({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∩ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) ⊆ (dom 𝐼 ∩ dom 𝐽)
62	61, 26	sseqtrid 4030	. . . . . . 7 ⊢ (𝜑 → ({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∩ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) ⊆ ∅)
63		ss0 4394	. . . . . . 7 ⊢ (({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∩ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) ⊆ ∅ → ({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∩ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) = ∅)
64	62, 63	syl 17	. . . . . 6 ⊢ (𝜑 → ({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∩ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) = ∅)
65		hashunx 14369	. . . . . 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 2767	. . . 4 ⊢ (𝜑 → (♯‘{𝑥 ∈ dom (iEdg‘𝑈) ∣ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)}) = ((♯‘{𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) +_𝑒 (♯‘{𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)})))
68		df-rab 3428	. . . . . . . 8 ⊢ {𝑥 ∈ dom (iEdg‘𝑈) ∣ ((iEdg‘𝑈)‘𝑥) = {𝑁}} = {𝑥 ∣ (𝑥 ∈ dom (iEdg‘𝑈) ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})}
69	8	anbi1d 629	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑥 ∈ dom (iEdg‘𝑈) ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}) ↔ ((𝑥 ∈ dom 𝐼 ∨ 𝑥 ∈ dom 𝐽) ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})))
70		andir 1007	. . . . . . . . . 10 ⊢ (((𝑥 ∈ dom 𝐼 ∨ 𝑥 ∈ dom 𝐽) ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}) ↔ ((𝑥 ∈ dom 𝐼 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}) ∨ (𝑥 ∈ dom 𝐽 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})))
71	69, 70	bitrdi 287	. . . . . . . . 9 ⊢ (𝜑 → ((𝑥 ∈ dom (iEdg‘𝑈) ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}) ↔ ((𝑥 ∈ dom 𝐼 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}) ∨ (𝑥 ∈ dom 𝐽 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}))))
72	71	abbidv 2796	. . . . . . . 8 ⊢ (𝜑 → {𝑥 ∣ (𝑥 ∈ dom (iEdg‘𝑈) ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})} = {𝑥 ∣ ((𝑥 ∈ dom 𝐼 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}) ∨ (𝑥 ∈ dom 𝐽 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}))})
73	68, 72	eqtrid 2779	. . . . . . 7 ⊢ (𝜑 → {𝑥 ∈ dom (iEdg‘𝑈) ∣ ((iEdg‘𝑈)‘𝑥) = {𝑁}} = {𝑥 ∣ ((𝑥 ∈ dom 𝐼 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}) ∨ (𝑥 ∈ dom 𝐽 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}))})
74		unab 4294	. . . . . . . . 9 ⊢ ({𝑥 ∣ (𝑥 ∈ dom 𝐼 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})} ∪ {𝑥 ∣ (𝑥 ∈ dom 𝐽 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})}) = {𝑥 ∣ ((𝑥 ∈ dom 𝐼 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}) ∨ (𝑥 ∈ dom 𝐽 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}))}
75	74	eqcomi 2736	. . . . . . . 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 3428	. . . . . . . . 9 ⊢ {𝑥 ∈ dom 𝐼 ∣ ((iEdg‘𝑈)‘𝑥) = {𝑁}} = {𝑥 ∣ (𝑥 ∈ dom 𝐼 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})}
78	30	eqeq1d 2729	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐼) → (((iEdg‘𝑈)‘𝑥) = {𝑁} ↔ (𝐼‘𝑥) = {𝑁}))
79	78	rabbidva 3434	. . . . . . . . 9 ⊢ (𝜑 → {𝑥 ∈ dom 𝐼 ∣ ((iEdg‘𝑈)‘𝑥) = {𝑁}} = {𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}})
80	77, 79	eqtr3id 2781	. . . . . . . 8 ⊢ (𝜑 → {𝑥 ∣ (𝑥 ∈ dom 𝐼 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})} = {𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}})
81		df-rab 3428	. . . . . . . . 9 ⊢ {𝑥 ∈ dom 𝐽 ∣ ((iEdg‘𝑈)‘𝑥) = {𝑁}} = {𝑥 ∣ (𝑥 ∈ dom 𝐽 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})}
82	41	eqeq1d 2729	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐽) → (((iEdg‘𝑈)‘𝑥) = {𝑁} ↔ (𝐽‘𝑥) = {𝑁}))
83	82	rabbidva 3434	. . . . . . . . 9 ⊢ (𝜑 → {𝑥 ∈ dom 𝐽 ∣ ((iEdg‘𝑈)‘𝑥) = {𝑁}} = {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}})
84	81, 83	eqtr3id 2781	. . . . . . . 8 ⊢ (𝜑 → {𝑥 ∣ (𝑥 ∈ dom 𝐽 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})} = {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}})
85	80, 84	uneq12d 4160	. . . . . . 7 ⊢ (𝜑 → ({𝑥 ∣ (𝑥 ∈ dom 𝐼 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})} ∪ {𝑥 ∣ (𝑥 ∈ dom 𝐽 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})}) = ({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∪ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}))
86	73, 76, 85	3eqtrd 2771	. . . . . 6 ⊢ (𝜑 → {𝑥 ∈ dom (iEdg‘𝑈) ∣ ((iEdg‘𝑈)‘𝑥) = {𝑁}} = ({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∪ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}))
87	86	fveq2d 6895	. . . . 5 ⊢ (𝜑 → (♯‘{𝑥 ∈ dom (iEdg‘𝑈) ∣ ((iEdg‘𝑈)‘𝑥) = {𝑁}}) = (♯‘({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∪ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}})))
88	50	rabex 5328	. . . . . . 7 ⊢ {𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∈ V
89	88	a1i 11	. . . . . 6 ⊢ (𝜑 → {𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∈ V)
90	55	rabex 5328	. . . . . . 7 ⊢ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}} ∈ V
91	90	a1i 11	. . . . . 6 ⊢ (𝜑 → {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}} ∈ V)
92		ssrab2 4073	. . . . . . . . 9 ⊢ {𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ⊆ dom 𝐼
93		ssrab2 4073	. . . . . . . . 9 ⊢ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}} ⊆ dom 𝐽
94		ss2in 4232	. . . . . . . . 9 ⊢ (({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ⊆ dom 𝐼 ∧ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}} ⊆ dom 𝐽) → ({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∩ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}) ⊆ (dom 𝐼 ∩ dom 𝐽))
95	92, 93, 94	mp2an 691	. . . . . . . 8 ⊢ ({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∩ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}) ⊆ (dom 𝐼 ∩ dom 𝐽)
96	95, 26	sseqtrid 4030	. . . . . . 7 ⊢ (𝜑 → ({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∩ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}) ⊆ ∅)
97		ss0 4394	. . . . . . 7 ⊢ (({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∩ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}) ⊆ ∅ → ({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∩ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}) = ∅)
98	96, 97	syl 17	. . . . . 6 ⊢ (𝜑 → ({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∩ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}) = ∅)
99		hashunx 14369	. . . . . 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 2767	. . . 4 ⊢ (𝜑 → (♯‘{𝑥 ∈ dom (iEdg‘𝑈) ∣ ((iEdg‘𝑈)‘𝑥) = {𝑁}}) = ((♯‘{𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}}) +_𝑒 (♯‘{𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}})))
102	67, 101	oveq12d 7432	. . 3 ⊢ (𝜑 → ((♯‘{𝑥 ∈ dom (iEdg‘𝑈) ∣ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)}) +_𝑒 (♯‘{𝑥 ∈ dom (iEdg‘𝑈) ∣ ((iEdg‘𝑈)‘𝑥) = {𝑁}})) = (((♯‘{𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) +_𝑒 (♯‘{𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)})) +_𝑒 ((♯‘{𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}}) +_𝑒 (♯‘{𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}))))
103		hashxnn0 14322	. . . . 5 ⊢ ({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∈ V → (♯‘{𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) ∈ ℕ₀^*)
104	52, 103	syl 17	. . . 4 ⊢ (𝜑 → (♯‘{𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) ∈ ℕ₀^*)
105		hashxnn0 14322	. . . . 5 ⊢ ({𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)} ∈ V → (♯‘{𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) ∈ ℕ₀^*)
106	57, 105	syl 17	. . . 4 ⊢ (𝜑 → (♯‘{𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) ∈ ℕ₀^*)
107		hashxnn0 14322	. . . . 5 ⊢ ({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∈ V → (♯‘{𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}}) ∈ ℕ₀^*)
108	89, 107	syl 17	. . . 4 ⊢ (𝜑 → (♯‘{𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}}) ∈ ℕ₀^*)
109		hashxnn0 14322	. . . . 5 ⊢ ({𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}} ∈ V → (♯‘{𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}) ∈ ℕ₀^*)
110	91, 109	syl 17	. . . 4 ⊢ (𝜑 → (♯‘{𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}) ∈ ℕ₀^*)
111	104, 106, 108, 110	xnn0add4d 13307	. . 3 ⊢ (𝜑 → (((♯‘{𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) +_𝑒 (♯‘{𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)})) +_𝑒 ((♯‘{𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}}) +_𝑒 (♯‘{𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}))) = (((♯‘{𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) +_𝑒 (♯‘{𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}})) +_𝑒 ((♯‘{𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) +_𝑒 (♯‘{𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}))))
112	102, 111	eqtrd 2767	. 2 ⊢ (𝜑 → ((♯‘{𝑥 ∈ dom (iEdg‘𝑈) ∣ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)}) +_𝑒 (♯‘{𝑥 ∈ dom (iEdg‘𝑈) ∣ ((iEdg‘𝑈)‘𝑥) = {𝑁}})) = (((♯‘{𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) +_𝑒 (♯‘{𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}})) +_𝑒 ((♯‘{𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) +_𝑒 (♯‘{𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}))))
113		vtxdun.n	. . . 4 ⊢ (𝜑 → 𝑁 ∈ 𝑉)
114		vtxdun.vu	. . . 4 ⊢ (𝜑 → (Vtx‘𝑈) = 𝑉)
115	113, 114	eleqtrrd 2831	. . 3 ⊢ (𝜑 → 𝑁 ∈ (Vtx‘𝑈))
116		eqid 2727	. . . 4 ⊢ (Vtx‘𝑈) = (Vtx‘𝑈)
117		eqid 2727	. . . 4 ⊢ (iEdg‘𝑈) = (iEdg‘𝑈)
118		eqid 2727	. . . 4 ⊢ dom (iEdg‘𝑈) = dom (iEdg‘𝑈)
119	116, 117, 118	vtxdgval 29269	. . 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 2727	. . . . 5 ⊢ dom 𝐼 = dom 𝐼
123	121, 48, 122	vtxdgval 29269	. . . 4 ⊢ (𝑁 ∈ 𝑉 → ((VtxDeg‘𝐺)‘𝑁) = ((♯‘{𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) +_𝑒 (♯‘{𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}})))
124	113, 123	syl 17	. . 3 ⊢ (𝜑 → ((VtxDeg‘𝐺)‘𝑁) = ((♯‘{𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) +_𝑒 (♯‘{𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}})))
125		vtxdun.vh	. . . . 5 ⊢ (𝜑 → (Vtx‘𝐻) = 𝑉)
126	113, 125	eleqtrrd 2831	. . . 4 ⊢ (𝜑 → 𝑁 ∈ (Vtx‘𝐻))
127		eqid 2727	. . . . 5 ⊢ (Vtx‘𝐻) = (Vtx‘𝐻)
128		eqid 2727	. . . . 5 ⊢ dom 𝐽 = dom 𝐽
129	127, 53, 128	vtxdgval 29269	. . . 4 ⊢ (𝑁 ∈ (Vtx‘𝐻) → ((VtxDeg‘𝐻)‘𝑁) = ((♯‘{𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) +_𝑒 (♯‘{𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}})))
130	126, 129	syl 17	. . 3 ⊢ (𝜑 → ((VtxDeg‘𝐻)‘𝑁) = ((♯‘{𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) +_𝑒 (♯‘{𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}})))
131	124, 130	oveq12d 7432	. 2 ⊢ (𝜑 → (((VtxDeg‘𝐺)‘𝑁) +_𝑒 ((VtxDeg‘𝐻)‘𝑁)) = (((♯‘{𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) +_𝑒 (♯‘{𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}})) +_𝑒 ((♯‘{𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) +_𝑒 (♯‘{𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}))))
132	112, 120, 131	3eqtr4d 2777	1 ⊢ (𝜑 → ((VtxDeg‘𝑈)‘𝑁) = (((VtxDeg‘𝐺)‘𝑁) +_𝑒 ((VtxDeg‘𝐻)‘𝑁)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∨ wo 846 = wceq 1534 ∈ wcel 2099 {cab 2704 {crab 3427 Vcvv 3469 ∪ cun 3942 ∩ cin 3943 ⊆ wss 3944 ∅c0 4318 {csn 4624 dom cdm 5672 Fun wfun 6536 Fn wfn 6537 ‘cfv 6542 (class class class)co 7414 ℕ₀^*cxnn0 12566 +_𝑒 cxad 13114 ♯chash 14313 Vtxcvtx 28796 iEdgciedg 28797 VtxDegcvtxdg 29266

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2164 ax-ext 2698 ax-rep 5279 ax-sep 5293 ax-nul 5300 ax-pow 5359 ax-pr 5423 ax-un 7734 ax-cnex 11186 ax-resscn 11187 ax-1cn 11188 ax-icn 11189 ax-addcl 11190 ax-addrcl 11191 ax-mulcl 11192 ax-mulrcl 11193 ax-mulcom 11194 ax-addass 11195 ax-mulass 11196 ax-distr 11197 ax-i2m1 11198 ax-1ne0 11199 ax-1rid 11200 ax-rnegex 11201 ax-rrecex 11202 ax-cnre 11203 ax-pre-lttri 11204 ax-pre-lttrn 11205 ax-pre-ltadd 11206 ax-pre-mulgt0 11207

This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3or 1086 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-eu 2558 df-clab 2705 df-cleq 2719 df-clel 2805 df-nfc 2880 df-ne 2936 df-nel 3042 df-ral 3057 df-rex 3066 df-reu 3372 df-rab 3428 df-v 3471 df-sbc 3775 df-csb 3890 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-pss 3963 df-nul 4319 df-if 4525 df-pw 4600 df-sn 4625 df-pr 4627 df-op 4631 df-uni 4904 df-int 4945 df-iun 4993 df-br 5143 df-opab 5205 df-mpt 5226 df-tr 5260 df-id 5570 df-eprel 5576 df-po 5584 df-so 5585 df-fr 5627 df-we 5629 df-xp 5678 df-rel 5679 df-cnv 5680 df-co 5681 df-dm 5682 df-rn 5683 df-res 5684 df-ima 5685 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 7370 df-ov 7417 df-oprab 7418 df-mpo 7419 df-om 7865 df-1st 7987 df-2nd 7988 df-frecs 8280 df-wrecs 8311 df-recs 8385 df-rdg 8424 df-1o 8480 df-oadd 8484 df-er 8718 df-en 8956 df-dom 8957 df-sdom 8958 df-fin 8959 df-dju 9916 df-card 9954 df-pnf 11272 df-mnf 11273 df-xr 11274 df-ltxr 11275 df-le 11276 df-sub 11468 df-neg 11469 df-nn 12235 df-n0 12495 df-xnn0 12567 df-z 12581 df-uz 12845 df-xadd 13117 df-hash 14314 df-vtxdg 29267

This theorem is referenced by: vtxdfiun 29283 vtxduhgrun 29284 p1evtxdeqlem 29313

W3C validator