Step | Hyp | Ref
| Expression |
1 | | fveq2 6846 |
. . . . . 6
β’ (π€ = π β (1st βπ€) = (1st βπ)) |
2 | | clwlkclwwlkf.a |
. . . . . 6
β’ π΄ = (1st βπ) |
3 | 1, 2 | eqtr4di 2791 |
. . . . 5
β’ (π€ = π β (1st βπ€) = π΄) |
4 | 3 | fveq2d 6850 |
. . . 4
β’ (π€ = π β (β―β(1st
βπ€)) =
(β―βπ΄)) |
5 | 4 | breq2d 5121 |
. . 3
β’ (π€ = π β (1 β€
(β―β(1st βπ€)) β 1 β€ (β―βπ΄))) |
6 | | clwlkclwwlkf.c |
. . 3
β’ πΆ = {π€ β (ClWalksβπΊ) β£ 1 β€
(β―β(1st βπ€))} |
7 | 5, 6 | elrab2 3652 |
. 2
β’ (π β πΆ β (π β (ClWalksβπΊ) β§ 1 β€ (β―βπ΄))) |
8 | | clwlkwlk 28772 |
. . . 4
β’ (π β (ClWalksβπΊ) β π β (WalksβπΊ)) |
9 | | wlkop 28625 |
. . . . 5
β’ (π β (WalksβπΊ) β π = β¨(1st βπ), (2nd βπ)β©) |
10 | | clwlkclwwlkf.b |
. . . . . . . 8
β’ π΅ = (2nd βπ) |
11 | 2, 10 | opeq12i 4839 |
. . . . . . 7
β’
β¨π΄, π΅β© = β¨(1st
βπ), (2nd
βπ)β© |
12 | 11 | eqeq2i 2746 |
. . . . . 6
β’ (π = β¨π΄, π΅β© β π = β¨(1st βπ), (2nd βπ)β©) |
13 | | eleq1 2822 |
. . . . . . 7
β’ (π = β¨π΄, π΅β© β (π β (ClWalksβπΊ) β β¨π΄, π΅β© β (ClWalksβπΊ))) |
14 | | df-br 5110 |
. . . . . . . 8
β’ (π΄(ClWalksβπΊ)π΅ β β¨π΄, π΅β© β (ClWalksβπΊ)) |
15 | | isclwlk 28770 |
. . . . . . . . 9
β’ (π΄(ClWalksβπΊ)π΅ β (π΄(WalksβπΊ)π΅ β§ (π΅β0) = (π΅β(β―βπ΄)))) |
16 | | wlkcl 28612 |
. . . . . . . . . . . . . . 15
β’ (π΄(WalksβπΊ)π΅ β (β―βπ΄) β
β0) |
17 | | elnnnn0c 12466 |
. . . . . . . . . . . . . . . 16
β’
((β―βπ΄)
β β β ((β―βπ΄) β β0 β§ 1 β€
(β―βπ΄))) |
18 | 17 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (π΄(WalksβπΊ)π΅ β ((β―βπ΄) β β β
((β―βπ΄) β
β0 β§ 1 β€ (β―βπ΄)))) |
19 | 16, 18 | mpbirand 706 |
. . . . . . . . . . . . . 14
β’ (π΄(WalksβπΊ)π΅ β ((β―βπ΄) β β β 1 β€
(β―βπ΄))) |
20 | 19 | bicomd 222 |
. . . . . . . . . . . . 13
β’ (π΄(WalksβπΊ)π΅ β (1 β€ (β―βπ΄) β (β―βπ΄) β
β)) |
21 | 20 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π΄(WalksβπΊ)π΅ β§ (π΅β0) = (π΅β(β―βπ΄))) β (1 β€ (β―βπ΄) β (β―βπ΄) β
β)) |
22 | 21 | pm5.32i 576 |
. . . . . . . . . . 11
β’ (((π΄(WalksβπΊ)π΅ β§ (π΅β0) = (π΅β(β―βπ΄))) β§ 1 β€ (β―βπ΄)) β ((π΄(WalksβπΊ)π΅ β§ (π΅β0) = (π΅β(β―βπ΄))) β§ (β―βπ΄) β β)) |
23 | | df-3an 1090 |
. . . . . . . . . . 11
β’ ((π΄(WalksβπΊ)π΅ β§ (π΅β0) = (π΅β(β―βπ΄)) β§ (β―βπ΄) β β) β ((π΄(WalksβπΊ)π΅ β§ (π΅β0) = (π΅β(β―βπ΄))) β§ (β―βπ΄) β β)) |
24 | 22, 23 | sylbb2 237 |
. . . . . . . . . 10
β’ (((π΄(WalksβπΊ)π΅ β§ (π΅β0) = (π΅β(β―βπ΄))) β§ 1 β€ (β―βπ΄)) β (π΄(WalksβπΊ)π΅ β§ (π΅β0) = (π΅β(β―βπ΄)) β§ (β―βπ΄) β β)) |
25 | 24 | ex 414 |
. . . . . . . . 9
β’ ((π΄(WalksβπΊ)π΅ β§ (π΅β0) = (π΅β(β―βπ΄))) β (1 β€ (β―βπ΄) β (π΄(WalksβπΊ)π΅ β§ (π΅β0) = (π΅β(β―βπ΄)) β§ (β―βπ΄) β β))) |
26 | 15, 25 | sylbi 216 |
. . . . . . . 8
β’ (π΄(ClWalksβπΊ)π΅ β (1 β€ (β―βπ΄) β (π΄(WalksβπΊ)π΅ β§ (π΅β0) = (π΅β(β―βπ΄)) β§ (β―βπ΄) β β))) |
27 | 14, 26 | sylbir 234 |
. . . . . . 7
β’
(β¨π΄, π΅β© β
(ClWalksβπΊ) β (1
β€ (β―βπ΄)
β (π΄(WalksβπΊ)π΅ β§ (π΅β0) = (π΅β(β―βπ΄)) β§ (β―βπ΄) β β))) |
28 | 13, 27 | syl6bi 253 |
. . . . . 6
β’ (π = β¨π΄, π΅β© β (π β (ClWalksβπΊ) β (1 β€ (β―βπ΄) β (π΄(WalksβπΊ)π΅ β§ (π΅β0) = (π΅β(β―βπ΄)) β§ (β―βπ΄) β β)))) |
29 | 12, 28 | sylbir 234 |
. . . . 5
β’ (π = β¨(1st
βπ), (2nd
βπ)β© β
(π β
(ClWalksβπΊ) β (1
β€ (β―βπ΄)
β (π΄(WalksβπΊ)π΅ β§ (π΅β0) = (π΅β(β―βπ΄)) β§ (β―βπ΄) β β)))) |
30 | 9, 29 | syl 17 |
. . . 4
β’ (π β (WalksβπΊ) β (π β (ClWalksβπΊ) β (1 β€ (β―βπ΄) β (π΄(WalksβπΊ)π΅ β§ (π΅β0) = (π΅β(β―βπ΄)) β§ (β―βπ΄) β β)))) |
31 | 8, 30 | mpcom 38 |
. . 3
β’ (π β (ClWalksβπΊ) β (1 β€
(β―βπ΄) β
(π΄(WalksβπΊ)π΅ β§ (π΅β0) = (π΅β(β―βπ΄)) β§ (β―βπ΄) β β))) |
32 | 31 | imp 408 |
. 2
β’ ((π β (ClWalksβπΊ) β§ 1 β€
(β―βπ΄)) β
(π΄(WalksβπΊ)π΅ β§ (π΅β0) = (π΅β(β―βπ΄)) β§ (β―βπ΄) β β)) |
33 | 7, 32 | sylbi 216 |
1
β’ (π β πΆ β (π΄(WalksβπΊ)π΅ β§ (π΅β0) = (π΅β(β―βπ΄)) β§ (β―βπ΄) β β)) |