Step | Hyp | Ref
| Expression |
1 | | s2cl 14794 |
. . 3
β’ ((π β π β§ π β π) β β¨βππββ© β Word π) |
2 | 1 | 3adant3 1132 |
. 2
β’ ((π β π β§ π β π β§ {π, π} β πΈ) β β¨βππββ© β Word π) |
3 | | s2len 14805 |
. . . 4
β’
(β―ββ¨βππββ©) = 2 |
4 | 3 | a1i 11 |
. . 3
β’ ((π β π β§ π β π β§ {π, π} β πΈ) β (β―ββ¨βππββ©) = 2) |
5 | | s2fv0 14803 |
. . . . . . . 8
β’ (π β π β (β¨βππββ©β0) = π) |
6 | 5 | adantr 481 |
. . . . . . 7
β’ ((π β π β§ π β π) β (β¨βππββ©β0) = π) |
7 | | s2fv1 14804 |
. . . . . . . 8
β’ (π β π β (β¨βππββ©β1) = π) |
8 | 7 | adantl 482 |
. . . . . . 7
β’ ((π β π β§ π β π) β (β¨βππββ©β1) = π) |
9 | 6, 8 | preq12d 4722 |
. . . . . 6
β’ ((π β π β§ π β π) β {(β¨βππββ©β0), (β¨βππββ©β1)} = {π, π}) |
10 | 9 | eqcomd 2737 |
. . . . 5
β’ ((π β π β§ π β π) β {π, π} = {(β¨βππββ©β0), (β¨βππββ©β1)}) |
11 | 10 | eleq1d 2817 |
. . . 4
β’ ((π β π β§ π β π) β ({π, π} β πΈ β {(β¨βππββ©β0), (β¨βππββ©β1)} β πΈ)) |
12 | 11 | biimp3a 1469 |
. . 3
β’ ((π β π β§ π β π β§ {π, π} β πΈ) β {(β¨βππββ©β0), (β¨βππββ©β1)} β πΈ) |
13 | 6 | 3adant3 1132 |
. . 3
β’ ((π β π β§ π β π β§ {π, π} β πΈ) β (β¨βππββ©β0) = π) |
14 | 4, 12, 13 | 3jca 1128 |
. 2
β’ ((π β π β§ π β π β§ {π, π} β πΈ) β ((β―ββ¨βππββ©) = 2 β§
{(β¨βππββ©β0),
(β¨βππββ©β1)} β
πΈ β§ (β¨βππββ©β0) = π)) |
15 | | fveqeq2 6871 |
. . . 4
β’ (π€ = β¨βππββ© β ((β―βπ€) = 2 β
(β―ββ¨βππββ©) = 2)) |
16 | | fveq1 6861 |
. . . . . 6
β’ (π€ = β¨βππββ© β (π€β0) = (β¨βππββ©β0)) |
17 | | fveq1 6861 |
. . . . . 6
β’ (π€ = β¨βππββ© β (π€β1) = (β¨βππββ©β1)) |
18 | 16, 17 | preq12d 4722 |
. . . . 5
β’ (π€ = β¨βππββ© β {(π€β0), (π€β1)} = {(β¨βππββ©β0), (β¨βππββ©β1)}) |
19 | 18 | eleq1d 2817 |
. . . 4
β’ (π€ = β¨βππββ© β ({(π€β0), (π€β1)} β πΈ β {(β¨βππββ©β0), (β¨βππββ©β1)} β πΈ)) |
20 | 16 | eqeq1d 2733 |
. . . 4
β’ (π€ = β¨βππββ© β ((π€β0) = π β (β¨βππββ©β0) = π)) |
21 | 15, 19, 20 | 3anbi123d 1436 |
. . 3
β’ (π€ = β¨βππββ© β (((β―βπ€) = 2 β§ {(π€β0), (π€β1)} β πΈ β§ (π€β0) = π) β ((β―ββ¨βππββ©) = 2 β§
{(β¨βππββ©β0),
(β¨βππββ©β1)} β
πΈ β§ (β¨βππββ©β0) = π))) |
22 | | clwwlknon2.c |
. . . 4
β’ πΆ = (ClWWalksNOnβπΊ) |
23 | | clwwlknon2x.v |
. . . 4
β’ π = (VtxβπΊ) |
24 | | clwwlknon2x.e |
. . . 4
β’ πΈ = (EdgβπΊ) |
25 | 22, 23, 24 | clwwlknon2x 29144 |
. . 3
β’ (ππΆ2) = {π€ β Word π β£ ((β―βπ€) = 2 β§ {(π€β0), (π€β1)} β πΈ β§ (π€β0) = π)} |
26 | 21, 25 | elrab2 3666 |
. 2
β’
(β¨βππββ© β (ππΆ2) β (β¨βππββ© β Word π β§ ((β―ββ¨βππββ©) = 2 β§
{(β¨βππββ©β0),
(β¨βππββ©β1)} β
πΈ β§ (β¨βππββ©β0) = π))) |
27 | 2, 14, 26 | sylanbrc 583 |
1
β’ ((π β π β§ π β π β§ {π, π} β πΈ) β β¨βππββ© β (ππΆ2)) |