Step |
Hyp |
Ref |
Expression |
1 |
|
vtxdun.i |
|- I = ( iEdg ` G ) |
2 |
|
vtxdun.j |
|- J = ( iEdg ` H ) |
3 |
|
vtxdun.vg |
|- V = ( Vtx ` G ) |
4 |
|
vtxdun.vh |
|- ( ph -> ( Vtx ` H ) = V ) |
5 |
|
vtxdun.vu |
|- ( ph -> ( Vtx ` U ) = V ) |
6 |
|
vtxdun.d |
|- ( ph -> ( dom I i^i dom J ) = (/) ) |
7 |
|
vtxdun.fi |
|- ( ph -> Fun I ) |
8 |
|
vtxdun.fj |
|- ( ph -> Fun J ) |
9 |
|
vtxdun.n |
|- ( ph -> N e. V ) |
10 |
|
vtxdun.u |
|- ( ph -> ( iEdg ` U ) = ( I u. J ) ) |
11 |
|
df-rab |
|- { x e. dom ( iEdg ` U ) | N e. ( ( iEdg ` U ) ` x ) } = { x | ( x e. dom ( iEdg ` U ) /\ N e. ( ( iEdg ` U ) ` x ) ) } |
12 |
10
|
dmeqd |
|- ( ph -> dom ( iEdg ` U ) = dom ( I u. J ) ) |
13 |
|
dmun |
|- dom ( I u. J ) = ( dom I u. dom J ) |
14 |
12 13
|
eqtrdi |
|- ( ph -> dom ( iEdg ` U ) = ( dom I u. dom J ) ) |
15 |
14
|
eleq2d |
|- ( ph -> ( x e. dom ( iEdg ` U ) <-> x e. ( dom I u. dom J ) ) ) |
16 |
|
elun |
|- ( x e. ( dom I u. dom J ) <-> ( x e. dom I \/ x e. dom J ) ) |
17 |
15 16
|
bitrdi |
|- ( ph -> ( x e. dom ( iEdg ` U ) <-> ( x e. dom I \/ x e. dom J ) ) ) |
18 |
17
|
anbi1d |
|- ( ph -> ( ( x e. dom ( iEdg ` U ) /\ N e. ( ( iEdg ` U ) ` x ) ) <-> ( ( x e. dom I \/ x e. dom J ) /\ N e. ( ( iEdg ` U ) ` x ) ) ) ) |
19 |
|
andir |
|- ( ( ( x e. dom I \/ x e. dom J ) /\ N e. ( ( iEdg ` U ) ` x ) ) <-> ( ( x e. dom I /\ N e. ( ( iEdg ` U ) ` x ) ) \/ ( x e. dom J /\ N e. ( ( iEdg ` U ) ` x ) ) ) ) |
20 |
18 19
|
bitrdi |
|- ( ph -> ( ( x e. dom ( iEdg ` U ) /\ N e. ( ( iEdg ` U ) ` x ) ) <-> ( ( x e. dom I /\ N e. ( ( iEdg ` U ) ` x ) ) \/ ( x e. dom J /\ N e. ( ( iEdg ` U ) ` x ) ) ) ) ) |
21 |
20
|
abbidv |
|- ( ph -> { x | ( x e. dom ( iEdg ` U ) /\ N e. ( ( iEdg ` U ) ` x ) ) } = { x | ( ( x e. dom I /\ N e. ( ( iEdg ` U ) ` x ) ) \/ ( x e. dom J /\ N e. ( ( iEdg ` U ) ` x ) ) ) } ) |
22 |
11 21
|
syl5eq |
|- ( ph -> { x e. dom ( iEdg ` U ) | N e. ( ( iEdg ` U ) ` x ) } = { x | ( ( x e. dom I /\ N e. ( ( iEdg ` U ) ` x ) ) \/ ( x e. dom J /\ N e. ( ( iEdg ` U ) ` x ) ) ) } ) |
23 |
|
unab |
|- ( { x | ( x e. dom I /\ N e. ( ( iEdg ` U ) ` x ) ) } u. { x | ( x e. dom J /\ N e. ( ( iEdg ` U ) ` x ) ) } ) = { x | ( ( x e. dom I /\ N e. ( ( iEdg ` U ) ` x ) ) \/ ( x e. dom J /\ N e. ( ( iEdg ` U ) ` x ) ) ) } |
24 |
23
|
eqcomi |
|- { x | ( ( x e. dom I /\ N e. ( ( iEdg ` U ) ` x ) ) \/ ( x e. dom J /\ N e. ( ( iEdg ` U ) ` x ) ) ) } = ( { x | ( x e. dom I /\ N e. ( ( iEdg ` U ) ` x ) ) } u. { x | ( x e. dom J /\ N e. ( ( iEdg ` U ) ` x ) ) } ) |
25 |
24
|
a1i |
|- ( ph -> { x | ( ( x e. dom I /\ N e. ( ( iEdg ` U ) ` x ) ) \/ ( x e. dom J /\ N e. ( ( iEdg ` U ) ` x ) ) ) } = ( { x | ( x e. dom I /\ N e. ( ( iEdg ` U ) ` x ) ) } u. { x | ( x e. dom J /\ N e. ( ( iEdg ` U ) ` x ) ) } ) ) |
26 |
|
df-rab |
|- { x e. dom I | N e. ( ( iEdg ` U ) ` x ) } = { x | ( x e. dom I /\ N e. ( ( iEdg ` U ) ` x ) ) } |
27 |
10
|
fveq1d |
|- ( ph -> ( ( iEdg ` U ) ` x ) = ( ( I u. J ) ` x ) ) |
28 |
27
|
adantr |
|- ( ( ph /\ x e. dom I ) -> ( ( iEdg ` U ) ` x ) = ( ( I u. J ) ` x ) ) |
29 |
7
|
funfnd |
|- ( ph -> I Fn dom I ) |
30 |
29
|
adantr |
|- ( ( ph /\ x e. dom I ) -> I Fn dom I ) |
31 |
8
|
funfnd |
|- ( ph -> J Fn dom J ) |
32 |
31
|
adantr |
|- ( ( ph /\ x e. dom I ) -> J Fn dom J ) |
33 |
6
|
anim1i |
|- ( ( ph /\ x e. dom I ) -> ( ( dom I i^i dom J ) = (/) /\ x e. dom I ) ) |
34 |
|
fvun1 |
|- ( ( I Fn dom I /\ J Fn dom J /\ ( ( dom I i^i dom J ) = (/) /\ x e. dom I ) ) -> ( ( I u. J ) ` x ) = ( I ` x ) ) |
35 |
30 32 33 34
|
syl3anc |
|- ( ( ph /\ x e. dom I ) -> ( ( I u. J ) ` x ) = ( I ` x ) ) |
36 |
28 35
|
eqtrd |
|- ( ( ph /\ x e. dom I ) -> ( ( iEdg ` U ) ` x ) = ( I ` x ) ) |
37 |
36
|
eleq2d |
|- ( ( ph /\ x e. dom I ) -> ( N e. ( ( iEdg ` U ) ` x ) <-> N e. ( I ` x ) ) ) |
38 |
37
|
rabbidva |
|- ( ph -> { x e. dom I | N e. ( ( iEdg ` U ) ` x ) } = { x e. dom I | N e. ( I ` x ) } ) |
39 |
26 38
|
eqtr3id |
|- ( ph -> { x | ( x e. dom I /\ N e. ( ( iEdg ` U ) ` x ) ) } = { x e. dom I | N e. ( I ` x ) } ) |
40 |
|
df-rab |
|- { x e. dom J | N e. ( ( iEdg ` U ) ` x ) } = { x | ( x e. dom J /\ N e. ( ( iEdg ` U ) ` x ) ) } |
41 |
27
|
adantr |
|- ( ( ph /\ x e. dom J ) -> ( ( iEdg ` U ) ` x ) = ( ( I u. J ) ` x ) ) |
42 |
29
|
adantr |
|- ( ( ph /\ x e. dom J ) -> I Fn dom I ) |
43 |
31
|
adantr |
|- ( ( ph /\ x e. dom J ) -> J Fn dom J ) |
44 |
6
|
anim1i |
|- ( ( ph /\ x e. dom J ) -> ( ( dom I i^i dom J ) = (/) /\ x e. dom J ) ) |
45 |
|
fvun2 |
|- ( ( I Fn dom I /\ J Fn dom J /\ ( ( dom I i^i dom J ) = (/) /\ x e. dom J ) ) -> ( ( I u. J ) ` x ) = ( J ` x ) ) |
46 |
42 43 44 45
|
syl3anc |
|- ( ( ph /\ x e. dom J ) -> ( ( I u. J ) ` x ) = ( J ` x ) ) |
47 |
41 46
|
eqtrd |
|- ( ( ph /\ x e. dom J ) -> ( ( iEdg ` U ) ` x ) = ( J ` x ) ) |
48 |
47
|
eleq2d |
|- ( ( ph /\ x e. dom J ) -> ( N e. ( ( iEdg ` U ) ` x ) <-> N e. ( J ` x ) ) ) |
49 |
48
|
rabbidva |
|- ( ph -> { x e. dom J | N e. ( ( iEdg ` U ) ` x ) } = { x e. dom J | N e. ( J ` x ) } ) |
50 |
40 49
|
eqtr3id |
|- ( ph -> { x | ( x e. dom J /\ N e. ( ( iEdg ` U ) ` x ) ) } = { x e. dom J | N e. ( J ` x ) } ) |
51 |
39 50
|
uneq12d |
|- ( ph -> ( { x | ( x e. dom I /\ N e. ( ( iEdg ` U ) ` x ) ) } u. { x | ( x e. dom J /\ N e. ( ( iEdg ` U ) ` x ) ) } ) = ( { x e. dom I | N e. ( I ` x ) } u. { x e. dom J | N e. ( J ` x ) } ) ) |
52 |
22 25 51
|
3eqtrd |
|- ( ph -> { x e. dom ( iEdg ` U ) | N e. ( ( iEdg ` U ) ` x ) } = ( { x e. dom I | N e. ( I ` x ) } u. { x e. dom J | N e. ( J ` x ) } ) ) |
53 |
52
|
fveq2d |
|- ( ph -> ( # ` { x e. dom ( iEdg ` U ) | N e. ( ( iEdg ` U ) ` x ) } ) = ( # ` ( { x e. dom I | N e. ( I ` x ) } u. { x e. dom J | N e. ( J ` x ) } ) ) ) |
54 |
1
|
fvexi |
|- I e. _V |
55 |
54
|
dmex |
|- dom I e. _V |
56 |
55
|
rabex |
|- { x e. dom I | N e. ( I ` x ) } e. _V |
57 |
56
|
a1i |
|- ( ph -> { x e. dom I | N e. ( I ` x ) } e. _V ) |
58 |
2
|
fvexi |
|- J e. _V |
59 |
58
|
dmex |
|- dom J e. _V |
60 |
59
|
rabex |
|- { x e. dom J | N e. ( J ` x ) } e. _V |
61 |
60
|
a1i |
|- ( ph -> { x e. dom J | N e. ( J ` x ) } e. _V ) |
62 |
|
ssrab2 |
|- { x e. dom I | N e. ( I ` x ) } C_ dom I |
63 |
|
ssrab2 |
|- { x e. dom J | N e. ( J ` x ) } C_ dom J |
64 |
|
ss2in |
|- ( ( { x e. dom I | N e. ( I ` x ) } C_ dom I /\ { x e. dom J | N e. ( J ` x ) } C_ dom J ) -> ( { x e. dom I | N e. ( I ` x ) } i^i { x e. dom J | N e. ( J ` x ) } ) C_ ( dom I i^i dom J ) ) |
65 |
62 63 64
|
mp2an |
|- ( { x e. dom I | N e. ( I ` x ) } i^i { x e. dom J | N e. ( J ` x ) } ) C_ ( dom I i^i dom J ) |
66 |
65 6
|
sseqtrid |
|- ( ph -> ( { x e. dom I | N e. ( I ` x ) } i^i { x e. dom J | N e. ( J ` x ) } ) C_ (/) ) |
67 |
|
ss0 |
|- ( ( { x e. dom I | N e. ( I ` x ) } i^i { x e. dom J | N e. ( J ` x ) } ) C_ (/) -> ( { x e. dom I | N e. ( I ` x ) } i^i { x e. dom J | N e. ( J ` x ) } ) = (/) ) |
68 |
66 67
|
syl |
|- ( ph -> ( { x e. dom I | N e. ( I ` x ) } i^i { x e. dom J | N e. ( J ` x ) } ) = (/) ) |
69 |
|
hashunx |
|- ( ( { x e. dom I | N e. ( I ` x ) } e. _V /\ { x e. dom J | N e. ( J ` x ) } e. _V /\ ( { x e. dom I | N e. ( I ` x ) } i^i { x e. dom J | N e. ( J ` x ) } ) = (/) ) -> ( # ` ( { x e. dom I | N e. ( I ` x ) } u. { x e. dom J | N e. ( J ` x ) } ) ) = ( ( # ` { x e. dom I | N e. ( I ` x ) } ) +e ( # ` { x e. dom J | N e. ( J ` x ) } ) ) ) |
70 |
57 61 68 69
|
syl3anc |
|- ( ph -> ( # ` ( { x e. dom I | N e. ( I ` x ) } u. { x e. dom J | N e. ( J ` x ) } ) ) = ( ( # ` { x e. dom I | N e. ( I ` x ) } ) +e ( # ` { x e. dom J | N e. ( J ` x ) } ) ) ) |
71 |
53 70
|
eqtrd |
|- ( ph -> ( # ` { x e. dom ( iEdg ` U ) | N e. ( ( iEdg ` U ) ` x ) } ) = ( ( # ` { x e. dom I | N e. ( I ` x ) } ) +e ( # ` { x e. dom J | N e. ( J ` x ) } ) ) ) |
72 |
|
df-rab |
|- { x e. dom ( iEdg ` U ) | ( ( iEdg ` U ) ` x ) = { N } } = { x | ( x e. dom ( iEdg ` U ) /\ ( ( iEdg ` U ) ` x ) = { N } ) } |
73 |
17
|
anbi1d |
|- ( ph -> ( ( x e. dom ( iEdg ` U ) /\ ( ( iEdg ` U ) ` x ) = { N } ) <-> ( ( x e. dom I \/ x e. dom J ) /\ ( ( iEdg ` U ) ` x ) = { N } ) ) ) |
74 |
|
andir |
|- ( ( ( x e. dom I \/ x e. dom J ) /\ ( ( iEdg ` U ) ` x ) = { N } ) <-> ( ( x e. dom I /\ ( ( iEdg ` U ) ` x ) = { N } ) \/ ( x e. dom J /\ ( ( iEdg ` U ) ` x ) = { N } ) ) ) |
75 |
73 74
|
bitrdi |
|- ( ph -> ( ( x e. dom ( iEdg ` U ) /\ ( ( iEdg ` U ) ` x ) = { N } ) <-> ( ( x e. dom I /\ ( ( iEdg ` U ) ` x ) = { N } ) \/ ( x e. dom J /\ ( ( iEdg ` U ) ` x ) = { N } ) ) ) ) |
76 |
75
|
abbidv |
|- ( ph -> { x | ( x e. dom ( iEdg ` U ) /\ ( ( iEdg ` U ) ` x ) = { N } ) } = { x | ( ( x e. dom I /\ ( ( iEdg ` U ) ` x ) = { N } ) \/ ( x e. dom J /\ ( ( iEdg ` U ) ` x ) = { N } ) ) } ) |
77 |
72 76
|
syl5eq |
|- ( ph -> { x e. dom ( iEdg ` U ) | ( ( iEdg ` U ) ` x ) = { N } } = { x | ( ( x e. dom I /\ ( ( iEdg ` U ) ` x ) = { N } ) \/ ( x e. dom J /\ ( ( iEdg ` U ) ` x ) = { N } ) ) } ) |
78 |
|
unab |
|- ( { x | ( x e. dom I /\ ( ( iEdg ` U ) ` x ) = { N } ) } u. { x | ( x e. dom J /\ ( ( iEdg ` U ) ` x ) = { N } ) } ) = { x | ( ( x e. dom I /\ ( ( iEdg ` U ) ` x ) = { N } ) \/ ( x e. dom J /\ ( ( iEdg ` U ) ` x ) = { N } ) ) } |
79 |
78
|
eqcomi |
|- { x | ( ( x e. dom I /\ ( ( iEdg ` U ) ` x ) = { N } ) \/ ( x e. dom J /\ ( ( iEdg ` U ) ` x ) = { N } ) ) } = ( { x | ( x e. dom I /\ ( ( iEdg ` U ) ` x ) = { N } ) } u. { x | ( x e. dom J /\ ( ( iEdg ` U ) ` x ) = { N } ) } ) |
80 |
79
|
a1i |
|- ( ph -> { x | ( ( x e. dom I /\ ( ( iEdg ` U ) ` x ) = { N } ) \/ ( x e. dom J /\ ( ( iEdg ` U ) ` x ) = { N } ) ) } = ( { x | ( x e. dom I /\ ( ( iEdg ` U ) ` x ) = { N } ) } u. { x | ( x e. dom J /\ ( ( iEdg ` U ) ` x ) = { N } ) } ) ) |
81 |
|
df-rab |
|- { x e. dom I | ( ( iEdg ` U ) ` x ) = { N } } = { x | ( x e. dom I /\ ( ( iEdg ` U ) ` x ) = { N } ) } |
82 |
36
|
eqeq1d |
|- ( ( ph /\ x e. dom I ) -> ( ( ( iEdg ` U ) ` x ) = { N } <-> ( I ` x ) = { N } ) ) |
83 |
82
|
rabbidva |
|- ( ph -> { x e. dom I | ( ( iEdg ` U ) ` x ) = { N } } = { x e. dom I | ( I ` x ) = { N } } ) |
84 |
81 83
|
eqtr3id |
|- ( ph -> { x | ( x e. dom I /\ ( ( iEdg ` U ) ` x ) = { N } ) } = { x e. dom I | ( I ` x ) = { N } } ) |
85 |
|
df-rab |
|- { x e. dom J | ( ( iEdg ` U ) ` x ) = { N } } = { x | ( x e. dom J /\ ( ( iEdg ` U ) ` x ) = { N } ) } |
86 |
47
|
eqeq1d |
|- ( ( ph /\ x e. dom J ) -> ( ( ( iEdg ` U ) ` x ) = { N } <-> ( J ` x ) = { N } ) ) |
87 |
86
|
rabbidva |
|- ( ph -> { x e. dom J | ( ( iEdg ` U ) ` x ) = { N } } = { x e. dom J | ( J ` x ) = { N } } ) |
88 |
85 87
|
eqtr3id |
|- ( ph -> { x | ( x e. dom J /\ ( ( iEdg ` U ) ` x ) = { N } ) } = { x e. dom J | ( J ` x ) = { N } } ) |
89 |
84 88
|
uneq12d |
|- ( ph -> ( { x | ( x e. dom I /\ ( ( iEdg ` U ) ` x ) = { N } ) } u. { x | ( x e. dom J /\ ( ( iEdg ` U ) ` x ) = { N } ) } ) = ( { x e. dom I | ( I ` x ) = { N } } u. { x e. dom J | ( J ` x ) = { N } } ) ) |
90 |
77 80 89
|
3eqtrd |
|- ( ph -> { x e. dom ( iEdg ` U ) | ( ( iEdg ` U ) ` x ) = { N } } = ( { x e. dom I | ( I ` x ) = { N } } u. { x e. dom J | ( J ` x ) = { N } } ) ) |
91 |
90
|
fveq2d |
|- ( ph -> ( # ` { x e. dom ( iEdg ` U ) | ( ( iEdg ` U ) ` x ) = { N } } ) = ( # ` ( { x e. dom I | ( I ` x ) = { N } } u. { x e. dom J | ( J ` x ) = { N } } ) ) ) |
92 |
55
|
rabex |
|- { x e. dom I | ( I ` x ) = { N } } e. _V |
93 |
92
|
a1i |
|- ( ph -> { x e. dom I | ( I ` x ) = { N } } e. _V ) |
94 |
59
|
rabex |
|- { x e. dom J | ( J ` x ) = { N } } e. _V |
95 |
94
|
a1i |
|- ( ph -> { x e. dom J | ( J ` x ) = { N } } e. _V ) |
96 |
|
ssrab2 |
|- { x e. dom I | ( I ` x ) = { N } } C_ dom I |
97 |
|
ssrab2 |
|- { x e. dom J | ( J ` x ) = { N } } C_ dom J |
98 |
|
ss2in |
|- ( ( { x e. dom I | ( I ` x ) = { N } } C_ dom I /\ { x e. dom J | ( J ` x ) = { N } } C_ dom J ) -> ( { x e. dom I | ( I ` x ) = { N } } i^i { x e. dom J | ( J ` x ) = { N } } ) C_ ( dom I i^i dom J ) ) |
99 |
96 97 98
|
mp2an |
|- ( { x e. dom I | ( I ` x ) = { N } } i^i { x e. dom J | ( J ` x ) = { N } } ) C_ ( dom I i^i dom J ) |
100 |
99 6
|
sseqtrid |
|- ( ph -> ( { x e. dom I | ( I ` x ) = { N } } i^i { x e. dom J | ( J ` x ) = { N } } ) C_ (/) ) |
101 |
|
ss0 |
|- ( ( { x e. dom I | ( I ` x ) = { N } } i^i { x e. dom J | ( J ` x ) = { N } } ) C_ (/) -> ( { x e. dom I | ( I ` x ) = { N } } i^i { x e. dom J | ( J ` x ) = { N } } ) = (/) ) |
102 |
100 101
|
syl |
|- ( ph -> ( { x e. dom I | ( I ` x ) = { N } } i^i { x e. dom J | ( J ` x ) = { N } } ) = (/) ) |
103 |
|
hashunx |
|- ( ( { x e. dom I | ( I ` x ) = { N } } e. _V /\ { x e. dom J | ( J ` x ) = { N } } e. _V /\ ( { x e. dom I | ( I ` x ) = { N } } i^i { x e. dom J | ( J ` x ) = { N } } ) = (/) ) -> ( # ` ( { x e. dom I | ( I ` x ) = { N } } u. { x e. dom J | ( J ` x ) = { N } } ) ) = ( ( # ` { x e. dom I | ( I ` x ) = { N } } ) +e ( # ` { x e. dom J | ( J ` x ) = { N } } ) ) ) |
104 |
93 95 102 103
|
syl3anc |
|- ( ph -> ( # ` ( { x e. dom I | ( I ` x ) = { N } } u. { x e. dom J | ( J ` x ) = { N } } ) ) = ( ( # ` { x e. dom I | ( I ` x ) = { N } } ) +e ( # ` { x e. dom J | ( J ` x ) = { N } } ) ) ) |
105 |
91 104
|
eqtrd |
|- ( ph -> ( # ` { x e. dom ( iEdg ` U ) | ( ( iEdg ` U ) ` x ) = { N } } ) = ( ( # ` { x e. dom I | ( I ` x ) = { N } } ) +e ( # ` { x e. dom J | ( J ` x ) = { N } } ) ) ) |
106 |
71 105
|
oveq12d |
|- ( ph -> ( ( # ` { x e. dom ( iEdg ` U ) | N e. ( ( iEdg ` U ) ` x ) } ) +e ( # ` { x e. dom ( iEdg ` U ) | ( ( iEdg ` U ) ` x ) = { N } } ) ) = ( ( ( # ` { x e. dom I | N e. ( I ` x ) } ) +e ( # ` { x e. dom J | N e. ( J ` x ) } ) ) +e ( ( # ` { x e. dom I | ( I ` x ) = { N } } ) +e ( # ` { x e. dom J | ( J ` x ) = { N } } ) ) ) ) |
107 |
|
hashxnn0 |
|- ( { x e. dom I | N e. ( I ` x ) } e. _V -> ( # ` { x e. dom I | N e. ( I ` x ) } ) e. NN0* ) |
108 |
57 107
|
syl |
|- ( ph -> ( # ` { x e. dom I | N e. ( I ` x ) } ) e. NN0* ) |
109 |
|
hashxnn0 |
|- ( { x e. dom J | N e. ( J ` x ) } e. _V -> ( # ` { x e. dom J | N e. ( J ` x ) } ) e. NN0* ) |
110 |
61 109
|
syl |
|- ( ph -> ( # ` { x e. dom J | N e. ( J ` x ) } ) e. NN0* ) |
111 |
|
hashxnn0 |
|- ( { x e. dom I | ( I ` x ) = { N } } e. _V -> ( # ` { x e. dom I | ( I ` x ) = { N } } ) e. NN0* ) |
112 |
93 111
|
syl |
|- ( ph -> ( # ` { x e. dom I | ( I ` x ) = { N } } ) e. NN0* ) |
113 |
|
hashxnn0 |
|- ( { x e. dom J | ( J ` x ) = { N } } e. _V -> ( # ` { x e. dom J | ( J ` x ) = { N } } ) e. NN0* ) |
114 |
95 113
|
syl |
|- ( ph -> ( # ` { x e. dom J | ( J ` x ) = { N } } ) e. NN0* ) |
115 |
108 110 112 114
|
xnn0add4d |
|- ( ph -> ( ( ( # ` { x e. dom I | N e. ( I ` x ) } ) +e ( # ` { x e. dom J | N e. ( J ` x ) } ) ) +e ( ( # ` { x e. dom I | ( I ` x ) = { N } } ) +e ( # ` { x e. dom J | ( J ` x ) = { N } } ) ) ) = ( ( ( # ` { x e. dom I | N e. ( I ` x ) } ) +e ( # ` { x e. dom I | ( I ` x ) = { N } } ) ) +e ( ( # ` { x e. dom J | N e. ( J ` x ) } ) +e ( # ` { x e. dom J | ( J ` x ) = { N } } ) ) ) ) |
116 |
106 115
|
eqtrd |
|- ( ph -> ( ( # ` { x e. dom ( iEdg ` U ) | N e. ( ( iEdg ` U ) ` x ) } ) +e ( # ` { x e. dom ( iEdg ` U ) | ( ( iEdg ` U ) ` x ) = { N } } ) ) = ( ( ( # ` { x e. dom I | N e. ( I ` x ) } ) +e ( # ` { x e. dom I | ( I ` x ) = { N } } ) ) +e ( ( # ` { x e. dom J | N e. ( J ` x ) } ) +e ( # ` { x e. dom J | ( J ` x ) = { N } } ) ) ) ) |
117 |
9 5
|
eleqtrrd |
|- ( ph -> N e. ( Vtx ` U ) ) |
118 |
|
eqid |
|- ( Vtx ` U ) = ( Vtx ` U ) |
119 |
|
eqid |
|- ( iEdg ` U ) = ( iEdg ` U ) |
120 |
|
eqid |
|- dom ( iEdg ` U ) = dom ( iEdg ` U ) |
121 |
118 119 120
|
vtxdgval |
|- ( N e. ( Vtx ` U ) -> ( ( VtxDeg ` U ) ` N ) = ( ( # ` { x e. dom ( iEdg ` U ) | N e. ( ( iEdg ` U ) ` x ) } ) +e ( # ` { x e. dom ( iEdg ` U ) | ( ( iEdg ` U ) ` x ) = { N } } ) ) ) |
122 |
117 121
|
syl |
|- ( ph -> ( ( VtxDeg ` U ) ` N ) = ( ( # ` { x e. dom ( iEdg ` U ) | N e. ( ( iEdg ` U ) ` x ) } ) +e ( # ` { x e. dom ( iEdg ` U ) | ( ( iEdg ` U ) ` x ) = { N } } ) ) ) |
123 |
|
eqid |
|- dom I = dom I |
124 |
3 1 123
|
vtxdgval |
|- ( N e. V -> ( ( VtxDeg ` G ) ` N ) = ( ( # ` { x e. dom I | N e. ( I ` x ) } ) +e ( # ` { x e. dom I | ( I ` x ) = { N } } ) ) ) |
125 |
9 124
|
syl |
|- ( ph -> ( ( VtxDeg ` G ) ` N ) = ( ( # ` { x e. dom I | N e. ( I ` x ) } ) +e ( # ` { x e. dom I | ( I ` x ) = { N } } ) ) ) |
126 |
9 4
|
eleqtrrd |
|- ( ph -> N e. ( Vtx ` H ) ) |
127 |
|
eqid |
|- ( Vtx ` H ) = ( Vtx ` H ) |
128 |
|
eqid |
|- dom J = dom J |
129 |
127 2 128
|
vtxdgval |
|- ( N e. ( Vtx ` H ) -> ( ( VtxDeg ` H ) ` N ) = ( ( # ` { x e. dom J | N e. ( J ` x ) } ) +e ( # ` { x e. dom J | ( J ` x ) = { N } } ) ) ) |
130 |
126 129
|
syl |
|- ( ph -> ( ( VtxDeg ` H ) ` N ) = ( ( # ` { x e. dom J | N e. ( J ` x ) } ) +e ( # ` { x e. dom J | ( J ` x ) = { N } } ) ) ) |
131 |
125 130
|
oveq12d |
|- ( ph -> ( ( ( VtxDeg ` G ) ` N ) +e ( ( VtxDeg ` H ) ` N ) ) = ( ( ( # ` { x e. dom I | N e. ( I ` x ) } ) +e ( # ` { x e. dom I | ( I ` x ) = { N } } ) ) +e ( ( # ` { x e. dom J | N e. ( J ` x ) } ) +e ( # ` { x e. dom J | ( J ` x ) = { N } } ) ) ) ) |
132 |
116 122 131
|
3eqtr4d |
|- ( ph -> ( ( VtxDeg ` U ) ` N ) = ( ( ( VtxDeg ` G ) ` N ) +e ( ( VtxDeg ` H ) ` N ) ) ) |