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