Step | Hyp | Ref
| Expression |
1 | | 0nn0 12433 |
. . . . . . . . . . . . . 14
β’ 0 β
β0 |
2 | | 2nn0 12435 |
. . . . . . . . . . . . . 14
β’ 2 β
β0 |
3 | | 0le2 12260 |
. . . . . . . . . . . . . 14
β’ 0 β€
2 |
4 | | elfz2nn0 13538 |
. . . . . . . . . . . . . 14
β’ (0 β
(0...2) β (0 β β0 β§ 2 β β0
β§ 0 β€ 2)) |
5 | 1, 2, 3, 4 | mpbir3an 1342 |
. . . . . . . . . . . . 13
β’ 0 β
(0...2) |
6 | | ffvelcdm 7033 |
. . . . . . . . . . . . 13
β’ ((π:(0...2)βΆπ β§ 0 β (0...2)) β
(πβ0) β π) |
7 | 5, 6 | mpan2 690 |
. . . . . . . . . . . 12
β’ (π:(0...2)βΆπ β (πβ0) β π) |
8 | 7 | adantl 483 |
. . . . . . . . . . 11
β’ ((((πΉ:(0..^2)β1-1βdom πΌ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})) β§ πΊ β USGraph) β§ π:(0...2)βΆπ) β (πβ0) β π) |
9 | | 1nn0 12434 |
. . . . . . . . . . . . . . . . . 18
β’ 1 β
β0 |
10 | | 1le2 12367 |
. . . . . . . . . . . . . . . . . 18
β’ 1 β€
2 |
11 | | elfz2nn0 13538 |
. . . . . . . . . . . . . . . . . 18
β’ (1 β
(0...2) β (1 β β0 β§ 2 β β0
β§ 1 β€ 2)) |
12 | 9, 2, 10, 11 | mpbir3an 1342 |
. . . . . . . . . . . . . . . . 17
β’ 1 β
(0...2) |
13 | | ffvelcdm 7033 |
. . . . . . . . . . . . . . . . 17
β’ ((π:(0...2)βΆπ β§ 1 β (0...2)) β
(πβ1) β π) |
14 | 12, 13 | mpan2 690 |
. . . . . . . . . . . . . . . 16
β’ (π:(0...2)βΆπ β (πβ1) β π) |
15 | 14 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((((πΉ:(0..^2)β1-1βdom πΌ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})) β§ πΊ β USGraph) β§ π:(0...2)βΆπ) β (πβ1) β π) |
16 | | simpr 486 |
. . . . . . . . . . . . . . . . . . 19
β’ (((πΉ:(0..^2)β1-1βdom πΌ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})) β§ πΊ β USGraph) β πΊ β USGraph) |
17 | | fvex 6856 |
. . . . . . . . . . . . . . . . . . 19
β’ (πβ1) β
V |
18 | 16, 17 | jctir 522 |
. . . . . . . . . . . . . . . . . 18
β’ (((πΉ:(0..^2)β1-1βdom πΌ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})) β§ πΊ β USGraph) β (πΊ β USGraph β§ (πβ1) β V)) |
19 | | prcom 4694 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ {(πβ0), (πβ1)} = {(πβ1), (πβ0)} |
20 | 19 | eqeq2i 2746 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β (πΌβ(πΉβ0)) = {(πβ1), (πβ0)}) |
21 | 20 | biimpi 215 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β (πΌβ(πΉβ0)) = {(πβ1), (πβ0)}) |
22 | 21 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ (((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)}) β (πΌβ(πΉβ0)) = {(πβ1), (πβ0)}) |
23 | 22 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . 18
β’ (((πΉ:(0..^2)β1-1βdom πΌ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})) β§ πΊ β USGraph) β (πΌβ(πΉβ0)) = {(πβ1), (πβ0)}) |
24 | | usgr2pthlem.i |
. . . . . . . . . . . . . . . . . . 19
β’ πΌ = (iEdgβπΊ) |
25 | 24 | usgrnloopv 28190 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΊ β USGraph β§ (πβ1) β V) β
((πΌβ(πΉβ0)) = {(πβ1), (πβ0)} β (πβ1) β (πβ0))) |
26 | 18, 23, 25 | sylc 65 |
. . . . . . . . . . . . . . . . 17
β’ (((πΉ:(0..^2)β1-1βdom πΌ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})) β§ πΊ β USGraph) β (πβ1) β (πβ0)) |
27 | 26 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((((πΉ:(0..^2)β1-1βdom πΌ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})) β§ πΊ β USGraph) β§ π:(0...2)βΆπ) β (πβ1) β (πβ0)) |
28 | 17 | elsn 4602 |
. . . . . . . . . . . . . . . . 17
β’ ((πβ1) β {(πβ0)} β (πβ1) = (πβ0)) |
29 | 28 | necon3bbii 2988 |
. . . . . . . . . . . . . . . 16
β’ (Β¬
(πβ1) β {(πβ0)} β (πβ1) β (πβ0)) |
30 | 27, 29 | sylibr 233 |
. . . . . . . . . . . . . . 15
β’ ((((πΉ:(0..^2)β1-1βdom πΌ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})) β§ πΊ β USGraph) β§ π:(0...2)βΆπ) β Β¬ (πβ1) β {(πβ0)}) |
31 | 15, 30 | eldifd 3922 |
. . . . . . . . . . . . . 14
β’ ((((πΉ:(0..^2)β1-1βdom πΌ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})) β§ πΊ β USGraph) β§ π:(0...2)βΆπ) β (πβ1) β (π β {(πβ0)})) |
32 | 31 | adantr 482 |
. . . . . . . . . . . . 13
β’
(((((πΉ:(0..^2)β1-1βdom πΌ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})) β§ πΊ β USGraph) β§ π:(0...2)βΆπ) β§ π₯ = (πβ0)) β (πβ1) β (π β {(πβ0)})) |
33 | | sneq 4597 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = (πβ0) β {π₯} = {(πβ0)}) |
34 | 33 | difeq2d 4083 |
. . . . . . . . . . . . . . 15
β’ (π₯ = (πβ0) β (π β {π₯}) = (π β {(πβ0)})) |
35 | 34 | eleq2d 2820 |
. . . . . . . . . . . . . 14
β’ (π₯ = (πβ0) β ((πβ1) β (π β {π₯}) β (πβ1) β (π β {(πβ0)}))) |
36 | 35 | adantl 483 |
. . . . . . . . . . . . 13
β’
(((((πΉ:(0..^2)β1-1βdom πΌ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})) β§ πΊ β USGraph) β§ π:(0...2)βΆπ) β§ π₯ = (πβ0)) β ((πβ1) β (π β {π₯}) β (πβ1) β (π β {(πβ0)}))) |
37 | 32, 36 | mpbird 257 |
. . . . . . . . . . . 12
β’
(((((πΉ:(0..^2)β1-1βdom πΌ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})) β§ πΊ β USGraph) β§ π:(0...2)βΆπ) β§ π₯ = (πβ0)) β (πβ1) β (π β {π₯})) |
38 | | 2re 12232 |
. . . . . . . . . . . . . . . . . . . 20
β’ 2 β
β |
39 | 38 | leidi 11694 |
. . . . . . . . . . . . . . . . . . 19
β’ 2 β€
2 |
40 | | elfz2nn0 13538 |
. . . . . . . . . . . . . . . . . . 19
β’ (2 β
(0...2) β (2 β β0 β§ 2 β β0
β§ 2 β€ 2)) |
41 | 2, 2, 39, 40 | mpbir3an 1342 |
. . . . . . . . . . . . . . . . . 18
β’ 2 β
(0...2) |
42 | | ffvelcdm 7033 |
. . . . . . . . . . . . . . . . . 18
β’ ((π:(0...2)βΆπ β§ 2 β (0...2)) β
(πβ2) β π) |
43 | 41, 42 | mpan2 690 |
. . . . . . . . . . . . . . . . 17
β’ (π:(0...2)βΆπ β (πβ2) β π) |
44 | 43 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ ((((πΉ:(0..^2)β1-1βdom πΌ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})) β§ πΊ β USGraph) β§ π:(0...2)βΆπ) β (πβ2) β π) |
45 | 24 | usgrf1 28165 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (πΊ β USGraph β πΌ:dom πΌβ1-1βran πΌ) |
46 | 45 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((πΉ:(0..^2)β1-1βdom πΌ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})) β§ πΊ β USGraph) β§ π:(0...2)βΆπ) β πΌ:dom πΌβ1-1βran πΌ) |
47 | | simpl 484 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((πΉ:(0..^2)β1-1βdom πΌ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})) β πΉ:(0..^2)β1-1βdom πΌ) |
48 | 47 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((πΉ:(0..^2)β1-1βdom πΌ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})) β§ πΊ β USGraph) β§ π:(0...2)βΆπ) β πΉ:(0..^2)β1-1βdom πΌ) |
49 | 46, 48 | jca 513 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((πΉ:(0..^2)β1-1βdom πΌ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})) β§ πΊ β USGraph) β§ π:(0...2)βΆπ) β (πΌ:dom πΌβ1-1βran πΌ β§ πΉ:(0..^2)β1-1βdom πΌ)) |
50 | | 2nn 12231 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ 2 β
β |
51 | | lbfzo0 13618 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (0 β
(0..^2) β 2 β β) |
52 | 50, 51 | mpbir 230 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ 0 β
(0..^2) |
53 | | 1lt2 12329 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ 1 <
2 |
54 | | elfzo0 13619 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (1 β
(0..^2) β (1 β β0 β§ 2 β β β§ 1
< 2)) |
55 | 9, 50, 53, 54 | mpbir3an 1342 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ 1 β
(0..^2) |
56 | 52, 55 | pm3.2i 472 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (0 β
(0..^2) β§ 1 β (0..^2)) |
57 | 56 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((πΉ:(0..^2)β1-1βdom πΌ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})) β§ πΊ β USGraph) β§ π:(0...2)βΆπ) β (0 β (0..^2) β§ 1 β
(0..^2))) |
58 | | 0ne1 12229 |
. . . . . . . . . . . . . . . . . . . . 21
β’ 0 β
1 |
59 | 58 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((πΉ:(0..^2)β1-1βdom πΌ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})) β§ πΊ β USGraph) β§ π:(0...2)βΆπ) β 0 β 1) |
60 | 49, 57, 59 | 3jca 1129 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((πΉ:(0..^2)β1-1βdom πΌ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})) β§ πΊ β USGraph) β§ π:(0...2)βΆπ) β ((πΌ:dom πΌβ1-1βran πΌ β§ πΉ:(0..^2)β1-1βdom πΌ) β§ (0 β (0..^2) β§ 1 β
(0..^2)) β§ 0 β 1)) |
61 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πΉ:(0..^2)β1-1βdom πΌ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})) β ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})) |
62 | 61 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((πΉ:(0..^2)β1-1βdom πΌ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})) β§ πΊ β USGraph) β§ π:(0...2)βΆπ) β ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})) |
63 | | 2f1fvneq 7208 |
. . . . . . . . . . . . . . . . . . 19
β’ (((πΌ:dom πΌβ1-1βran πΌ β§ πΉ:(0..^2)β1-1βdom πΌ) β§ (0 β (0..^2) β§ 1 β
(0..^2)) β§ 0 β 1) β (((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)}) β {(πβ0), (πβ1)} β {(πβ1), (πβ2)})) |
64 | 60, 62, 63 | sylc 65 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πΉ:(0..^2)β1-1βdom πΌ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})) β§ πΊ β USGraph) β§ π:(0...2)βΆπ) β {(πβ0), (πβ1)} β {(πβ1), (πβ2)}) |
65 | | necom 2994 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πβ2) β (πβ0) β (πβ0) β (πβ2)) |
66 | | fvex 6856 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (πβ0) β
V |
67 | | fvex 6856 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (πβ2) β
V |
68 | 66, 17, 67 | 3pm3.2i 1340 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πβ0) β V β§ (πβ1) β V β§ (πβ2) β
V) |
69 | | fvexd 6858 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((πΉ:(0..^2)β1-1βdom πΌ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})) β§ πΊ β USGraph) β (πβ0) β V) |
70 | | simpl 484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)}) β (πΌβ(πΉβ0)) = {(πβ0), (πβ1)}) |
71 | 70 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((πΉ:(0..^2)β1-1βdom πΌ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})) β§ πΊ β USGraph) β (πΌβ(πΉβ0)) = {(πβ0), (πβ1)}) |
72 | 16, 69, 71 | jca31 516 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((πΉ:(0..^2)β1-1βdom πΌ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})) β§ πΊ β USGraph) β ((πΊ β USGraph β§ (πβ0) β V) β§ (πΌβ(πΉβ0)) = {(πβ0), (πβ1)})) |
73 | 72 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((πΉ:(0..^2)β1-1βdom πΌ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})) β§ πΊ β USGraph) β§ π:(0...2)βΆπ) β ((πΊ β USGraph β§ (πβ0) β V) β§ (πΌβ(πΉβ0)) = {(πβ0), (πβ1)})) |
74 | 24 | usgrnloopv 28190 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((πΊ β USGraph β§ (πβ0) β V) β
((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β (πβ0) β (πβ1))) |
75 | 74 | imp 408 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((πΊ β USGraph β§ (πβ0) β V) β§ (πΌβ(πΉβ0)) = {(πβ0), (πβ1)}) β (πβ0) β (πβ1)) |
76 | 73, 75 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((πΉ:(0..^2)β1-1βdom πΌ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})) β§ πΊ β USGraph) β§ π:(0...2)βΆπ) β (πβ0) β (πβ1)) |
77 | | pr1nebg 4816 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((πβ0) β V β§ (πβ1) β V β§ (πβ2) β V) β§ (πβ0) β (πβ1)) β ((πβ0) β (πβ2) β {(πβ0), (πβ1)} β {(πβ1), (πβ2)})) |
78 | 68, 76, 77 | sylancr 588 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((πΉ:(0..^2)β1-1βdom πΌ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})) β§ πΊ β USGraph) β§ π:(0...2)βΆπ) β ((πβ0) β (πβ2) β {(πβ0), (πβ1)} β {(πβ1), (πβ2)})) |
79 | 65, 78 | bitrid 283 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πΉ:(0..^2)β1-1βdom πΌ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})) β§ πΊ β USGraph) β§ π:(0...2)βΆπ) β ((πβ2) β (πβ0) β {(πβ0), (πβ1)} β {(πβ1), (πβ2)})) |
80 | 64, 79 | mpbird 257 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΉ:(0..^2)β1-1βdom πΌ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})) β§ πΊ β USGraph) β§ π:(0...2)βΆπ) β (πβ2) β (πβ0)) |
81 | | fvexd 6858 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((πΉ:(0..^2)β1-1βdom πΌ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})) β§ πΊ β USGraph) β (πβ2) β V) |
82 | | prcom 4694 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ {(πβ1), (πβ2)} = {(πβ2), (πβ1)} |
83 | 82 | eqeq2i 2746 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((πΌβ(πΉβ1)) = {(πβ1), (πβ2)} β (πΌβ(πΉβ1)) = {(πβ2), (πβ1)}) |
84 | 83 | biimpi 215 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((πΌβ(πΉβ1)) = {(πβ1), (πβ2)} β (πΌβ(πΉβ1)) = {(πβ2), (πβ1)}) |
85 | 84 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)}) β (πΌβ(πΉβ1)) = {(πβ2), (πβ1)}) |
86 | 85 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((πΉ:(0..^2)β1-1βdom πΌ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})) β§ πΊ β USGraph) β (πΌβ(πΉβ1)) = {(πβ2), (πβ1)}) |
87 | 16, 81, 86 | jca31 516 |
. . . . . . . . . . . . . . . . . . 19
β’ (((πΉ:(0..^2)β1-1βdom πΌ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})) β§ πΊ β USGraph) β ((πΊ β USGraph β§ (πβ2) β V) β§ (πΌβ(πΉβ1)) = {(πβ2), (πβ1)})) |
88 | 87 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πΉ:(0..^2)β1-1βdom πΌ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})) β§ πΊ β USGraph) β§ π:(0...2)βΆπ) β ((πΊ β USGraph β§ (πβ2) β V) β§ (πΌβ(πΉβ1)) = {(πβ2), (πβ1)})) |
89 | 24 | usgrnloopv 28190 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΊ β USGraph β§ (πβ2) β V) β
((πΌβ(πΉβ1)) = {(πβ2), (πβ1)} β (πβ2) β (πβ1))) |
90 | 89 | imp 408 |
. . . . . . . . . . . . . . . . . 18
β’ (((πΊ β USGraph β§ (πβ2) β V) β§ (πΌβ(πΉβ1)) = {(πβ2), (πβ1)}) β (πβ2) β (πβ1)) |
91 | 88, 90 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΉ:(0..^2)β1-1βdom πΌ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})) β§ πΊ β USGraph) β§ π:(0...2)βΆπ) β (πβ2) β (πβ1)) |
92 | 80, 91 | nelprd 4618 |
. . . . . . . . . . . . . . . 16
β’ ((((πΉ:(0..^2)β1-1βdom πΌ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})) β§ πΊ β USGraph) β§ π:(0...2)βΆπ) β Β¬ (πβ2) β {(πβ0), (πβ1)}) |
93 | 44, 92 | eldifd 3922 |
. . . . . . . . . . . . . . 15
β’ ((((πΉ:(0..^2)β1-1βdom πΌ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})) β§ πΊ β USGraph) β§ π:(0...2)βΆπ) β (πβ2) β (π β {(πβ0), (πβ1)})) |
94 | 93 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’
((((((πΉ:(0..^2)β1-1βdom πΌ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})) β§ πΊ β USGraph) β§ π:(0...2)βΆπ) β§ π₯ = (πβ0)) β§ π¦ = (πβ1)) β (πβ2) β (π β {(πβ0), (πβ1)})) |
95 | | preq12 4697 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ = (πβ0) β§ π¦ = (πβ1)) β {π₯, π¦} = {(πβ0), (πβ1)}) |
96 | 95 | difeq2d 4083 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ = (πβ0) β§ π¦ = (πβ1)) β (π β {π₯, π¦}) = (π β {(πβ0), (πβ1)})) |
97 | 96 | eleq2d 2820 |
. . . . . . . . . . . . . . 15
β’ ((π₯ = (πβ0) β§ π¦ = (πβ1)) β ((πβ2) β (π β {π₯, π¦}) β (πβ2) β (π β {(πβ0), (πβ1)}))) |
98 | 97 | adantll 713 |
. . . . . . . . . . . . . 14
β’
((((((πΉ:(0..^2)β1-1βdom πΌ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})) β§ πΊ β USGraph) β§ π:(0...2)βΆπ) β§ π₯ = (πβ0)) β§ π¦ = (πβ1)) β ((πβ2) β (π β {π₯, π¦}) β (πβ2) β (π β {(πβ0), (πβ1)}))) |
99 | 94, 98 | mpbird 257 |
. . . . . . . . . . . . 13
β’
((((((πΉ:(0..^2)β1-1βdom πΌ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})) β§ πΊ β USGraph) β§ π:(0...2)βΆπ) β§ π₯ = (πβ0)) β§ π¦ = (πβ1)) β (πβ2) β (π β {π₯, π¦})) |
100 | | eqcom 2740 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ = (πβ0) β (πβ0) = π₯) |
101 | | eqcom 2740 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π¦ = (πβ1) β (πβ1) = π¦) |
102 | | eqcom 2740 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π§ = (πβ2) β (πβ2) = π§) |
103 | 100, 101,
102 | 3anbi123i 1156 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π₯ = (πβ0) β§ π¦ = (πβ1) β§ π§ = (πβ2)) β ((πβ0) = π₯ β§ (πβ1) = π¦ β§ (πβ2) = π§)) |
104 | 103 | biimpi 215 |
. . . . . . . . . . . . . . . . . 18
β’ ((π₯ = (πβ0) β§ π¦ = (πβ1) β§ π§ = (πβ2)) β ((πβ0) = π₯ β§ (πβ1) = π¦ β§ (πβ2) = π§)) |
105 | 104 | ad4ant123 1173 |
. . . . . . . . . . . . . . . . 17
β’ ((((π₯ = (πβ0) β§ π¦ = (πβ1)) β§ π§ = (πβ2)) β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})) β ((πβ0) = π₯ β§ (πβ1) = π¦ β§ (πβ2) = π§)) |
106 | 100 | biimpi 215 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π₯ = (πβ0) β (πβ0) = π₯) |
107 | 106 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π₯ = (πβ0) β§ π¦ = (πβ1)) β§ π§ = (πβ2)) β (πβ0) = π₯) |
108 | 101 | biimpi 215 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π¦ = (πβ1) β (πβ1) = π¦) |
109 | 108 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π₯ = (πβ0) β§ π¦ = (πβ1)) β§ π§ = (πβ2)) β (πβ1) = π¦) |
110 | 107, 109 | preq12d 4703 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π₯ = (πβ0) β§ π¦ = (πβ1)) β§ π§ = (πβ2)) β {(πβ0), (πβ1)} = {π₯, π¦}) |
111 | 110 | eqeq2d 2744 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π₯ = (πβ0) β§ π¦ = (πβ1)) β§ π§ = (πβ2)) β ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β (πΌβ(πΉβ0)) = {π₯, π¦})) |
112 | 102 | biimpi 215 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π§ = (πβ2) β (πβ2) = π§) |
113 | 112 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π₯ = (πβ0) β§ π¦ = (πβ1)) β§ π§ = (πβ2)) β (πβ2) = π§) |
114 | 109, 113 | preq12d 4703 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π₯ = (πβ0) β§ π¦ = (πβ1)) β§ π§ = (πβ2)) β {(πβ1), (πβ2)} = {π¦, π§}) |
115 | 114 | eqeq2d 2744 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π₯ = (πβ0) β§ π¦ = (πβ1)) β§ π§ = (πβ2)) β ((πΌβ(πΉβ1)) = {(πβ1), (πβ2)} β (πΌβ(πΉβ1)) = {π¦, π§})) |
116 | 111, 115 | anbi12d 632 |
. . . . . . . . . . . . . . . . . 18
β’ (((π₯ = (πβ0) β§ π¦ = (πβ1)) β§ π§ = (πβ2)) β (((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)}) β ((πΌβ(πΉβ0)) = {π₯, π¦} β§ (πΌβ(πΉβ1)) = {π¦, π§}))) |
117 | 116 | biimpa 478 |
. . . . . . . . . . . . . . . . 17
β’ ((((π₯ = (πβ0) β§ π¦ = (πβ1)) β§ π§ = (πβ2)) β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})) β ((πΌβ(πΉβ0)) = {π₯, π¦} β§ (πΌβ(πΉβ1)) = {π¦, π§})) |
118 | 105, 117 | jca 513 |
. . . . . . . . . . . . . . . 16
β’ ((((π₯ = (πβ0) β§ π¦ = (πβ1)) β§ π§ = (πβ2)) β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})) β (((πβ0) = π₯ β§ (πβ1) = π¦ β§ (πβ2) = π§) β§ ((πΌβ(πΉβ0)) = {π₯, π¦} β§ (πΌβ(πΉβ1)) = {π¦, π§}))) |
119 | 118 | exp41 436 |
. . . . . . . . . . . . . . 15
β’ (π₯ = (πβ0) β (π¦ = (πβ1) β (π§ = (πβ2) β (((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)}) β (((πβ0) = π₯ β§ (πβ1) = π¦ β§ (πβ2) = π§) β§ ((πΌβ(πΉβ0)) = {π₯, π¦} β§ (πΌβ(πΉβ1)) = {π¦, π§})))))) |
120 | 119 | adantl 483 |
. . . . . . . . . . . . . 14
β’
(((((πΉ:(0..^2)β1-1βdom πΌ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})) β§ πΊ β USGraph) β§ π:(0...2)βΆπ) β§ π₯ = (πβ0)) β (π¦ = (πβ1) β (π§ = (πβ2) β (((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)}) β (((πβ0) = π₯ β§ (πβ1) = π¦ β§ (πβ2) = π§) β§ ((πΌβ(πΉβ0)) = {π₯, π¦} β§ (πΌβ(πΉβ1)) = {π¦, π§})))))) |
121 | 120 | imp31 419 |
. . . . . . . . . . . . 13
β’
(((((((πΉ:(0..^2)β1-1βdom πΌ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})) β§ πΊ β USGraph) β§ π:(0...2)βΆπ) β§ π₯ = (πβ0)) β§ π¦ = (πβ1)) β§ π§ = (πβ2)) β (((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)}) β (((πβ0) = π₯ β§ (πβ1) = π¦ β§ (πβ2) = π§) β§ ((πΌβ(πΉβ0)) = {π₯, π¦} β§ (πΌβ(πΉβ1)) = {π¦, π§})))) |
122 | 99, 121 | rspcimedv 3571 |
. . . . . . . . . . . 12
β’
((((((πΉ:(0..^2)β1-1βdom πΌ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})) β§ πΊ β USGraph) β§ π:(0...2)βΆπ) β§ π₯ = (πβ0)) β§ π¦ = (πβ1)) β (((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)}) β βπ§ β (π β {π₯, π¦})(((πβ0) = π₯ β§ (πβ1) = π¦ β§ (πβ2) = π§) β§ ((πΌβ(πΉβ0)) = {π₯, π¦} β§ (πΌβ(πΉβ1)) = {π¦, π§})))) |
123 | 37, 122 | rspcimedv 3571 |
. . . . . . . . . . 11
β’
(((((πΉ:(0..^2)β1-1βdom πΌ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})) β§ πΊ β USGraph) β§ π:(0...2)βΆπ) β§ π₯ = (πβ0)) β (((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)}) β βπ¦ β (π β {π₯})βπ§ β (π β {π₯, π¦})(((πβ0) = π₯ β§ (πβ1) = π¦ β§ (πβ2) = π§) β§ ((πΌβ(πΉβ0)) = {π₯, π¦} β§ (πΌβ(πΉβ1)) = {π¦, π§})))) |
124 | 8, 123 | rspcimedv 3571 |
. . . . . . . . . 10
β’ ((((πΉ:(0..^2)β1-1βdom πΌ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})) β§ πΊ β USGraph) β§ π:(0...2)βΆπ) β (((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)}) β βπ₯ β π βπ¦ β (π β {π₯})βπ§ β (π β {π₯, π¦})(((πβ0) = π₯ β§ (πβ1) = π¦ β§ (πβ2) = π§) β§ ((πΌβ(πΉβ0)) = {π₯, π¦} β§ (πΌβ(πΉβ1)) = {π¦, π§})))) |
125 | 124 | exp41 436 |
. . . . . . . . 9
β’ (πΉ:(0..^2)β1-1βdom πΌ β (((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)}) β (πΊ β USGraph β (π:(0...2)βΆπ β (((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)}) β βπ₯ β π βπ¦ β (π β {π₯})βπ§ β (π β {π₯, π¦})(((πβ0) = π₯ β§ (πβ1) = π¦ β§ (πβ2) = π§) β§ ((πΌβ(πΉβ0)) = {π₯, π¦} β§ (πΌβ(πΉβ1)) = {π¦, π§}))))))) |
126 | 125 | com15 101 |
. . . . . . . 8
β’ (((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)}) β (((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)}) β (πΊ β USGraph β (π:(0...2)βΆπ β (πΉ:(0..^2)β1-1βdom πΌ β βπ₯ β π βπ¦ β (π β {π₯})βπ§ β (π β {π₯, π¦})(((πβ0) = π₯ β§ (πβ1) = π¦ β§ (πβ2) = π§) β§ ((πΌβ(πΉβ0)) = {π₯, π¦} β§ (πΌβ(πΉβ1)) = {π¦, π§}))))))) |
127 | 126 | pm2.43i 52 |
. . . . . . 7
β’ (((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)}) β (πΊ β USGraph β (π:(0...2)βΆπ β (πΉ:(0..^2)β1-1βdom πΌ β βπ₯ β π βπ¦ β (π β {π₯})βπ§ β (π β {π₯, π¦})(((πβ0) = π₯ β§ (πβ1) = π¦ β§ (πβ2) = π§) β§ ((πΌβ(πΉβ0)) = {π₯, π¦} β§ (πΌβ(πΉβ1)) = {π¦, π§})))))) |
128 | 127 | com12 32 |
. . . . . 6
β’ (πΊ β USGraph β (((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)}) β (π:(0...2)βΆπ β (πΉ:(0..^2)β1-1βdom πΌ β βπ₯ β π βπ¦ β (π β {π₯})βπ§ β (π β {π₯, π¦})(((πβ0) = π₯ β§ (πβ1) = π¦ β§ (πβ2) = π§) β§ ((πΌβ(πΉβ0)) = {π₯, π¦} β§ (πΌβ(πΉβ1)) = {π¦, π§})))))) |
129 | 128 | adantr 482 |
. . . . 5
β’ ((πΊ β USGraph β§
(β―βπΉ) = 2)
β (((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)}) β (π:(0...2)βΆπ β (πΉ:(0..^2)β1-1βdom πΌ β βπ₯ β π βπ¦ β (π β {π₯})βπ§ β (π β {π₯, π¦})(((πβ0) = π₯ β§ (πβ1) = π¦ β§ (πβ2) = π§) β§ ((πΌβ(πΉβ0)) = {π₯, π¦} β§ (πΌβ(πΉβ1)) = {π¦, π§})))))) |
130 | | oveq2 7366 |
. . . . . . . 8
β’
((β―βπΉ) =
2 β (0..^(β―βπΉ)) = (0..^2)) |
131 | 130 | raleqdv 3312 |
. . . . . . 7
β’
((β―βπΉ) =
2 β (βπ β
(0..^(β―βπΉ))(πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))} β βπ β (0..^2)(πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))})) |
132 | | fzo0to2pr 13663 |
. . . . . . . . 9
β’ (0..^2) =
{0, 1} |
133 | 132 | raleqi 3310 |
. . . . . . . 8
β’
(βπ β
(0..^2)(πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))} β βπ β {0, 1} (πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))}) |
134 | | 2wlklem 28657 |
. . . . . . . 8
β’
(βπ β
{0, 1} (πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))} β ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})) |
135 | 133, 134 | bitri 275 |
. . . . . . 7
β’
(βπ β
(0..^2)(πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))} β ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})) |
136 | 131, 135 | bitrdi 287 |
. . . . . 6
β’
((β―βπΉ) =
2 β (βπ β
(0..^(β―βπΉ))(πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))} β ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)}))) |
137 | 136 | adantl 483 |
. . . . 5
β’ ((πΊ β USGraph β§
(β―βπΉ) = 2)
β (βπ β
(0..^(β―βπΉ))(πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))} β ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)}))) |
138 | | oveq2 7366 |
. . . . . . . 8
β’
((β―βπΉ) =
2 β (0...(β―βπΉ)) = (0...2)) |
139 | 138 | feq2d 6655 |
. . . . . . 7
β’
((β―βπΉ) =
2 β (π:(0...(β―βπΉ))βΆπ β π:(0...2)βΆπ)) |
140 | 139 | adantl 483 |
. . . . . 6
β’ ((πΊ β USGraph β§
(β―βπΉ) = 2)
β (π:(0...(β―βπΉ))βΆπ β π:(0...2)βΆπ)) |
141 | | f1eq2 6735 |
. . . . . . . . 9
β’
((0..^(β―βπΉ)) = (0..^2) β (πΉ:(0..^(β―βπΉ))β1-1βdom πΌ β πΉ:(0..^2)β1-1βdom πΌ)) |
142 | 130, 141 | syl 17 |
. . . . . . . 8
β’
((β―βπΉ) =
2 β (πΉ:(0..^(β―βπΉ))β1-1βdom πΌ β πΉ:(0..^2)β1-1βdom πΌ)) |
143 | 142 | imbi1d 342 |
. . . . . . 7
β’
((β―βπΉ) =
2 β ((πΉ:(0..^(β―βπΉ))β1-1βdom πΌ β βπ₯ β π βπ¦ β (π β {π₯})βπ§ β (π β {π₯, π¦})(((πβ0) = π₯ β§ (πβ1) = π¦ β§ (πβ2) = π§) β§ ((πΌβ(πΉβ0)) = {π₯, π¦} β§ (πΌβ(πΉβ1)) = {π¦, π§}))) β (πΉ:(0..^2)β1-1βdom πΌ β βπ₯ β π βπ¦ β (π β {π₯})βπ§ β (π β {π₯, π¦})(((πβ0) = π₯ β§ (πβ1) = π¦ β§ (πβ2) = π§) β§ ((πΌβ(πΉβ0)) = {π₯, π¦} β§ (πΌβ(πΉβ1)) = {π¦, π§}))))) |
144 | 143 | adantl 483 |
. . . . . 6
β’ ((πΊ β USGraph β§
(β―βπΉ) = 2)
β ((πΉ:(0..^(β―βπΉ))β1-1βdom πΌ β βπ₯ β π βπ¦ β (π β {π₯})βπ§ β (π β {π₯, π¦})(((πβ0) = π₯ β§ (πβ1) = π¦ β§ (πβ2) = π§) β§ ((πΌβ(πΉβ0)) = {π₯, π¦} β§ (πΌβ(πΉβ1)) = {π¦, π§}))) β (πΉ:(0..^2)β1-1βdom πΌ β βπ₯ β π βπ¦ β (π β {π₯})βπ§ β (π β {π₯, π¦})(((πβ0) = π₯ β§ (πβ1) = π¦ β§ (πβ2) = π§) β§ ((πΌβ(πΉβ0)) = {π₯, π¦} β§ (πΌβ(πΉβ1)) = {π¦, π§}))))) |
145 | 140, 144 | imbi12d 345 |
. . . . 5
β’ ((πΊ β USGraph β§
(β―βπΉ) = 2)
β ((π:(0...(β―βπΉ))βΆπ β (πΉ:(0..^(β―βπΉ))β1-1βdom πΌ β βπ₯ β π βπ¦ β (π β {π₯})βπ§ β (π β {π₯, π¦})(((πβ0) = π₯ β§ (πβ1) = π¦ β§ (πβ2) = π§) β§ ((πΌβ(πΉβ0)) = {π₯, π¦} β§ (πΌβ(πΉβ1)) = {π¦, π§})))) β (π:(0...2)βΆπ β (πΉ:(0..^2)β1-1βdom πΌ β βπ₯ β π βπ¦ β (π β {π₯})βπ§ β (π β {π₯, π¦})(((πβ0) = π₯ β§ (πβ1) = π¦ β§ (πβ2) = π§) β§ ((πΌβ(πΉβ0)) = {π₯, π¦} β§ (πΌβ(πΉβ1)) = {π¦, π§})))))) |
146 | 129, 137,
145 | 3imtr4d 294 |
. . . 4
β’ ((πΊ β USGraph β§
(β―βπΉ) = 2)
β (βπ β
(0..^(β―βπΉ))(πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))} β (π:(0...(β―βπΉ))βΆπ β (πΉ:(0..^(β―βπΉ))β1-1βdom πΌ β βπ₯ β π βπ¦ β (π β {π₯})βπ§ β (π β {π₯, π¦})(((πβ0) = π₯ β§ (πβ1) = π¦ β§ (πβ2) = π§) β§ ((πΌβ(πΉβ0)) = {π₯, π¦} β§ (πΌβ(πΉβ1)) = {π¦, π§})))))) |
147 | 146 | com14 96 |
. . 3
β’ (πΉ:(0..^(β―βπΉ))β1-1βdom πΌ β (βπ β (0..^(β―βπΉ))(πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))} β (π:(0...(β―βπΉ))βΆπ β ((πΊ β USGraph β§ (β―βπΉ) = 2) β βπ₯ β π βπ¦ β (π β {π₯})βπ§ β (π β {π₯, π¦})(((πβ0) = π₯ β§ (πβ1) = π¦ β§ (πβ2) = π§) β§ ((πΌβ(πΉβ0)) = {π₯, π¦} β§ (πΌβ(πΉβ1)) = {π¦, π§})))))) |
148 | 147 | com23 86 |
. 2
β’ (πΉ:(0..^(β―βπΉ))β1-1βdom πΌ β (π:(0...(β―βπΉ))βΆπ β (βπ β (0..^(β―βπΉ))(πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))} β ((πΊ β USGraph β§ (β―βπΉ) = 2) β βπ₯ β π βπ¦ β (π β {π₯})βπ§ β (π β {π₯, π¦})(((πβ0) = π₯ β§ (πβ1) = π¦ β§ (πβ2) = π§) β§ ((πΌβ(πΉβ0)) = {π₯, π¦} β§ (πΌβ(πΉβ1)) = {π¦, π§})))))) |
149 | 148 | 3imp 1112 |
1
β’ ((πΉ:(0..^(β―βπΉ))β1-1βdom πΌ β§ π:(0...(β―βπΉ))βΆπ β§ βπ β (0..^(β―βπΉ))(πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))}) β ((πΊ β USGraph β§ (β―βπΉ) = 2) β βπ₯ β π βπ¦ β (π β {π₯})βπ§ β (π β {π₯, π¦})(((πβ0) = π₯ β§ (πβ1) = π¦ β§ (πβ2) = π§) β§ ((πΌβ(πΉβ0)) = {π₯, π¦} β§ (πΌβ(πΉβ1)) = {π¦, π§})))) |