Step | Hyp | Ref
| Expression |
1 | | fvex 6856 |
. . . . 5
β’
(WalksβπΊ)
β V |
2 | 1 | mptrabex 7176 |
. . . 4
β’ (π β {π β (WalksβπΊ) β£ (β―β(1st
βπ)) = π} β¦ (2nd
βπ)) β
V |
3 | 2 | resex 5986 |
. . 3
β’ ((π β {π β (WalksβπΊ) β£ (β―β(1st
βπ)) = π} β¦ (2nd
βπ)) βΎ {π β {π β (WalksβπΊ) β£ (β―β(1st
βπ)) = π} β£ ((2nd
βπ)β0) = π}) β V |
4 | | eqid 2733 |
. . . 4
β’ (π β {π β (WalksβπΊ) β£ (β―β(1st
βπ)) = π} β¦ (2nd
βπ)) = (π β {π β (WalksβπΊ) β£ (β―β(1st
βπ)) = π} β¦ (2nd
βπ)) |
5 | | eqid 2733 |
. . . . 5
β’ {π β (WalksβπΊ) β£
(β―β(1st βπ)) = π} = {π β (WalksβπΊ) β£ (β―β(1st
βπ)) = π} |
6 | | eqid 2733 |
. . . . 5
β’ (π WWalksN πΊ) = (π WWalksN πΊ) |
7 | 5, 6, 4 | wlknwwlksnbij 28875 |
. . . 4
β’ ((πΊ β USPGraph β§ π β β0)
β (π β {π β (WalksβπΊ) β£
(β―β(1st βπ)) = π} β¦ (2nd βπ)):{π β (WalksβπΊ) β£ (β―β(1st
βπ)) = π}β1-1-ontoβ(π WWalksN πΊ)) |
8 | | fveq1 6842 |
. . . . . 6
β’ (π€ = (2nd βπ) β (π€β0) = ((2nd βπ)β0)) |
9 | 8 | eqeq1d 2735 |
. . . . 5
β’ (π€ = (2nd βπ) β ((π€β0) = π β ((2nd βπ)β0) = π)) |
10 | 9 | 3ad2ant3 1136 |
. . . 4
β’ (((πΊ β USPGraph β§ π β β0)
β§ π β {π β (WalksβπΊ) β£
(β―β(1st βπ)) = π} β§ π€ = (2nd βπ)) β ((π€β0) = π β ((2nd βπ)β0) = π)) |
11 | 4, 7, 10 | f1oresrab 7074 |
. . 3
β’ ((πΊ β USPGraph β§ π β β0)
β ((π β {π β (WalksβπΊ) β£
(β―β(1st βπ)) = π} β¦ (2nd βπ)) βΎ {π β {π β (WalksβπΊ) β£ (β―β(1st
βπ)) = π} β£ ((2nd
βπ)β0) = π}):{π β {π β (WalksβπΊ) β£ (β―β(1st
βπ)) = π} β£ ((2nd
βπ)β0) = π}β1-1-ontoβ{π€ β (π WWalksN πΊ) β£ (π€β0) = π}) |
12 | | f1oeq1 6773 |
. . . 4
β’ (π = ((π β {π β (WalksβπΊ) β£ (β―β(1st
βπ)) = π} β¦ (2nd
βπ)) βΎ {π β {π β (WalksβπΊ) β£ (β―β(1st
βπ)) = π} β£ ((2nd
βπ)β0) = π}) β (π:{π β {π β (WalksβπΊ) β£ (β―β(1st
βπ)) = π} β£ ((2nd
βπ)β0) = π}β1-1-ontoβ{π€ β (π WWalksN πΊ) β£ (π€β0) = π} β ((π β {π β (WalksβπΊ) β£ (β―β(1st
βπ)) = π} β¦ (2nd
βπ)) βΎ {π β {π β (WalksβπΊ) β£ (β―β(1st
βπ)) = π} β£ ((2nd
βπ)β0) = π}):{π β {π β (WalksβπΊ) β£ (β―β(1st
βπ)) = π} β£ ((2nd
βπ)β0) = π}β1-1-ontoβ{π€ β (π WWalksN πΊ) β£ (π€β0) = π})) |
13 | 12 | spcegv 3555 |
. . 3
β’ (((π β {π β (WalksβπΊ) β£ (β―β(1st
βπ)) = π} β¦ (2nd
βπ)) βΎ {π β {π β (WalksβπΊ) β£ (β―β(1st
βπ)) = π} β£ ((2nd
βπ)β0) = π}) β V β (((π β {π β (WalksβπΊ) β£ (β―β(1st
βπ)) = π} β¦ (2nd
βπ)) βΎ {π β {π β (WalksβπΊ) β£ (β―β(1st
βπ)) = π} β£ ((2nd
βπ)β0) = π}):{π β {π β (WalksβπΊ) β£ (β―β(1st
βπ)) = π} β£ ((2nd
βπ)β0) = π}β1-1-ontoβ{π€ β (π WWalksN πΊ) β£ (π€β0) = π} β βπ π:{π β {π β (WalksβπΊ) β£ (β―β(1st
βπ)) = π} β£ ((2nd
βπ)β0) = π}β1-1-ontoβ{π€ β (π WWalksN πΊ) β£ (π€β0) = π})) |
14 | 3, 11, 13 | mpsyl 68 |
. 2
β’ ((πΊ β USPGraph β§ π β β0)
β βπ π:{π β {π β (WalksβπΊ) β£ (β―β(1st
βπ)) = π} β£ ((2nd
βπ)β0) = π}β1-1-ontoβ{π€ β (π WWalksN πΊ) β£ (π€β0) = π}) |
15 | | 2fveq3 6848 |
. . . . . . 7
β’ (π = π β (β―β(1st
βπ)) =
(β―β(1st βπ))) |
16 | 15 | eqeq1d 2735 |
. . . . . 6
β’ (π = π β ((β―β(1st
βπ)) = π β
(β―β(1st βπ)) = π)) |
17 | 16 | rabrabi 3424 |
. . . . 5
β’ {π β {π β (WalksβπΊ) β£ (β―β(1st
βπ)) = π} β£ ((2nd
βπ)β0) = π} = {π β (WalksβπΊ) β£ ((β―β(1st
βπ)) = π β§ ((2nd
βπ)β0) = π)} |
18 | 17 | eqcomi 2742 |
. . . 4
β’ {π β (WalksβπΊ) β£
((β―β(1st βπ)) = π β§ ((2nd βπ)β0) = π)} = {π β {π β (WalksβπΊ) β£ (β―β(1st
βπ)) = π} β£ ((2nd
βπ)β0) = π} |
19 | | f1oeq2 6774 |
. . . 4
β’ ({π β (WalksβπΊ) β£
((β―β(1st βπ)) = π β§ ((2nd βπ)β0) = π)} = {π β {π β (WalksβπΊ) β£ (β―β(1st
βπ)) = π} β£ ((2nd
βπ)β0) = π} β (π:{π β (WalksβπΊ) β£ ((β―β(1st
βπ)) = π β§ ((2nd
βπ)β0) = π)}β1-1-ontoβ{π€ β (π WWalksN πΊ) β£ (π€β0) = π} β π:{π β {π β (WalksβπΊ) β£ (β―β(1st
βπ)) = π} β£ ((2nd
βπ)β0) = π}β1-1-ontoβ{π€ β (π WWalksN πΊ) β£ (π€β0) = π})) |
20 | 18, 19 | mp1i 13 |
. . 3
β’ ((πΊ β USPGraph β§ π β β0)
β (π:{π β (WalksβπΊ) β£
((β―β(1st βπ)) = π β§ ((2nd βπ)β0) = π)}β1-1-ontoβ{π€ β (π WWalksN πΊ) β£ (π€β0) = π} β π:{π β {π β (WalksβπΊ) β£ (β―β(1st
βπ)) = π} β£ ((2nd
βπ)β0) = π}β1-1-ontoβ{π€ β (π WWalksN πΊ) β£ (π€β0) = π})) |
21 | 20 | exbidv 1925 |
. 2
β’ ((πΊ β USPGraph β§ π β β0)
β (βπ π:{π β (WalksβπΊ) β£ ((β―β(1st
βπ)) = π β§ ((2nd
βπ)β0) = π)}β1-1-ontoβ{π€ β (π WWalksN πΊ) β£ (π€β0) = π} β βπ π:{π β {π β (WalksβπΊ) β£ (β―β(1st
βπ)) = π} β£ ((2nd
βπ)β0) = π}β1-1-ontoβ{π€ β (π WWalksN πΊ) β£ (π€β0) = π})) |
22 | 14, 21 | mpbird 257 |
1
β’ ((πΊ β USPGraph β§ π β β0)
β βπ π:{π β (WalksβπΊ) β£ ((β―β(1st
βπ)) = π β§ ((2nd
βπ)β0) = π)}β1-1-ontoβ{π€ β (π WWalksN πΊ) β£ (π€β0) = π}) |