Step | Hyp | Ref
| Expression |
1 | | df-rab 3063 |
. . . . . . . 8
⊢ {𝑥 ∈ dom (iEdg‘𝑈) ∣ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)} = {𝑥 ∣ (𝑥 ∈ dom (iEdg‘𝑈) ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))} |
2 | | vtxdun.u |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (iEdg‘𝑈) = (𝐼 ∪ 𝐽)) |
3 | 2 | dmeqd 5758 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → dom (iEdg‘𝑈) = dom (𝐼 ∪ 𝐽)) |
4 | | dmun 5763 |
. . . . . . . . . . . . . 14
⊢ dom
(𝐼 ∪ 𝐽) = (dom 𝐼 ∪ dom 𝐽) |
5 | 3, 4 | eqtrdi 2790 |
. . . . . . . . . . . . 13
⊢ (𝜑 → dom (iEdg‘𝑈) = (dom 𝐼 ∪ dom 𝐽)) |
6 | 5 | eleq2d 2819 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ dom (iEdg‘𝑈) ↔ 𝑥 ∈ (dom 𝐼 ∪ dom 𝐽))) |
7 | | elun 4049 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (dom 𝐼 ∪ dom 𝐽) ↔ (𝑥 ∈ dom 𝐼 ∨ 𝑥 ∈ dom 𝐽)) |
8 | 6, 7 | bitrdi 290 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ dom (iEdg‘𝑈) ↔ (𝑥 ∈ dom 𝐼 ∨ 𝑥 ∈ dom 𝐽))) |
9 | 8 | anbi1d 633 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑥 ∈ dom (iEdg‘𝑈) ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)) ↔ ((𝑥 ∈ dom 𝐼 ∨ 𝑥 ∈ dom 𝐽) ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)))) |
10 | | andir 1008 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ dom 𝐼 ∨ 𝑥 ∈ dom 𝐽) ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)) ↔ ((𝑥 ∈ dom 𝐼 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)) ∨ (𝑥 ∈ dom 𝐽 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)))) |
11 | 9, 10 | bitrdi 290 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑥 ∈ dom (iEdg‘𝑈) ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)) ↔ ((𝑥 ∈ dom 𝐼 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)) ∨ (𝑥 ∈ dom 𝐽 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))))) |
12 | 11 | abbidv 2803 |
. . . . . . . 8
⊢ (𝜑 → {𝑥 ∣ (𝑥 ∈ dom (iEdg‘𝑈) ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))} = {𝑥 ∣ ((𝑥 ∈ dom 𝐼 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)) ∨ (𝑥 ∈ dom 𝐽 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)))}) |
13 | 1, 12 | syl5eq 2786 |
. . . . . . 7
⊢ (𝜑 → {𝑥 ∈ dom (iEdg‘𝑈) ∣ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)} = {𝑥 ∣ ((𝑥 ∈ dom 𝐼 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)) ∨ (𝑥 ∈ dom 𝐽 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)))}) |
14 | | unab 4198 |
. . . . . . . . 9
⊢ ({𝑥 ∣ (𝑥 ∈ dom 𝐼 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))} ∪ {𝑥 ∣ (𝑥 ∈ dom 𝐽 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))}) = {𝑥 ∣ ((𝑥 ∈ dom 𝐼 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)) ∨ (𝑥 ∈ dom 𝐽 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)))} |
15 | 14 | eqcomi 2748 |
. . . . . . . 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 3063 |
. . . . . . . . 9
⊢ {𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)} = {𝑥 ∣ (𝑥 ∈ dom 𝐼 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))} |
18 | 2 | fveq1d 6688 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((iEdg‘𝑈)‘𝑥) = ((𝐼 ∪ 𝐽)‘𝑥)) |
19 | 18 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐼) → ((iEdg‘𝑈)‘𝑥) = ((𝐼 ∪ 𝐽)‘𝑥)) |
20 | | vtxdun.fi |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → Fun 𝐼) |
21 | 20 | funfnd 6380 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐼 Fn dom 𝐼) |
22 | 21 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐼) → 𝐼 Fn dom 𝐼) |
23 | | vtxdun.fj |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → Fun 𝐽) |
24 | 23 | funfnd 6380 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐽 Fn dom 𝐽) |
25 | 24 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐼) → 𝐽 Fn dom 𝐽) |
26 | | vtxdun.d |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (dom 𝐼 ∩ dom 𝐽) = ∅) |
27 | 26 | anim1i 618 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐼) → ((dom 𝐼 ∩ dom 𝐽) = ∅ ∧ 𝑥 ∈ dom 𝐼)) |
28 | | fvun1 6771 |
. . . . . . . . . . . . 13
⊢ ((𝐼 Fn dom 𝐼 ∧ 𝐽 Fn dom 𝐽 ∧ ((dom 𝐼 ∩ dom 𝐽) = ∅ ∧ 𝑥 ∈ dom 𝐼)) → ((𝐼 ∪ 𝐽)‘𝑥) = (𝐼‘𝑥)) |
29 | 22, 25, 27, 28 | syl3anc 1372 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐼) → ((𝐼 ∪ 𝐽)‘𝑥) = (𝐼‘𝑥)) |
30 | 19, 29 | eqtrd 2774 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐼) → ((iEdg‘𝑈)‘𝑥) = (𝐼‘𝑥)) |
31 | 30 | eleq2d 2819 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐼) → (𝑁 ∈ ((iEdg‘𝑈)‘𝑥) ↔ 𝑁 ∈ (𝐼‘𝑥))) |
32 | 31 | rabbidva 3380 |
. . . . . . . . 9
⊢ (𝜑 → {𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)} = {𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) |
33 | 17, 32 | eqtr3id 2788 |
. . . . . . . 8
⊢ (𝜑 → {𝑥 ∣ (𝑥 ∈ dom 𝐼 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))} = {𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) |
34 | | df-rab 3063 |
. . . . . . . . 9
⊢ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)} = {𝑥 ∣ (𝑥 ∈ dom 𝐽 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))} |
35 | 18 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐽) → ((iEdg‘𝑈)‘𝑥) = ((𝐼 ∪ 𝐽)‘𝑥)) |
36 | 21 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐽) → 𝐼 Fn dom 𝐼) |
37 | 24 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐽) → 𝐽 Fn dom 𝐽) |
38 | 26 | anim1i 618 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐽) → ((dom 𝐼 ∩ dom 𝐽) = ∅ ∧ 𝑥 ∈ dom 𝐽)) |
39 | | fvun2 6772 |
. . . . . . . . . . . . 13
⊢ ((𝐼 Fn dom 𝐼 ∧ 𝐽 Fn dom 𝐽 ∧ ((dom 𝐼 ∩ dom 𝐽) = ∅ ∧ 𝑥 ∈ dom 𝐽)) → ((𝐼 ∪ 𝐽)‘𝑥) = (𝐽‘𝑥)) |
40 | 36, 37, 38, 39 | syl3anc 1372 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐽) → ((𝐼 ∪ 𝐽)‘𝑥) = (𝐽‘𝑥)) |
41 | 35, 40 | eqtrd 2774 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐽) → ((iEdg‘𝑈)‘𝑥) = (𝐽‘𝑥)) |
42 | 41 | eleq2d 2819 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐽) → (𝑁 ∈ ((iEdg‘𝑈)‘𝑥) ↔ 𝑁 ∈ (𝐽‘𝑥))) |
43 | 42 | rabbidva 3380 |
. . . . . . . . 9
⊢ (𝜑 → {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)} = {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) |
44 | 34, 43 | eqtr3id 2788 |
. . . . . . . 8
⊢ (𝜑 → {𝑥 ∣ (𝑥 ∈ dom 𝐽 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))} = {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) |
45 | 33, 44 | uneq12d 4064 |
. . . . . . 7
⊢ (𝜑 → ({𝑥 ∣ (𝑥 ∈ dom 𝐼 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))} ∪ {𝑥 ∣ (𝑥 ∈ dom 𝐽 ∧ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥))}) = ({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∪ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)})) |
46 | 13, 16, 45 | 3eqtrd 2778 |
. . . . . 6
⊢ (𝜑 → {𝑥 ∈ dom (iEdg‘𝑈) ∣ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)} = ({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∪ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)})) |
47 | 46 | fveq2d 6690 |
. . . . 5
⊢ (𝜑 → (♯‘{𝑥 ∈ dom (iEdg‘𝑈) ∣ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)}) = (♯‘({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∪ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}))) |
48 | | vtxdun.i |
. . . . . . . . . 10
⊢ 𝐼 = (iEdg‘𝐺) |
49 | 48 | fvexi 6700 |
. . . . . . . . 9
⊢ 𝐼 ∈ V |
50 | 49 | dmex 7654 |
. . . . . . . 8
⊢ dom 𝐼 ∈ V |
51 | 50 | rabex 5210 |
. . . . . . 7
⊢ {𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∈ V |
52 | 51 | a1i 11 |
. . . . . 6
⊢ (𝜑 → {𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∈ V) |
53 | | vtxdun.j |
. . . . . . . . . 10
⊢ 𝐽 = (iEdg‘𝐻) |
54 | 53 | fvexi 6700 |
. . . . . . . . 9
⊢ 𝐽 ∈ V |
55 | 54 | dmex 7654 |
. . . . . . . 8
⊢ dom 𝐽 ∈ V |
56 | 55 | rabex 5210 |
. . . . . . 7
⊢ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)} ∈ V |
57 | 56 | a1i 11 |
. . . . . 6
⊢ (𝜑 → {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)} ∈ V) |
58 | | ssrab2 3979 |
. . . . . . . . 9
⊢ {𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ⊆ dom 𝐼 |
59 | | ssrab2 3979 |
. . . . . . . . 9
⊢ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)} ⊆ dom 𝐽 |
60 | | ss2in 4137 |
. . . . . . . . 9
⊢ (({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ⊆ dom 𝐼 ∧ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)} ⊆ dom 𝐽) → ({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∩ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) ⊆ (dom 𝐼 ∩ dom 𝐽)) |
61 | 58, 59, 60 | mp2an 692 |
. . . . . . . 8
⊢ ({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∩ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) ⊆ (dom 𝐼 ∩ dom 𝐽) |
62 | 61, 26 | sseqtrid 3939 |
. . . . . . 7
⊢ (𝜑 → ({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∩ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) ⊆ ∅) |
63 | | ss0 4297 |
. . . . . . 7
⊢ (({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∩ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) ⊆ ∅ → ({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∩ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) = ∅) |
64 | 62, 63 | syl 17 |
. . . . . 6
⊢ (𝜑 → ({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∩ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) = ∅) |
65 | | hashunx 13851 |
. . . . . 6
⊢ (({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∈ V ∧ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)} ∈ V ∧ ({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∩ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) = ∅) → (♯‘({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∪ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)})) = ((♯‘{𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) +𝑒
(♯‘{𝑥 ∈
dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}))) |
66 | 52, 57, 64, 65 | syl3anc 1372 |
. . . . 5
⊢ (𝜑 → (♯‘({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∪ {𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)})) = ((♯‘{𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) +𝑒
(♯‘{𝑥 ∈
dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}))) |
67 | 47, 66 | eqtrd 2774 |
. . . 4
⊢ (𝜑 → (♯‘{𝑥 ∈ dom (iEdg‘𝑈) ∣ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)}) = ((♯‘{𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) +𝑒
(♯‘{𝑥 ∈
dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}))) |
68 | | df-rab 3063 |
. . . . . . . 8
⊢ {𝑥 ∈ dom (iEdg‘𝑈) ∣ ((iEdg‘𝑈)‘𝑥) = {𝑁}} = {𝑥 ∣ (𝑥 ∈ dom (iEdg‘𝑈) ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})} |
69 | 8 | anbi1d 633 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑥 ∈ dom (iEdg‘𝑈) ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}) ↔ ((𝑥 ∈ dom 𝐼 ∨ 𝑥 ∈ dom 𝐽) ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}))) |
70 | | andir 1008 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ dom 𝐼 ∨ 𝑥 ∈ dom 𝐽) ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}) ↔ ((𝑥 ∈ dom 𝐼 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}) ∨ (𝑥 ∈ dom 𝐽 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}))) |
71 | 69, 70 | bitrdi 290 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑥 ∈ dom (iEdg‘𝑈) ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}) ↔ ((𝑥 ∈ dom 𝐼 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}) ∨ (𝑥 ∈ dom 𝐽 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})))) |
72 | 71 | abbidv 2803 |
. . . . . . . 8
⊢ (𝜑 → {𝑥 ∣ (𝑥 ∈ dom (iEdg‘𝑈) ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})} = {𝑥 ∣ ((𝑥 ∈ dom 𝐼 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}) ∨ (𝑥 ∈ dom 𝐽 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}))}) |
73 | 68, 72 | syl5eq 2786 |
. . . . . . 7
⊢ (𝜑 → {𝑥 ∈ dom (iEdg‘𝑈) ∣ ((iEdg‘𝑈)‘𝑥) = {𝑁}} = {𝑥 ∣ ((𝑥 ∈ dom 𝐼 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}) ∨ (𝑥 ∈ dom 𝐽 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}))}) |
74 | | unab 4198 |
. . . . . . . . 9
⊢ ({𝑥 ∣ (𝑥 ∈ dom 𝐼 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})} ∪ {𝑥 ∣ (𝑥 ∈ dom 𝐽 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})}) = {𝑥 ∣ ((𝑥 ∈ dom 𝐼 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}) ∨ (𝑥 ∈ dom 𝐽 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁}))} |
75 | 74 | eqcomi 2748 |
. . . . . . . 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 3063 |
. . . . . . . . 9
⊢ {𝑥 ∈ dom 𝐼 ∣ ((iEdg‘𝑈)‘𝑥) = {𝑁}} = {𝑥 ∣ (𝑥 ∈ dom 𝐼 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})} |
78 | 30 | eqeq1d 2741 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐼) → (((iEdg‘𝑈)‘𝑥) = {𝑁} ↔ (𝐼‘𝑥) = {𝑁})) |
79 | 78 | rabbidva 3380 |
. . . . . . . . 9
⊢ (𝜑 → {𝑥 ∈ dom 𝐼 ∣ ((iEdg‘𝑈)‘𝑥) = {𝑁}} = {𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}}) |
80 | 77, 79 | eqtr3id 2788 |
. . . . . . . 8
⊢ (𝜑 → {𝑥 ∣ (𝑥 ∈ dom 𝐼 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})} = {𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}}) |
81 | | df-rab 3063 |
. . . . . . . . 9
⊢ {𝑥 ∈ dom 𝐽 ∣ ((iEdg‘𝑈)‘𝑥) = {𝑁}} = {𝑥 ∣ (𝑥 ∈ dom 𝐽 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})} |
82 | 41 | eqeq1d 2741 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐽) → (((iEdg‘𝑈)‘𝑥) = {𝑁} ↔ (𝐽‘𝑥) = {𝑁})) |
83 | 82 | rabbidva 3380 |
. . . . . . . . 9
⊢ (𝜑 → {𝑥 ∈ dom 𝐽 ∣ ((iEdg‘𝑈)‘𝑥) = {𝑁}} = {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}) |
84 | 81, 83 | eqtr3id 2788 |
. . . . . . . 8
⊢ (𝜑 → {𝑥 ∣ (𝑥 ∈ dom 𝐽 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})} = {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}) |
85 | 80, 84 | uneq12d 4064 |
. . . . . . 7
⊢ (𝜑 → ({𝑥 ∣ (𝑥 ∈ dom 𝐼 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})} ∪ {𝑥 ∣ (𝑥 ∈ dom 𝐽 ∧ ((iEdg‘𝑈)‘𝑥) = {𝑁})}) = ({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∪ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}})) |
86 | 73, 76, 85 | 3eqtrd 2778 |
. . . . . 6
⊢ (𝜑 → {𝑥 ∈ dom (iEdg‘𝑈) ∣ ((iEdg‘𝑈)‘𝑥) = {𝑁}} = ({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∪ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}})) |
87 | 86 | fveq2d 6690 |
. . . . 5
⊢ (𝜑 → (♯‘{𝑥 ∈ dom (iEdg‘𝑈) ∣ ((iEdg‘𝑈)‘𝑥) = {𝑁}}) = (♯‘({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∪ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}))) |
88 | 50 | rabex 5210 |
. . . . . . 7
⊢ {𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∈ V |
89 | 88 | a1i 11 |
. . . . . 6
⊢ (𝜑 → {𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∈ V) |
90 | 55 | rabex 5210 |
. . . . . . 7
⊢ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}} ∈ V |
91 | 90 | a1i 11 |
. . . . . 6
⊢ (𝜑 → {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}} ∈ V) |
92 | | ssrab2 3979 |
. . . . . . . . 9
⊢ {𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ⊆ dom 𝐼 |
93 | | ssrab2 3979 |
. . . . . . . . 9
⊢ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}} ⊆ dom 𝐽 |
94 | | ss2in 4137 |
. . . . . . . . 9
⊢ (({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ⊆ dom 𝐼 ∧ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}} ⊆ dom 𝐽) → ({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∩ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}) ⊆ (dom 𝐼 ∩ dom 𝐽)) |
95 | 92, 93, 94 | mp2an 692 |
. . . . . . . 8
⊢ ({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∩ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}) ⊆ (dom 𝐼 ∩ dom 𝐽) |
96 | 95, 26 | sseqtrid 3939 |
. . . . . . 7
⊢ (𝜑 → ({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∩ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}) ⊆ ∅) |
97 | | ss0 4297 |
. . . . . . 7
⊢ (({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∩ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}) ⊆ ∅ → ({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∩ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}) = ∅) |
98 | 96, 97 | syl 17 |
. . . . . 6
⊢ (𝜑 → ({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∩ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}) = ∅) |
99 | | hashunx 13851 |
. . . . . 6
⊢ (({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∈ V ∧ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}} ∈ V ∧ ({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∩ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}) = ∅) → (♯‘({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∪ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}})) = ((♯‘{𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}}) +𝑒
(♯‘{𝑥 ∈
dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}))) |
100 | 89, 91, 98, 99 | syl3anc 1372 |
. . . . 5
⊢ (𝜑 → (♯‘({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∪ {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}})) = ((♯‘{𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}}) +𝑒
(♯‘{𝑥 ∈
dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}))) |
101 | 87, 100 | eqtrd 2774 |
. . . 4
⊢ (𝜑 → (♯‘{𝑥 ∈ dom (iEdg‘𝑈) ∣ ((iEdg‘𝑈)‘𝑥) = {𝑁}}) = ((♯‘{𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}}) +𝑒
(♯‘{𝑥 ∈
dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}))) |
102 | 67, 101 | oveq12d 7200 |
. . 3
⊢ (𝜑 → ((♯‘{𝑥 ∈ dom (iEdg‘𝑈) ∣ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)}) +𝑒
(♯‘{𝑥 ∈
dom (iEdg‘𝑈) ∣
((iEdg‘𝑈)‘𝑥) = {𝑁}})) = (((♯‘{𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) +𝑒
(♯‘{𝑥 ∈
dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)})) +𝑒
((♯‘{𝑥 ∈
dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}}) +𝑒
(♯‘{𝑥 ∈
dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}})))) |
103 | | hashxnn0 13803 |
. . . . 5
⊢ ({𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)} ∈ V → (♯‘{𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) ∈
ℕ0*) |
104 | 52, 103 | syl 17 |
. . . 4
⊢ (𝜑 → (♯‘{𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) ∈
ℕ0*) |
105 | | hashxnn0 13803 |
. . . . 5
⊢ ({𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)} ∈ V → (♯‘{𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) ∈
ℕ0*) |
106 | 57, 105 | syl 17 |
. . . 4
⊢ (𝜑 → (♯‘{𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) ∈
ℕ0*) |
107 | | hashxnn0 13803 |
. . . . 5
⊢ ({𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}} ∈ V → (♯‘{𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}}) ∈
ℕ0*) |
108 | 89, 107 | syl 17 |
. . . 4
⊢ (𝜑 → (♯‘{𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}}) ∈
ℕ0*) |
109 | | hashxnn0 13803 |
. . . . 5
⊢ ({𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}} ∈ V → (♯‘{𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}) ∈
ℕ0*) |
110 | 91, 109 | syl 17 |
. . . 4
⊢ (𝜑 → (♯‘{𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}) ∈
ℕ0*) |
111 | 104, 106,
108, 110 | xnn0add4d 12792 |
. . 3
⊢ (𝜑 → (((♯‘{𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) +𝑒
(♯‘{𝑥 ∈
dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)})) +𝑒
((♯‘{𝑥 ∈
dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}}) +𝑒
(♯‘{𝑥 ∈
dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}))) = (((♯‘{𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) +𝑒
(♯‘{𝑥 ∈
dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}})) +𝑒
((♯‘{𝑥 ∈
dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) +𝑒
(♯‘{𝑥 ∈
dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}})))) |
112 | 102, 111 | eqtrd 2774 |
. 2
⊢ (𝜑 → ((♯‘{𝑥 ∈ dom (iEdg‘𝑈) ∣ 𝑁 ∈ ((iEdg‘𝑈)‘𝑥)}) +𝑒
(♯‘{𝑥 ∈
dom (iEdg‘𝑈) ∣
((iEdg‘𝑈)‘𝑥) = {𝑁}})) = (((♯‘{𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) +𝑒
(♯‘{𝑥 ∈
dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}})) +𝑒
((♯‘{𝑥 ∈
dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) +𝑒
(♯‘{𝑥 ∈
dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}})))) |
113 | | vtxdun.n |
. . . 4
⊢ (𝜑 → 𝑁 ∈ 𝑉) |
114 | | vtxdun.vu |
. . . 4
⊢ (𝜑 → (Vtx‘𝑈) = 𝑉) |
115 | 113, 114 | eleqtrrd 2837 |
. . 3
⊢ (𝜑 → 𝑁 ∈ (Vtx‘𝑈)) |
116 | | eqid 2739 |
. . . 4
⊢
(Vtx‘𝑈) =
(Vtx‘𝑈) |
117 | | eqid 2739 |
. . . 4
⊢
(iEdg‘𝑈) =
(iEdg‘𝑈) |
118 | | eqid 2739 |
. . . 4
⊢ dom
(iEdg‘𝑈) = dom
(iEdg‘𝑈) |
119 | 116, 117,
118 | vtxdgval 27422 |
. . 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 2739 |
. . . . 5
⊢ dom 𝐼 = dom 𝐼 |
123 | 121, 48, 122 | vtxdgval 27422 |
. . . 4
⊢ (𝑁 ∈ 𝑉 → ((VtxDeg‘𝐺)‘𝑁) = ((♯‘{𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) +𝑒
(♯‘{𝑥 ∈
dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}}))) |
124 | 113, 123 | syl 17 |
. . 3
⊢ (𝜑 → ((VtxDeg‘𝐺)‘𝑁) = ((♯‘{𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) +𝑒
(♯‘{𝑥 ∈
dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}}))) |
125 | | vtxdun.vh |
. . . . 5
⊢ (𝜑 → (Vtx‘𝐻) = 𝑉) |
126 | 113, 125 | eleqtrrd 2837 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ (Vtx‘𝐻)) |
127 | | eqid 2739 |
. . . . 5
⊢
(Vtx‘𝐻) =
(Vtx‘𝐻) |
128 | | eqid 2739 |
. . . . 5
⊢ dom 𝐽 = dom 𝐽 |
129 | 127, 53, 128 | vtxdgval 27422 |
. . . 4
⊢ (𝑁 ∈ (Vtx‘𝐻) → ((VtxDeg‘𝐻)‘𝑁) = ((♯‘{𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) +𝑒
(♯‘{𝑥 ∈
dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}))) |
130 | 126, 129 | syl 17 |
. . 3
⊢ (𝜑 → ((VtxDeg‘𝐻)‘𝑁) = ((♯‘{𝑥 ∈ dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) +𝑒
(♯‘{𝑥 ∈
dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}}))) |
131 | 124, 130 | oveq12d 7200 |
. 2
⊢ (𝜑 → (((VtxDeg‘𝐺)‘𝑁) +𝑒 ((VtxDeg‘𝐻)‘𝑁)) = (((♯‘{𝑥 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑥)}) +𝑒
(♯‘{𝑥 ∈
dom 𝐼 ∣ (𝐼‘𝑥) = {𝑁}})) +𝑒
((♯‘{𝑥 ∈
dom 𝐽 ∣ 𝑁 ∈ (𝐽‘𝑥)}) +𝑒
(♯‘{𝑥 ∈
dom 𝐽 ∣ (𝐽‘𝑥) = {𝑁}})))) |
132 | 112, 120,
131 | 3eqtr4d 2784 |
1
⊢ (𝜑 → ((VtxDeg‘𝑈)‘𝑁) = (((VtxDeg‘𝐺)‘𝑁) +𝑒 ((VtxDeg‘𝐻)‘𝑁))) |