vtxdun - Mathbox for Alexander van der Vekens

	Mathbox for Alexander van der Vekens		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > vtxdun		Structured version Visualization version GIF version

Theorem vtxdun 40696

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 2905	. . . . . . . 8 ⊢ {𝑥 ∈ dom (iEdg‘𝑈) ∣ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)} = {𝑥 ∣ (𝑥 ∈ dom (iEdg‘𝑈) ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))}
2		vtxdun.u	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (iEdg‘𝑈) = (𝐼 ∪ 𝐽))
3	2	dmeqd 5248	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom (iEdg‘𝑈) = dom (𝐼 ∪ 𝐽))
4		dmun 5253	. . . . . . . . . . . . . 14 ⊢ dom (𝐼 ∪ 𝐽) = (dom 𝐼 ∪ dom 𝐽)
5	3, 4	syl6eq 2660	. . . . . . . . . . . . 13 ⊢ (𝜑 → dom (iEdg‘𝑈) = (dom 𝐼 ∪ dom 𝐽))
6	5	eleq2d 2673	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑥 ∈ dom (iEdg‘𝑈) ↔ 𝑥 ∈ (dom 𝐼 ∪ dom 𝐽)))
7		elun 3715	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (dom 𝐼 ∪ dom 𝐽) ↔ (𝑥 ∈ dom 𝐼 ∨ 𝑥 ∈ dom 𝐽))
8	6, 7	syl6bb 275	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ dom (iEdg‘𝑈) ↔ (𝑥 ∈ dom 𝐼 ∨ 𝑥 ∈ dom 𝐽)))
9	8	anbi1d 737	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑥 ∈ dom (iEdg‘𝑈) ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)) ↔ ((𝑥 ∈ dom 𝐼 ∨ 𝑥 ∈ dom 𝐽) ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))))
10		andir 908	. . . . . . . . . 10 ⊢ (((𝑥 ∈ dom 𝐼 ∨ 𝑥 ∈ dom 𝐽) ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)) ↔ ((𝑥 ∈ dom 𝐼 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)) ∨ (𝑥 ∈ dom 𝐽 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))))
11	9, 10	syl6bb 275	. . . . . . . . 9 ⊢ (𝜑 → ((𝑥 ∈ dom (iEdg‘𝑈) ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)) ↔ ((𝑥 ∈ dom 𝐼 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)) ∨ (𝑥 ∈ dom 𝐽 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)))))
12	11	abbidv 2728	. . . . . . . 8 ⊢ (𝜑 → {𝑥 ∣ (𝑥 ∈ dom (iEdg‘𝑈) ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))} = {𝑥 ∣ ((𝑥 ∈ dom 𝐼 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)) ∨ (𝑥 ∈ dom 𝐽 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)))})
13	1, 12	syl5eq 2656	. . . . . . 7 ⊢ (𝜑 → {𝑥 ∈ dom (iEdg‘𝑈) ∣ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)} = {𝑥 ∣ ((𝑥 ∈ dom 𝐼 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)) ∨ (𝑥 ∈ dom 𝐽 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)))})
14		unab 3853	. . . . . . . . 9 ⊢ ({𝑥 ∣ (𝑥 ∈ dom 𝐼 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))} ∪ {𝑥 ∣ (𝑥 ∈ dom 𝐽 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))}) = {𝑥 ∣ ((𝑥 ∈ dom 𝐼 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)) ∨ (𝑥 ∈ dom 𝐽 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)))}
15	14	eqcomi 2619	. . . . . . . 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 2905	. . . . . . . . 9 ⊢ {𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)} = {𝑥 ∣ (𝑥 ∈ dom 𝐼 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))}
18	2	fveq1d 6105	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((iEdg‘𝑈)‘𝑥) = ((𝐼 ∪ 𝐽)‘𝑥))
19	18	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐼) → ((iEdg‘𝑈)‘𝑥) = ((𝐼 ∪ 𝐽)‘𝑥))
20		vtxdun.fi	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → Fun 𝐼)
21		funfn 5833	. . . . . . . . . . . . . . 15 ⊢ (Fun 𝐼 ↔ 𝐼 Fn dom 𝐼)
22	20, 21	sylib 207	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐼 Fn dom 𝐼)
23	22	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐼) → 𝐼 Fn dom 𝐼)
24		vtxdun.fj	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → Fun 𝐽)
25		funfn 5833	. . . . . . . . . . . . . . 15 ⊢ (Fun 𝐽 ↔ 𝐽 Fn dom 𝐽)
26	24, 25	sylib 207	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐽 Fn dom 𝐽)
27	26	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐼) → 𝐽 Fn dom 𝐽)
28		vtxdun.d	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (dom 𝐼 ∩ dom 𝐽) = ∅)
29	28	anim1i 590	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐼) → ((dom 𝐼 ∩ dom 𝐽) = ∅ ∧ 𝑥 ∈ dom 𝐼))
30		fvun1 6179	. . . . . . . . . . . . 13 ⊢ ((𝐼 Fn dom 𝐼 ∧ 𝐽 Fn dom 𝐽 ∧ ((dom 𝐼 ∩ dom 𝐽) = ∅ ∧ 𝑥 ∈ dom 𝐼)) → ((𝐼 ∪ 𝐽)‘𝑥) = (𝐼‘𝑥))
31	23, 27, 29, 30	syl3anc 1318	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐼) → ((𝐼 ∪ 𝐽)‘𝑥) = (𝐼‘𝑥))
32	19, 31	eqtrd 2644	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐼) → ((iEdg‘𝑈)‘𝑥) = (𝐼‘𝑥))
33	32	eleq2d 2673	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐼) → (𝑁 ∈ ((iEdg‘𝑈)‘𝑥) ↔ 𝑁 ∈ (𝐼‘𝑥)))
34	33	rabbidva 3163	. . . . . . . . 9 ⊢ (𝜑 → {𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)} = {𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)})
35	17, 34	syl5eqr 2658	. . . . . . . 8 ⊢ (𝜑 → {𝑥 ∣ (𝑥 ∈ dom 𝐼 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))} = {𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)})
36		df-rab 2905	. . . . . . . . 9 ⊢ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)} = {𝑥 ∣ (𝑥 ∈ dom 𝐽 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))}
37	18	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐽) → ((iEdg‘𝑈)‘𝑥) = ((𝐼 ∪ 𝐽)‘𝑥))
38	22	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐽) → 𝐼 Fn dom 𝐼)
39	26	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐽) → 𝐽 Fn dom 𝐽)
40	28	anim1i 590	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐽) → ((dom 𝐼 ∩ dom 𝐽) = ∅ ∧ 𝑥 ∈ dom 𝐽))
41		fvun2 6180	. . . . . . . . . . . . 13 ⊢ ((𝐼 Fn dom 𝐼 ∧ 𝐽 Fn dom 𝐽 ∧ ((dom 𝐼 ∩ dom 𝐽) = ∅ ∧ 𝑥 ∈ dom 𝐽)) → ((𝐼 ∪ 𝐽)‘𝑥) = (𝐽‘𝑥))
42	38, 39, 40, 41	syl3anc 1318	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐽) → ((𝐼 ∪ 𝐽)‘𝑥) = (𝐽‘𝑥))
43	37, 42	eqtrd 2644	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐽) → ((iEdg‘𝑈)‘𝑥) = (𝐽‘𝑥))
44	43	eleq2d 2673	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐽) → (𝑁 ∈ ((iEdg‘𝑈)‘𝑥) ↔ 𝑁 ∈ (𝐽‘𝑥)))
45	44	rabbidva 3163	. . . . . . . . 9 ⊢ (𝜑 → {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)} = {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)})
46	36, 45	syl5eqr 2658	. . . . . . . 8 ⊢ (𝜑 → {𝑥 ∣ (𝑥 ∈ dom 𝐽 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))} = {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)})
47	35, 46	uneq12d 3730	. . . . . . 7 ⊢ (𝜑 → ({𝑥 ∣ (𝑥 ∈ dom 𝐼 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))} ∪ {𝑥 ∣ (𝑥 ∈ dom 𝐽 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))}) = ({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∪ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}))
48	13, 16, 47	3eqtrd 2648	. . . . . 6 ⊢ (𝜑 → {𝑥 ∈ dom (iEdg‘𝑈) ∣ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)} = ({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∪ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}))
49	48	fveq2d 6107	. . . . 5 ⊢ (𝜑 → (#‘{𝑥 ∈ dom (iEdg‘𝑈) ∣ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)}) = (#‘({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∪ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)})))
50		vtxdun.i	. . . . . . . . . 10 ⊢ 𝐼 = (iEdg‘𝐺)
51		fvex 6113	. . . . . . . . . 10 ⊢ (iEdg‘𝐺) ∈ V
52	50, 51	eqeltri 2684	. . . . . . . . 9 ⊢ 𝐼 ∈ V
53	52	dmex 6991	. . . . . . . 8 ⊢ dom 𝐼 ∈ V
54	53	rabex 4740	. . . . . . 7 ⊢ {𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∈ V
55	54	a1i 11	. . . . . 6 ⊢ (𝜑 → {𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∈ V)
56		vtxdun.j	. . . . . . . . . 10 ⊢ 𝐽 = (iEdg‘𝐻)
57		fvex 6113	. . . . . . . . . 10 ⊢ (iEdg‘𝐻) ∈ V
58	56, 57	eqeltri 2684	. . . . . . . . 9 ⊢ 𝐽 ∈ V
59	58	dmex 6991	. . . . . . . 8 ⊢ dom 𝐽 ∈ V
60	59	rabex 4740	. . . . . . 7 ⊢ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)} ∈ V
61	60	a1i 11	. . . . . 6 ⊢ (𝜑 → {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)} ∈ V)
62		ssrab2 3650	. . . . . . . . 9 ⊢ {𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ⊆ dom 𝐼
63		ssrab2 3650	. . . . . . . . 9 ⊢ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)} ⊆ dom 𝐽
64		ss2in 3802	. . . . . . . . 9 ⊢ (({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ⊆ dom 𝐼 ∧ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)} ⊆ dom 𝐽) → ({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∩ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) ⊆ (dom 𝐼 ∩ dom 𝐽))
65	62, 63, 64	mp2an 704	. . . . . . . 8 ⊢ ({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∩ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) ⊆ (dom 𝐼 ∩ dom 𝐽)
66	65, 28	syl5sseq 3616	. . . . . . 7 ⊢ (𝜑 → ({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∩ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) ⊆ ∅)
67		ss0 3926	. . . . . . 7 ⊢ (({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∩ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) ⊆ ∅ → ({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∩ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) = ∅)
68	66, 67	syl 17	. . . . . 6 ⊢ (𝜑 → ({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∩ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) = ∅)
69		hashunx 13036	. . . . . 6 ⊢ (({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∈ V ∧ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)} ∈ V ∧ ({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∩ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) = ∅) → (#‘({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∪ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)})) = ((#‘{𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) +_𝑒 (#‘{𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)})))
70	55, 61, 68, 69	syl3anc 1318	. . . . 5 ⊢ (𝜑 → (#‘({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∪ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)})) = ((#‘{𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) +_𝑒 (#‘{𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)})))
71	49, 70	eqtrd 2644	. . . 4 ⊢ (𝜑 → (#‘{𝑥 ∈ dom (iEdg‘𝑈) ∣ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)}) = ((#‘{𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) +_𝑒 (#‘{𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)})))
72		df-rab 2905	. . . . . . . 8 ⊢ {𝑥 ∈ dom (iEdg‘𝑈) ∣ ((iEdg‘𝑈)‘𝑥) = {𝑁}} = {𝑥 ∣ (𝑥 ∈ dom (iEdg‘𝑈) ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})}
73	8	anbi1d 737	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑥 ∈ dom (iEdg‘𝑈) ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}) ↔ ((𝑥 ∈ dom 𝐼 ∨ 𝑥 ∈ dom 𝐽) ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})))
74		andir 908	. . . . . . . . . 10 ⊢ (((𝑥 ∈ dom 𝐼 ∨ 𝑥 ∈ dom 𝐽) ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}) ↔ ((𝑥 ∈ dom 𝐼 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}) ∨ (𝑥 ∈ dom 𝐽 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})))
75	73, 74	syl6bb 275	. . . . . . . . 9 ⊢ (𝜑 → ((𝑥 ∈ dom (iEdg‘𝑈) ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}) ↔ ((𝑥 ∈ dom 𝐼 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}) ∨ (𝑥 ∈ dom 𝐽 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}))))
76	75	abbidv 2728	. . . . . . . 8 ⊢ (𝜑 → {𝑥 ∣ (𝑥 ∈ dom (iEdg‘𝑈) ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})} = {𝑥 ∣ ((𝑥 ∈ dom 𝐼 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}) ∨ (𝑥 ∈ dom 𝐽 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}))})
77	72, 76	syl5eq 2656	. . . . . . 7 ⊢ (𝜑 → {𝑥 ∈ dom (iEdg‘𝑈) ∣ ((iEdg‘𝑈)‘𝑥) = {𝑁}} = {𝑥 ∣ ((𝑥 ∈ dom 𝐼 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}) ∨ (𝑥 ∈ dom 𝐽 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}))})
78		unab 3853	. . . . . . . . 9 ⊢ ({𝑥 ∣ (𝑥 ∈ dom 𝐼 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})} ∪ {𝑥 ∣ (𝑥 ∈ dom 𝐽 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})}) = {𝑥 ∣ ((𝑥 ∈ dom 𝐼 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}) ∨ (𝑥 ∈ dom 𝐽 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}))}
79	78	eqcomi 2619	. . . . . . . 8 ⊢ {𝑥 ∣ ((𝑥 ∈ dom 𝐼 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}) ∨ (𝑥 ∈ dom 𝐽 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}))} = ({𝑥 ∣ (𝑥 ∈ dom 𝐼 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})} ∪ {𝑥 ∣ (𝑥 ∈ dom 𝐽 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})})
80	79	a1i 11	. . . . . . 7 ⊢ (𝜑 → {𝑥 ∣ ((𝑥 ∈ dom 𝐼 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}) ∨ (𝑥 ∈ dom 𝐽 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}))} = ({𝑥 ∣ (𝑥 ∈ dom 𝐼 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})} ∪ {𝑥 ∣ (𝑥 ∈ dom 𝐽 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})}))
81		df-rab 2905	. . . . . . . . 9 ⊢ {𝑥 ∈ dom 𝐼 ∣ ((iEdg‘𝑈)‘𝑥) = {𝑁}} = {𝑥 ∣ (𝑥 ∈ dom 𝐼 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})}
82	32	eqeq1d 2612	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐼) → (((iEdg‘𝑈)‘𝑥) = {𝑁} ↔ (𝐼‘𝑥) = {𝑁}))
83	82	rabbidva 3163	. . . . . . . . 9 ⊢ (𝜑 → {𝑥 ∈ dom 𝐼 ∣ ((iEdg‘𝑈)‘𝑥) = {𝑁}} = {𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}})
84	81, 83	syl5eqr 2658	. . . . . . . 8 ⊢ (𝜑 → {𝑥 ∣ (𝑥 ∈ dom 𝐼 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})} = {𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}})
85		df-rab 2905	. . . . . . . . 9 ⊢ {𝑥 ∈ dom 𝐽 ∣ ((iEdg‘𝑈)‘𝑥) = {𝑁}} = {𝑥 ∣ (𝑥 ∈ dom 𝐽 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})}
86	43	eqeq1d 2612	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐽) → (((iEdg‘𝑈)‘𝑥) = {𝑁} ↔ (𝐽‘𝑥) = {𝑁}))
87	86	rabbidva 3163	. . . . . . . . 9 ⊢ (𝜑 → {𝑥 ∈ dom 𝐽 ∣ ((iEdg‘𝑈)‘𝑥) = {𝑁}} = {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}})
88	85, 87	syl5eqr 2658	. . . . . . . 8 ⊢ (𝜑 → {𝑥 ∣ (𝑥 ∈ dom 𝐽 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})} = {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}})
89	84, 88	uneq12d 3730	. . . . . . 7 ⊢ (𝜑 → ({𝑥 ∣ (𝑥 ∈ dom 𝐼 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})} ∪ {𝑥 ∣ (𝑥 ∈ dom 𝐽 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})}) = ({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∪ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}))
90	77, 80, 89	3eqtrd 2648	. . . . . 6 ⊢ (𝜑 → {𝑥 ∈ dom (iEdg‘𝑈) ∣ ((iEdg‘𝑈)‘𝑥) = {𝑁}} = ({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∪ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}))
91	90	fveq2d 6107	. . . . 5 ⊢ (𝜑 → (#‘{𝑥 ∈ dom (iEdg‘𝑈) ∣ ((iEdg‘𝑈)‘𝑥) = {𝑁}}) = (#‘({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∪ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}})))
92	53	rabex 4740	. . . . . . 7 ⊢ {𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∈ V
93	92	a1i 11	. . . . . 6 ⊢ (𝜑 → {𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∈ V)
94	59	rabex 4740	. . . . . . 7 ⊢ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}} ∈ V
95	94	a1i 11	. . . . . 6 ⊢ (𝜑 → {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}} ∈ V)
96		ssrab2 3650	. . . . . . . . 9 ⊢ {𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ⊆ dom 𝐼
97		ssrab2 3650	. . . . . . . . 9 ⊢ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}} ⊆ dom 𝐽
98		ss2in 3802	. . . . . . . . 9 ⊢ (({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ⊆ dom 𝐼 ∧ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}} ⊆ dom 𝐽) → ({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∩ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}) ⊆ (dom 𝐼 ∩ dom 𝐽))
99	96, 97, 98	mp2an 704	. . . . . . . 8 ⊢ ({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∩ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}) ⊆ (dom 𝐼 ∩ dom 𝐽)
100	99, 28	syl5sseq 3616	. . . . . . 7 ⊢ (𝜑 → ({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∩ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}) ⊆ ∅)
101		ss0 3926	. . . . . . 7 ⊢ (({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∩ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}) ⊆ ∅ → ({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∩ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}) = ∅)
102	100, 101	syl 17	. . . . . 6 ⊢ (𝜑 → ({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∩ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}) = ∅)
103		hashunx 13036	. . . . . 6 ⊢ (({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∈ V ∧ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}} ∈ V ∧ ({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∩ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}) = ∅) → (#‘({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∪ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}})) = ((#‘{𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}}) +_𝑒 (#‘{𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}})))
104	93, 95, 102, 103	syl3anc 1318	. . . . 5 ⊢ (𝜑 → (#‘({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∪ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}})) = ((#‘{𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}}) +_𝑒 (#‘{𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}})))
105	91, 104	eqtrd 2644	. . . 4 ⊢ (𝜑 → (#‘{𝑥 ∈ dom (iEdg‘𝑈) ∣ ((iEdg‘𝑈)‘𝑥) = {𝑁}}) = ((#‘{𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}}) +_𝑒 (#‘{𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}})))
106	71, 105	oveq12d 6567	. . 3 ⊢ (𝜑 → ((#‘{𝑥 ∈ dom (iEdg‘𝑈) ∣ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)}) +_𝑒 (#‘{𝑥 ∈ dom (iEdg‘𝑈) ∣ ((iEdg‘𝑈)‘𝑥) = {𝑁}})) = (((#‘{𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) +_𝑒 (#‘{𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)})) +_𝑒 ((#‘{𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}}) +_𝑒 (#‘{𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}))))
107		hashxnn0 12989	. . . . 5 ⊢ ({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∈ V → (#‘{𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) ∈ ℕ₀^*)
108	55, 107	syl 17	. . . 4 ⊢ (𝜑 → (#‘{𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) ∈ ℕ₀^*)
109		hashxnn0 12989	. . . . 5 ⊢ ({𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)} ∈ V → (#‘{𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) ∈ ℕ₀^*)
110	61, 109	syl 17	. . . 4 ⊢ (𝜑 → (#‘{𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) ∈ ℕ₀^*)
111		hashxnn0 12989	. . . . 5 ⊢ ({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∈ V → (#‘{𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}}) ∈ ℕ₀^*)
112	93, 111	syl 17	. . . 4 ⊢ (𝜑 → (#‘{𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}}) ∈ ℕ₀^*)
113		hashxnn0 12989	. . . . 5 ⊢ ({𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}} ∈ V → (#‘{𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}) ∈ ℕ₀^*)
114	95, 113	syl 17	. . . 4 ⊢ (𝜑 → (#‘{𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}) ∈ ℕ₀^*)
115	108, 110, 112, 114	xnn0add4d 12006	. . 3 ⊢ (𝜑 → (((#‘{𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) +_𝑒 (#‘{𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)})) +_𝑒 ((#‘{𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}}) +_𝑒 (#‘{𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}))) = (((#‘{𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) +_𝑒 (#‘{𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}})) +_𝑒 ((#‘{𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) +_𝑒 (#‘{𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}))))
116	106, 115	eqtrd 2644	. 2 ⊢ (𝜑 → ((#‘{𝑥 ∈ dom (iEdg‘𝑈) ∣ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)}) +_𝑒 (#‘{𝑥 ∈ dom (iEdg‘𝑈) ∣ ((iEdg‘𝑈)‘𝑥) = {𝑁}})) = (((#‘{𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) +_𝑒 (#‘{𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}})) +_𝑒 ((#‘{𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) +_𝑒 (#‘{𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}))))
117		vtxdun.n	. . . 4 ⊢ (𝜑 → 𝑁 ∈ 𝑉)
118		vtxdun.vu	. . . 4 ⊢ (𝜑 → (Vtx‘𝑈) = 𝑉)
119	117, 118	eleqtrrd 2691	. . 3 ⊢ (𝜑 → 𝑁 ∈ (Vtx‘𝑈))
120		eqid 2610	. . . 4 ⊢ (Vtx‘𝑈) = (Vtx‘𝑈)
121		eqid 2610	. . . 4 ⊢ (iEdg‘𝑈) = (iEdg‘𝑈)
122		eqid 2610	. . . 4 ⊢ dom (iEdg‘𝑈) = dom (iEdg‘𝑈)
123	120, 121, 122	vtxdgval 40684	. . 3 ⊢ (𝑁 ∈ (Vtx‘𝑈) → ((VtxDeg‘𝑈)‘𝑁) = ((#‘{𝑥 ∈ dom (iEdg‘𝑈) ∣ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)}) +_𝑒 (#‘{𝑥 ∈ dom (iEdg‘𝑈) ∣ ((iEdg‘𝑈)‘𝑥) = {𝑁}})))
124	119, 123	syl 17	. 2 ⊢ (𝜑 → ((VtxDeg‘𝑈)‘𝑁) = ((#‘{𝑥 ∈ dom (iEdg‘𝑈) ∣ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)}) +_𝑒 (#‘{𝑥 ∈ dom (iEdg‘𝑈) ∣ ((iEdg‘𝑈)‘𝑥) = {𝑁}})))
125		vtxdun.vg	. . . . 5 ⊢ 𝑉 = (Vtx‘𝐺)
126		eqid 2610	. . . . 5 ⊢ dom 𝐼 = dom 𝐼
127	125, 50, 126	vtxdgval 40684	. . . 4 ⊢ (𝑁 ∈ 𝑉 → ((VtxDeg‘𝐺)‘𝑁) = ((#‘{𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) +_𝑒 (#‘{𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}})))
128	117, 127	syl 17	. . 3 ⊢ (𝜑 → ((VtxDeg‘𝐺)‘𝑁) = ((#‘{𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) +_𝑒 (#‘{𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}})))
129		vtxdun.vh	. . . . 5 ⊢ (𝜑 → (Vtx‘𝐻) = 𝑉)
130	117, 129	eleqtrrd 2691	. . . 4 ⊢ (𝜑 → 𝑁 ∈ (Vtx‘𝐻))
131		eqid 2610	. . . . 5 ⊢ (Vtx‘𝐻) = (Vtx‘𝐻)
132		eqid 2610	. . . . 5 ⊢ dom 𝐽 = dom 𝐽
133	131, 56, 132	vtxdgval 40684	. . . 4 ⊢ (𝑁 ∈ (Vtx‘𝐻) → ((VtxDeg‘𝐻)‘𝑁) = ((#‘{𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) +_𝑒 (#‘{𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}})))
134	130, 133	syl 17	. . 3 ⊢ (𝜑 → ((VtxDeg‘𝐻)‘𝑁) = ((#‘{𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) +_𝑒 (#‘{𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}})))
135	128, 134	oveq12d 6567	. 2 ⊢ (𝜑 → (((VtxDeg‘𝐺)‘𝑁) +_𝑒 ((VtxDeg‘𝐻)‘𝑁)) = (((#‘{𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) +_𝑒 (#‘{𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}})) +_𝑒 ((#‘{𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) +_𝑒 (#‘{𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}))))
136	116, 124, 135	3eqtr4d 2654	1 ⊢ (𝜑 → ((VtxDeg‘𝑈)‘𝑁) = (((VtxDeg‘𝐺)‘𝑁) +_𝑒 ((VtxDeg‘𝐻)‘𝑁)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∨ wo 382 ∧ wa 383 = wceq 1475 ∈ wcel 1977 {cab 2596 {crab 2900 Vcvv 3173 ∪ cun 3538 ∩ cin 3539 ⊆ wss 3540 ∅c0 3874 {csn 4125 dom cdm 5038 Fun wfun 5798 Fn wfn 5799 ‘cfv 5804 (class class class)co 6549 ℕ₀^*cxnn0 11240 +_𝑒 cxad 11820 #chash 12979 Vtxcvtx 25673 iEdgciedg 25674 VtxDegcvtxdg 40681

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-rep 4699 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-cnex 9871 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 ax-pre-mulgt0 9892

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rmo 2904 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-int 4411 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-om 6958 df-1st 7059 df-2nd 7060 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-1o 7447 df-oadd 7451 df-er 7629 df-en 7842 df-dom 7843 df-sdom 7844 df-fin 7845 df-card 8648 df-cda 8873 df-pnf 9955 df-mnf 9956 df-xr 9957 df-ltxr 9958 df-le 9959 df-sub 10147 df-neg 10148 df-nn 10898 df-n0 11170 df-xnn0 11241 df-z 11255 df-uz 11564 df-xadd 11823 df-hash 12980 df-vtxdg 40682

This theorem is referenced by: vtxdfiun 40697 vtxduhgrun 40698 p1evtxdeqlem 40728

W3C validator