Step | Hyp | Ref
| Expression |
1 | | usgr2pthlem.v |
. . 3
β’ π = (VtxβπΊ) |
2 | | usgr2pthlem.i |
. . 3
β’ πΌ = (iEdgβπΊ) |
3 | 1, 2 | usgr2pth 28754 |
. 2
β’ (πΊ β USGraph β ((πΉ(PathsβπΊ)π β§ (β―βπΉ) = 2) β (πΉ:(0..^2)β1-1βdom πΌ β§ π:(0...2)β1-1βπ β§ βπ₯ β π βπ§ β (π β {π₯})βπ¦ β (π β {π₯, π§})(((πβ0) = π₯ β§ (πβ1) = π§ β§ (πβ2) = π¦) β§ ((πΌβ(πΉβ0)) = {π₯, π§} β§ (πΌβ(πΉβ1)) = {π§, π¦}))))) |
4 | | r19.42v 3188 |
. . . . . . . . 9
β’
(βπ¦ β
(π β {π₯, π§})(π§ β π₯ β§ (((πβ0) = π₯ β§ (πβ1) = π§ β§ (πβ2) = π¦) β§ ((πΌβ(πΉβ0)) = {π₯, π§} β§ (πΌβ(πΉβ1)) = {π§, π¦}))) β (π§ β π₯ β§ βπ¦ β (π β {π₯, π§})(((πβ0) = π₯ β§ (πβ1) = π§ β§ (πβ2) = π¦) β§ ((πΌβ(πΉβ0)) = {π₯, π§} β§ (πΌβ(πΉβ1)) = {π§, π¦})))) |
5 | | rexdifpr 4624 |
. . . . . . . . 9
β’
(βπ¦ β
(π β {π₯, π§})(π§ β π₯ β§ (((πβ0) = π₯ β§ (πβ1) = π§ β§ (πβ2) = π¦) β§ ((πΌβ(πΉβ0)) = {π₯, π§} β§ (πΌβ(πΉβ1)) = {π§, π¦}))) β βπ¦ β π (π¦ β π₯ β§ π¦ β π§ β§ (π§ β π₯ β§ (((πβ0) = π₯ β§ (πβ1) = π§ β§ (πβ2) = π¦) β§ ((πΌβ(πΉβ0)) = {π₯, π§} β§ (πΌβ(πΉβ1)) = {π§, π¦}))))) |
6 | 4, 5 | bitr3i 277 |
. . . . . . . 8
β’ ((π§ β π₯ β§ βπ¦ β (π β {π₯, π§})(((πβ0) = π₯ β§ (πβ1) = π§ β§ (πβ2) = π¦) β§ ((πΌβ(πΉβ0)) = {π₯, π§} β§ (πΌβ(πΉβ1)) = {π§, π¦}))) β βπ¦ β π (π¦ β π₯ β§ π¦ β π§ β§ (π§ β π₯ β§ (((πβ0) = π₯ β§ (πβ1) = π§ β§ (πβ2) = π¦) β§ ((πΌβ(πΉβ0)) = {π₯, π§} β§ (πΌβ(πΉβ1)) = {π§, π¦}))))) |
7 | 6 | rexbii 3098 |
. . . . . . 7
β’
(βπ§ β
π (π§ β π₯ β§ βπ¦ β (π β {π₯, π§})(((πβ0) = π₯ β§ (πβ1) = π§ β§ (πβ2) = π¦) β§ ((πΌβ(πΉβ0)) = {π₯, π§} β§ (πΌβ(πΉβ1)) = {π§, π¦}))) β βπ§ β π βπ¦ β π (π¦ β π₯ β§ π¦ β π§ β§ (π§ β π₯ β§ (((πβ0) = π₯ β§ (πβ1) = π§ β§ (πβ2) = π¦) β§ ((πΌβ(πΉβ0)) = {π₯, π§} β§ (πΌβ(πΉβ1)) = {π§, π¦}))))) |
8 | | rexcom 3276 |
. . . . . . 7
β’
(βπ§ β
π βπ¦ β π (π¦ β π₯ β§ π¦ β π§ β§ (π§ β π₯ β§ (((πβ0) = π₯ β§ (πβ1) = π§ β§ (πβ2) = π¦) β§ ((πΌβ(πΉβ0)) = {π₯, π§} β§ (πΌβ(πΉβ1)) = {π§, π¦})))) β βπ¦ β π βπ§ β π (π¦ β π₯ β§ π¦ β π§ β§ (π§ β π₯ β§ (((πβ0) = π₯ β§ (πβ1) = π§ β§ (πβ2) = π¦) β§ ((πΌβ(πΉβ0)) = {π₯, π§} β§ (πΌβ(πΉβ1)) = {π§, π¦}))))) |
9 | | df-3an 1090 |
. . . . . . . . . . 11
β’ ((π¦ β π₯ β§ π¦ β π§ β§ (π§ β π₯ β§ (((πβ0) = π₯ β§ (πβ1) = π§ β§ (πβ2) = π¦) β§ ((πΌβ(πΉβ0)) = {π₯, π§} β§ (πΌβ(πΉβ1)) = {π§, π¦})))) β ((π¦ β π₯ β§ π¦ β π§) β§ (π§ β π₯ β§ (((πβ0) = π₯ β§ (πβ1) = π§ β§ (πβ2) = π¦) β§ ((πΌβ(πΉβ0)) = {π₯, π§} β§ (πΌβ(πΉβ1)) = {π§, π¦}))))) |
10 | | anass 470 |
. . . . . . . . . . 11
β’ ((((π¦ β π₯ β§ π¦ β π§) β§ π§ β π₯) β§ (((πβ0) = π₯ β§ (πβ1) = π§ β§ (πβ2) = π¦) β§ ((πΌβ(πΉβ0)) = {π₯, π§} β§ (πΌβ(πΉβ1)) = {π§, π¦}))) β ((π¦ β π₯ β§ π¦ β π§) β§ (π§ β π₯ β§ (((πβ0) = π₯ β§ (πβ1) = π§ β§ (πβ2) = π¦) β§ ((πΌβ(πΉβ0)) = {π₯, π§} β§ (πΌβ(πΉβ1)) = {π§, π¦}))))) |
11 | | anass 470 |
. . . . . . . . . . . 12
β’ ((((π§ β π₯ β§ π§ β π¦) β§ π¦ β π₯) β§ (((πβ0) = π₯ β§ (πβ1) = π§ β§ (πβ2) = π¦) β§ ((πΌβ(πΉβ0)) = {π₯, π§} β§ (πΌβ(πΉβ1)) = {π§, π¦}))) β ((π§ β π₯ β§ π§ β π¦) β§ (π¦ β π₯ β§ (((πβ0) = π₯ β§ (πβ1) = π§ β§ (πβ2) = π¦) β§ ((πΌβ(πΉβ0)) = {π₯, π§} β§ (πΌβ(πΉβ1)) = {π§, π¦}))))) |
12 | | anass 470 |
. . . . . . . . . . . . . 14
β’ (((π¦ β π₯ β§ π¦ β π§) β§ π§ β π₯) β (π¦ β π₯ β§ (π¦ β π§ β§ π§ β π₯))) |
13 | | ancom 462 |
. . . . . . . . . . . . . 14
β’ ((π¦ β π₯ β§ (π¦ β π§ β§ π§ β π₯)) β ((π¦ β π§ β§ π§ β π₯) β§ π¦ β π₯)) |
14 | | necom 2998 |
. . . . . . . . . . . . . . . 16
β’ (π¦ β π§ β π§ β π¦) |
15 | 14 | anbi2ci 626 |
. . . . . . . . . . . . . . 15
β’ ((π¦ β π§ β§ π§ β π₯) β (π§ β π₯ β§ π§ β π¦)) |
16 | 15 | anbi1i 625 |
. . . . . . . . . . . . . 14
β’ (((π¦ β π§ β§ π§ β π₯) β§ π¦ β π₯) β ((π§ β π₯ β§ π§ β π¦) β§ π¦ β π₯)) |
17 | 12, 13, 16 | 3bitri 297 |
. . . . . . . . . . . . 13
β’ (((π¦ β π₯ β§ π¦ β π§) β§ π§ β π₯) β ((π§ β π₯ β§ π§ β π¦) β§ π¦ β π₯)) |
18 | 17 | anbi1i 625 |
. . . . . . . . . . . 12
β’ ((((π¦ β π₯ β§ π¦ β π§) β§ π§ β π₯) β§ (((πβ0) = π₯ β§ (πβ1) = π§ β§ (πβ2) = π¦) β§ ((πΌβ(πΉβ0)) = {π₯, π§} β§ (πΌβ(πΉβ1)) = {π§, π¦}))) β (((π§ β π₯ β§ π§ β π¦) β§ π¦ β π₯) β§ (((πβ0) = π₯ β§ (πβ1) = π§ β§ (πβ2) = π¦) β§ ((πΌβ(πΉβ0)) = {π₯, π§} β§ (πΌβ(πΉβ1)) = {π§, π¦})))) |
19 | | df-3an 1090 |
. . . . . . . . . . . 12
β’ ((π§ β π₯ β§ π§ β π¦ β§ (π¦ β π₯ β§ (((πβ0) = π₯ β§ (πβ1) = π§ β§ (πβ2) = π¦) β§ ((πΌβ(πΉβ0)) = {π₯, π§} β§ (πΌβ(πΉβ1)) = {π§, π¦})))) β ((π§ β π₯ β§ π§ β π¦) β§ (π¦ β π₯ β§ (((πβ0) = π₯ β§ (πβ1) = π§ β§ (πβ2) = π¦) β§ ((πΌβ(πΉβ0)) = {π₯, π§} β§ (πΌβ(πΉβ1)) = {π§, π¦}))))) |
20 | 11, 18, 19 | 3bitr4i 303 |
. . . . . . . . . . 11
β’ ((((π¦ β π₯ β§ π¦ β π§) β§ π§ β π₯) β§ (((πβ0) = π₯ β§ (πβ1) = π§ β§ (πβ2) = π¦) β§ ((πΌβ(πΉβ0)) = {π₯, π§} β§ (πΌβ(πΉβ1)) = {π§, π¦}))) β (π§ β π₯ β§ π§ β π¦ β§ (π¦ β π₯ β§ (((πβ0) = π₯ β§ (πβ1) = π§ β§ (πβ2) = π¦) β§ ((πΌβ(πΉβ0)) = {π₯, π§} β§ (πΌβ(πΉβ1)) = {π§, π¦}))))) |
21 | 9, 10, 20 | 3bitr2i 299 |
. . . . . . . . . 10
β’ ((π¦ β π₯ β§ π¦ β π§ β§ (π§ β π₯ β§ (((πβ0) = π₯ β§ (πβ1) = π§ β§ (πβ2) = π¦) β§ ((πΌβ(πΉβ0)) = {π₯, π§} β§ (πΌβ(πΉβ1)) = {π§, π¦})))) β (π§ β π₯ β§ π§ β π¦ β§ (π¦ β π₯ β§ (((πβ0) = π₯ β§ (πβ1) = π§ β§ (πβ2) = π¦) β§ ((πΌβ(πΉβ0)) = {π₯, π§} β§ (πΌβ(πΉβ1)) = {π§, π¦}))))) |
22 | 21 | rexbii 3098 |
. . . . . . . . 9
β’
(βπ§ β
π (π¦ β π₯ β§ π¦ β π§ β§ (π§ β π₯ β§ (((πβ0) = π₯ β§ (πβ1) = π§ β§ (πβ2) = π¦) β§ ((πΌβ(πΉβ0)) = {π₯, π§} β§ (πΌβ(πΉβ1)) = {π§, π¦})))) β βπ§ β π (π§ β π₯ β§ π§ β π¦ β§ (π¦ β π₯ β§ (((πβ0) = π₯ β§ (πβ1) = π§ β§ (πβ2) = π¦) β§ ((πΌβ(πΉβ0)) = {π₯, π§} β§ (πΌβ(πΉβ1)) = {π§, π¦}))))) |
23 | | rexdifpr 4624 |
. . . . . . . . 9
β’
(βπ§ β
(π β {π₯, π¦})(π¦ β π₯ β§ (((πβ0) = π₯ β§ (πβ1) = π§ β§ (πβ2) = π¦) β§ ((πΌβ(πΉβ0)) = {π₯, π§} β§ (πΌβ(πΉβ1)) = {π§, π¦}))) β βπ§ β π (π§ β π₯ β§ π§ β π¦ β§ (π¦ β π₯ β§ (((πβ0) = π₯ β§ (πβ1) = π§ β§ (πβ2) = π¦) β§ ((πΌβ(πΉβ0)) = {π₯, π§} β§ (πΌβ(πΉβ1)) = {π§, π¦}))))) |
24 | | r19.42v 3188 |
. . . . . . . . 9
β’
(βπ§ β
(π β {π₯, π¦})(π¦ β π₯ β§ (((πβ0) = π₯ β§ (πβ1) = π§ β§ (πβ2) = π¦) β§ ((πΌβ(πΉβ0)) = {π₯, π§} β§ (πΌβ(πΉβ1)) = {π§, π¦}))) β (π¦ β π₯ β§ βπ§ β (π β {π₯, π¦})(((πβ0) = π₯ β§ (πβ1) = π§ β§ (πβ2) = π¦) β§ ((πΌβ(πΉβ0)) = {π₯, π§} β§ (πΌβ(πΉβ1)) = {π§, π¦})))) |
25 | 22, 23, 24 | 3bitr2i 299 |
. . . . . . . 8
β’
(βπ§ β
π (π¦ β π₯ β§ π¦ β π§ β§ (π§ β π₯ β§ (((πβ0) = π₯ β§ (πβ1) = π§ β§ (πβ2) = π¦) β§ ((πΌβ(πΉβ0)) = {π₯, π§} β§ (πΌβ(πΉβ1)) = {π§, π¦})))) β (π¦ β π₯ β§ βπ§ β (π β {π₯, π¦})(((πβ0) = π₯ β§ (πβ1) = π§ β§ (πβ2) = π¦) β§ ((πΌβ(πΉβ0)) = {π₯, π§} β§ (πΌβ(πΉβ1)) = {π§, π¦})))) |
26 | 25 | rexbii 3098 |
. . . . . . 7
β’
(βπ¦ β
π βπ§ β π (π¦ β π₯ β§ π¦ β π§ β§ (π§ β π₯ β§ (((πβ0) = π₯ β§ (πβ1) = π§ β§ (πβ2) = π¦) β§ ((πΌβ(πΉβ0)) = {π₯, π§} β§ (πΌβ(πΉβ1)) = {π§, π¦})))) β βπ¦ β π (π¦ β π₯ β§ βπ§ β (π β {π₯, π¦})(((πβ0) = π₯ β§ (πβ1) = π§ β§ (πβ2) = π¦) β§ ((πΌβ(πΉβ0)) = {π₯, π§} β§ (πΌβ(πΉβ1)) = {π§, π¦})))) |
27 | 7, 8, 26 | 3bitri 297 |
. . . . . 6
β’
(βπ§ β
π (π§ β π₯ β§ βπ¦ β (π β {π₯, π§})(((πβ0) = π₯ β§ (πβ1) = π§ β§ (πβ2) = π¦) β§ ((πΌβ(πΉβ0)) = {π₯, π§} β§ (πΌβ(πΉβ1)) = {π§, π¦}))) β βπ¦ β π (π¦ β π₯ β§ βπ§ β (π β {π₯, π¦})(((πβ0) = π₯ β§ (πβ1) = π§ β§ (πβ2) = π¦) β§ ((πΌβ(πΉβ0)) = {π₯, π§} β§ (πΌβ(πΉβ1)) = {π§, π¦})))) |
28 | | rexdifsn 4759 |
. . . . . 6
β’
(βπ§ β
(π β {π₯})βπ¦ β (π β {π₯, π§})(((πβ0) = π₯ β§ (πβ1) = π§ β§ (πβ2) = π¦) β§ ((πΌβ(πΉβ0)) = {π₯, π§} β§ (πΌβ(πΉβ1)) = {π§, π¦})) β βπ§ β π (π§ β π₯ β§ βπ¦ β (π β {π₯, π§})(((πβ0) = π₯ β§ (πβ1) = π§ β§ (πβ2) = π¦) β§ ((πΌβ(πΉβ0)) = {π₯, π§} β§ (πΌβ(πΉβ1)) = {π§, π¦})))) |
29 | | rexdifsn 4759 |
. . . . . 6
β’
(βπ¦ β
(π β {π₯})βπ§ β (π β {π₯, π¦})(((πβ0) = π₯ β§ (πβ1) = π§ β§ (πβ2) = π¦) β§ ((πΌβ(πΉβ0)) = {π₯, π§} β§ (πΌβ(πΉβ1)) = {π§, π¦})) β βπ¦ β π (π¦ β π₯ β§ βπ§ β (π β {π₯, π¦})(((πβ0) = π₯ β§ (πβ1) = π§ β§ (πβ2) = π¦) β§ ((πΌβ(πΉβ0)) = {π₯, π§} β§ (πΌβ(πΉβ1)) = {π§, π¦})))) |
30 | 27, 28, 29 | 3bitr4i 303 |
. . . . 5
β’
(βπ§ β
(π β {π₯})βπ¦ β (π β {π₯, π§})(((πβ0) = π₯ β§ (πβ1) = π§ β§ (πβ2) = π¦) β§ ((πΌβ(πΉβ0)) = {π₯, π§} β§ (πΌβ(πΉβ1)) = {π§, π¦})) β βπ¦ β (π β {π₯})βπ§ β (π β {π₯, π¦})(((πβ0) = π₯ β§ (πβ1) = π§ β§ (πβ2) = π¦) β§ ((πΌβ(πΉβ0)) = {π₯, π§} β§ (πΌβ(πΉβ1)) = {π§, π¦}))) |
31 | 30 | a1i 11 |
. . . 4
β’ ((πΊ β USGraph β§ π₯ β π) β (βπ§ β (π β {π₯})βπ¦ β (π β {π₯, π§})(((πβ0) = π₯ β§ (πβ1) = π§ β§ (πβ2) = π¦) β§ ((πΌβ(πΉβ0)) = {π₯, π§} β§ (πΌβ(πΉβ1)) = {π§, π¦})) β βπ¦ β (π β {π₯})βπ§ β (π β {π₯, π¦})(((πβ0) = π₯ β§ (πβ1) = π§ β§ (πβ2) = π¦) β§ ((πΌβ(πΉβ0)) = {π₯, π§} β§ (πΌβ(πΉβ1)) = {π§, π¦})))) |
32 | 31 | rexbidva 3174 |
. . 3
β’ (πΊ β USGraph β
(βπ₯ β π βπ§ β (π β {π₯})βπ¦ β (π β {π₯, π§})(((πβ0) = π₯ β§ (πβ1) = π§ β§ (πβ2) = π¦) β§ ((πΌβ(πΉβ0)) = {π₯, π§} β§ (πΌβ(πΉβ1)) = {π§, π¦})) β βπ₯ β π βπ¦ β (π β {π₯})βπ§ β (π β {π₯, π¦})(((πβ0) = π₯ β§ (πβ1) = π§ β§ (πβ2) = π¦) β§ ((πΌβ(πΉβ0)) = {π₯, π§} β§ (πΌβ(πΉβ1)) = {π§, π¦})))) |
33 | 32 | 3anbi3d 1443 |
. 2
β’ (πΊ β USGraph β ((πΉ:(0..^2)β1-1βdom πΌ β§ π:(0...2)β1-1βπ β§ βπ₯ β π βπ§ β (π β {π₯})βπ¦ β (π β {π₯, π§})(((πβ0) = π₯ β§ (πβ1) = π§ β§ (πβ2) = π¦) β§ ((πΌβ(πΉβ0)) = {π₯, π§} β§ (πΌβ(πΉβ1)) = {π§, π¦}))) β (πΉ:(0..^2)β1-1βdom πΌ β§ π:(0...2)β1-1βπ β§ βπ₯ β π βπ¦ β (π β {π₯})βπ§ β (π β {π₯, π¦})(((πβ0) = π₯ β§ (πβ1) = π§ β§ (πβ2) = π¦) β§ ((πΌβ(πΉβ0)) = {π₯, π§} β§ (πΌβ(πΉβ1)) = {π§, π¦}))))) |
34 | 3, 33 | bitrd 279 |
1
β’ (πΊ β USGraph β ((πΉ(PathsβπΊ)π β§ (β―βπΉ) = 2) β (πΉ:(0..^2)β1-1βdom πΌ β§ π:(0...2)β1-1βπ β§ βπ₯ β π βπ¦ β (π β {π₯})βπ§ β (π β {π₯, π¦})(((πβ0) = π₯ β§ (πβ1) = π§ β§ (πβ2) = π¦) β§ ((πΌβ(πΉβ0)) = {π₯, π§} β§ (πΌβ(πΉβ1)) = {π§, π¦}))))) |