Step | Hyp | Ref
| Expression |
1 | | fvex 6856 |
. . . . 5
β’
(Vtxβπ») β
V |
2 | | fvex 6856 |
. . . . 5
β’
(Edgβπ») β
V |
3 | | ausgr.1 |
. . . . . 6
β’ πΊ = {β¨π£, πβ© β£ π β {π₯ β π« π£ β£ (β―βπ₯) = 2}} |
4 | 3 | isausgr 28157 |
. . . . 5
β’
(((Vtxβπ»)
β V β§ (Edgβπ») β V) β ((Vtxβπ»)πΊ(Edgβπ») β (Edgβπ») β {π₯ β π« (Vtxβπ») β£ (β―βπ₯) = 2})) |
5 | 1, 2, 4 | mp2an 691 |
. . . 4
β’
((Vtxβπ»)πΊ(Edgβπ») β (Edgβπ») β {π₯ β π« (Vtxβπ») β£ (β―βπ₯) = 2}) |
6 | | edgval 28042 |
. . . . . . 7
β’
(Edgβπ») = ran
(iEdgβπ») |
7 | 6 | a1i 11 |
. . . . . 6
β’ (π» β π β (Edgβπ») = ran (iEdgβπ»)) |
8 | 7 | sseq1d 3976 |
. . . . 5
β’ (π» β π β ((Edgβπ») β {π₯ β π« (Vtxβπ») β£ (β―βπ₯) = 2} β ran
(iEdgβπ») β
{π₯ β π«
(Vtxβπ») β£
(β―βπ₯) =
2})) |
9 | | ausgrusgri.1 |
. . . . . . . . . 10
β’ π = {π β£ π:dom πβ1-1βran π} |
10 | 9 | eleq2i 2826 |
. . . . . . . . 9
β’
((iEdgβπ»)
β π β
(iEdgβπ») β
{π β£ π:dom πβ1-1βran π}) |
11 | | fvex 6856 |
. . . . . . . . . 10
β’
(iEdgβπ»)
β V |
12 | | id 22 |
. . . . . . . . . . 11
β’ (π = (iEdgβπ») β π = (iEdgβπ»)) |
13 | | dmeq 5860 |
. . . . . . . . . . 11
β’ (π = (iEdgβπ») β dom π = dom (iEdgβπ»)) |
14 | | rneq 5892 |
. . . . . . . . . . 11
β’ (π = (iEdgβπ») β ran π = ran (iEdgβπ»)) |
15 | 12, 13, 14 | f1eq123d 6777 |
. . . . . . . . . 10
β’ (π = (iEdgβπ») β (π:dom πβ1-1βran π β (iEdgβπ»):dom (iEdgβπ»)β1-1βran (iEdgβπ»))) |
16 | 11, 15 | elab 3631 |
. . . . . . . . 9
β’
((iEdgβπ»)
β {π β£ π:dom πβ1-1βran π} β (iEdgβπ»):dom (iEdgβπ»)β1-1βran (iEdgβπ»)) |
17 | 10, 16 | sylbb 218 |
. . . . . . . 8
β’
((iEdgβπ»)
β π β
(iEdgβπ»):dom
(iEdgβπ»)β1-1βran (iEdgβπ»)) |
18 | 17 | 3ad2ant3 1136 |
. . . . . . 7
β’ ((π» β π β§ ran (iEdgβπ») β {π₯ β π« (Vtxβπ») β£ (β―βπ₯) = 2} β§ (iEdgβπ») β π) β (iEdgβπ»):dom (iEdgβπ»)β1-1βran (iEdgβπ»)) |
19 | | simp2 1138 |
. . . . . . 7
β’ ((π» β π β§ ran (iEdgβπ») β {π₯ β π« (Vtxβπ») β£ (β―βπ₯) = 2} β§ (iEdgβπ») β π) β ran (iEdgβπ») β {π₯ β π« (Vtxβπ») β£ (β―βπ₯) = 2}) |
20 | | f1ssr 6746 |
. . . . . . 7
β’
(((iEdgβπ»):dom
(iEdgβπ»)β1-1βran (iEdgβπ») β§ ran (iEdgβπ») β {π₯ β π« (Vtxβπ») β£ (β―βπ₯) = 2}) β (iEdgβπ»):dom (iEdgβπ»)β1-1β{π₯ β π« (Vtxβπ») β£ (β―βπ₯) = 2}) |
21 | 18, 19, 20 | syl2anc 585 |
. . . . . 6
β’ ((π» β π β§ ran (iEdgβπ») β {π₯ β π« (Vtxβπ») β£ (β―βπ₯) = 2} β§ (iEdgβπ») β π) β (iEdgβπ»):dom (iEdgβπ»)β1-1β{π₯ β π« (Vtxβπ») β£ (β―βπ₯) = 2}) |
22 | 21 | 3exp 1120 |
. . . . 5
β’ (π» β π β (ran (iEdgβπ») β {π₯ β π« (Vtxβπ») β£ (β―βπ₯) = 2} β ((iEdgβπ») β π β (iEdgβπ»):dom (iEdgβπ»)β1-1β{π₯ β π« (Vtxβπ») β£ (β―βπ₯) = 2}))) |
23 | 8, 22 | sylbid 239 |
. . . 4
β’ (π» β π β ((Edgβπ») β {π₯ β π« (Vtxβπ») β£ (β―βπ₯) = 2} β ((iEdgβπ») β π β (iEdgβπ»):dom (iEdgβπ»)β1-1β{π₯ β π« (Vtxβπ») β£ (β―βπ₯) = 2}))) |
24 | 5, 23 | biimtrid 241 |
. . 3
β’ (π» β π β ((Vtxβπ»)πΊ(Edgβπ») β ((iEdgβπ») β π β (iEdgβπ»):dom (iEdgβπ»)β1-1β{π₯ β π« (Vtxβπ») β£ (β―βπ₯) = 2}))) |
25 | 24 | 3imp 1112 |
. 2
β’ ((π» β π β§ (Vtxβπ»)πΊ(Edgβπ») β§ (iEdgβπ») β π) β (iEdgβπ»):dom (iEdgβπ»)β1-1β{π₯ β π« (Vtxβπ») β£ (β―βπ₯) = 2}) |
26 | | eqid 2733 |
. . . 4
β’
(Vtxβπ») =
(Vtxβπ») |
27 | | eqid 2733 |
. . . 4
β’
(iEdgβπ») =
(iEdgβπ») |
28 | 26, 27 | isusgrs 28149 |
. . 3
β’ (π» β π β (π» β USGraph β (iEdgβπ»):dom (iEdgβπ»)β1-1β{π₯ β π« (Vtxβπ») β£ (β―βπ₯) = 2})) |
29 | 28 | 3ad2ant1 1134 |
. 2
β’ ((π» β π β§ (Vtxβπ»)πΊ(Edgβπ») β§ (iEdgβπ») β π) β (π» β USGraph β (iEdgβπ»):dom (iEdgβπ»)β1-1β{π₯ β π« (Vtxβπ») β£ (β―βπ₯) = 2})) |
30 | 25, 29 | mpbird 257 |
1
β’ ((π» β π β§ (Vtxβπ»)πΊ(Edgβπ») β§ (iEdgβπ») β π) β π» β USGraph) |