Step | Hyp | Ref
| Expression |
1 | | eupthvdres.g |
. 2
β’ (π β πΊ β π) |
2 | | eupthvdres.h |
. . . 4
β’ π» = β¨π, (πΌ βΎ (πΉ β (0..^(β―βπΉ))))β© |
3 | | opex 5422 |
. . . 4
β’
β¨π, (πΌ βΎ (πΉ β (0..^(β―βπΉ))))β© β
V |
4 | 2, 3 | eqeltri 2834 |
. . 3
β’ π» β V |
5 | 4 | a1i 11 |
. 2
β’ (π β π» β V) |
6 | 2 | fveq2i 6846 |
. . . 4
β’
(Vtxβπ») =
(Vtxββ¨π, (πΌ βΎ (πΉ β (0..^(β―βπΉ))))β©) |
7 | | eupthvdres.v |
. . . . . . . 8
β’ π = (VtxβπΊ) |
8 | 7 | fvexi 6857 |
. . . . . . 7
β’ π β V |
9 | | eupthvdres.i |
. . . . . . . . 9
β’ πΌ = (iEdgβπΊ) |
10 | 9 | fvexi 6857 |
. . . . . . . 8
β’ πΌ β V |
11 | 10 | resex 5986 |
. . . . . . 7
β’ (πΌ βΎ (πΉ β (0..^(β―βπΉ)))) β V |
12 | 8, 11 | pm3.2i 472 |
. . . . . 6
β’ (π β V β§ (πΌ βΎ (πΉ β (0..^(β―βπΉ)))) β V) |
13 | 12 | a1i 11 |
. . . . 5
β’ (π β (π β V β§ (πΌ βΎ (πΉ β (0..^(β―βπΉ)))) β V)) |
14 | | opvtxfv 27958 |
. . . . 5
β’ ((π β V β§ (πΌ βΎ (πΉ β (0..^(β―βπΉ)))) β V) β
(Vtxββ¨π, (πΌ βΎ (πΉ β (0..^(β―βπΉ))))β©) = π) |
15 | 13, 14 | syl 17 |
. . . 4
β’ (π β (Vtxββ¨π, (πΌ βΎ (πΉ β (0..^(β―βπΉ))))β©) = π) |
16 | 6, 15 | eqtrid 2789 |
. . 3
β’ (π β (Vtxβπ») = π) |
17 | 16, 7 | eqtrdi 2793 |
. 2
β’ (π β (Vtxβπ») = (VtxβπΊ)) |
18 | 2 | fveq2i 6846 |
. . . . 5
β’
(iEdgβπ») =
(iEdgββ¨π, (πΌ βΎ (πΉ β (0..^(β―βπΉ))))β©) |
19 | | opiedgfv 27961 |
. . . . . 6
β’ ((π β V β§ (πΌ βΎ (πΉ β (0..^(β―βπΉ)))) β V) β
(iEdgββ¨π, (πΌ βΎ (πΉ β (0..^(β―βπΉ))))β©) = (πΌ βΎ (πΉ β (0..^(β―βπΉ))))) |
20 | 13, 19 | syl 17 |
. . . . 5
β’ (π β (iEdgββ¨π, (πΌ βΎ (πΉ β (0..^(β―βπΉ))))β©) = (πΌ βΎ (πΉ β (0..^(β―βπΉ))))) |
21 | 18, 20 | eqtrid 2789 |
. . . 4
β’ (π β (iEdgβπ») = (πΌ βΎ (πΉ β (0..^(β―βπΉ))))) |
22 | | eupthvdres.p |
. . . . . . 7
β’ (π β πΉ(EulerPathsβπΊ)π) |
23 | 9 | eupthf1o 29151 |
. . . . . . 7
β’ (πΉ(EulerPathsβπΊ)π β πΉ:(0..^(β―βπΉ))β1-1-ontoβdom
πΌ) |
24 | 22, 23 | syl 17 |
. . . . . 6
β’ (π β πΉ:(0..^(β―βπΉ))β1-1-ontoβdom
πΌ) |
25 | | f1ofo 6792 |
. . . . . 6
β’ (πΉ:(0..^(β―βπΉ))β1-1-ontoβdom
πΌ β πΉ:(0..^(β―βπΉ))βontoβdom πΌ) |
26 | | foima 6762 |
. . . . . 6
β’ (πΉ:(0..^(β―βπΉ))βontoβdom πΌ β (πΉ β (0..^(β―βπΉ))) = dom πΌ) |
27 | 24, 25, 26 | 3syl 18 |
. . . . 5
β’ (π β (πΉ β (0..^(β―βπΉ))) = dom πΌ) |
28 | 27 | reseq2d 5938 |
. . . 4
β’ (π β (πΌ βΎ (πΉ β (0..^(β―βπΉ)))) = (πΌ βΎ dom πΌ)) |
29 | | eupthvdres.f |
. . . . . 6
β’ (π β Fun πΌ) |
30 | 29 | funfnd 6533 |
. . . . 5
β’ (π β πΌ Fn dom πΌ) |
31 | | fnresdm 6621 |
. . . . 5
β’ (πΌ Fn dom πΌ β (πΌ βΎ dom πΌ) = πΌ) |
32 | 30, 31 | syl 17 |
. . . 4
β’ (π β (πΌ βΎ dom πΌ) = πΌ) |
33 | 21, 28, 32 | 3eqtrd 2781 |
. . 3
β’ (π β (iEdgβπ») = πΌ) |
34 | 33, 9 | eqtrdi 2793 |
. 2
β’ (π β (iEdgβπ») = (iEdgβπΊ)) |
35 | 1, 5, 17, 34 | vtxdeqd 28428 |
1
β’ (π β (VtxDegβπ») = (VtxDegβπΊ)) |