Metamath Proof Explorer


Theorem vtxdun

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)

Ref Expression
Hypotheses 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 vtxdun ( šœ‘ ā†’ ( ( VtxDeg ā€˜ š‘ˆ ) ā€˜ š‘ ) = ( ( ( VtxDeg ā€˜ šŗ ) ā€˜ š‘ ) +š‘’ ( ( VtxDeg ā€˜ š» ) ā€˜ š‘ ) ) )

Proof

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 ā€˜ š» ) ā€˜ š‘ ) ) )