Step | Hyp | Ref
| Expression |
1 | | umgr2cycllem.3 |
. . 3
β’ (π β πΊ β UMGraph) |
2 | | umgruhgr 28364 |
. . . . 5
β’ (πΊ β UMGraph β πΊ β
UHGraph) |
3 | | umgr2cycllem.2 |
. . . . . 6
β’ πΌ = (iEdgβπΊ) |
4 | 3 | uhgrfun 28326 |
. . . . 5
β’ (πΊ β UHGraph β Fun πΌ) |
5 | 1, 2, 4 | 3syl 18 |
. . . 4
β’ (π β Fun πΌ) |
6 | | umgr2cycllem.4 |
. . . 4
β’ (π β π½ β dom πΌ) |
7 | 3 | iedgedg 28310 |
. . . 4
β’ ((Fun
πΌ β§ π½ β dom πΌ) β (πΌβπ½) β (EdgβπΊ)) |
8 | 5, 6, 7 | syl2anc 585 |
. . 3
β’ (π β (πΌβπ½) β (EdgβπΊ)) |
9 | | eqid 2733 |
. . . 4
β’
(VtxβπΊ) =
(VtxβπΊ) |
10 | | eqid 2733 |
. . . 4
β’
(EdgβπΊ) =
(EdgβπΊ) |
11 | 9, 10 | umgredg 28398 |
. . 3
β’ ((πΊ β UMGraph β§ (πΌβπ½) β (EdgβπΊ)) β βπ β (VtxβπΊ)βπ β (VtxβπΊ)(π β π β§ (πΌβπ½) = {π, π})) |
12 | 1, 8, 11 | syl2anc 585 |
. 2
β’ (π β βπ β (VtxβπΊ)βπ β (VtxβπΊ)(π β π β§ (πΌβπ½) = {π, π})) |
13 | | ax-5 1914 |
. . . . . . 7
β’ (π β (VtxβπΊ) β βπ π β (VtxβπΊ)) |
14 | | alral 3076 |
. . . . . . 7
β’
(βπ π β (VtxβπΊ) β βπ β (VtxβπΊ)π β (VtxβπΊ)) |
15 | 13, 14 | syl 17 |
. . . . . 6
β’ (π β (VtxβπΊ) β βπ β (VtxβπΊ)π β (VtxβπΊ)) |
16 | | r19.29 3115 |
. . . . . 6
β’
((βπ β
(VtxβπΊ)π β (VtxβπΊ) β§ βπ β (VtxβπΊ)(π β π β§ (πΌβπ½) = {π, π})) β βπ β (VtxβπΊ)(π β (VtxβπΊ) β§ (π β π β§ (πΌβπ½) = {π, π}))) |
17 | 15, 16 | sylan 581 |
. . . . 5
β’ ((π β (VtxβπΊ) β§ βπ β (VtxβπΊ)(π β π β§ (πΌβπ½) = {π, π})) β βπ β (VtxβπΊ)(π β (VtxβπΊ) β§ (π β π β§ (πΌβπ½) = {π, π}))) |
18 | | eqid 2733 |
. . . . . . . . . . . 12
β’
β¨βπππββ© = β¨βπππββ© |
19 | | umgr2cycllem.1 |
. . . . . . . . . . . 12
β’ πΉ = β¨βπ½πΎββ© |
20 | | simp2 1138 |
. . . . . . . . . . . 12
β’ ((π β§ (π β (VtxβπΊ) β§ π β (VtxβπΊ)) β§ (π β π β§ (πΌβπ½) = {π, π})) β (π β (VtxβπΊ) β§ π β (VtxβπΊ))) |
21 | | simp3l 1202 |
. . . . . . . . . . . 12
β’ ((π β§ (π β (VtxβπΊ) β§ π β (VtxβπΊ)) β§ (π β π β§ (πΌβπ½) = {π, π})) β π β π) |
22 | | eqimss2 4042 |
. . . . . . . . . . . . . . 15
β’ ((πΌβπ½) = {π, π} β {π, π} β (πΌβπ½)) |
23 | 22 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π β π β§ (πΌβπ½) = {π, π}) β {π, π} β (πΌβπ½)) |
24 | 23 | 3ad2ant3 1136 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β (VtxβπΊ) β§ π β (VtxβπΊ)) β§ (π β π β§ (πΌβπ½) = {π, π})) β {π, π} β (πΌβπ½)) |
25 | | umgr2cycllem.6 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (πΌβπ½) = (πΌβπΎ)) |
26 | 25 | sseq2d 4015 |
. . . . . . . . . . . . . . . . 17
β’ (π β ({π, π} β (πΌβπ½) β {π, π} β (πΌβπΎ))) |
27 | 22, 26 | imbitrid 243 |
. . . . . . . . . . . . . . . 16
β’ (π β ((πΌβπ½) = {π, π} β {π, π} β (πΌβπΎ))) |
28 | 27 | adantld 492 |
. . . . . . . . . . . . . . 15
β’ (π β ((π β π β§ (πΌβπ½) = {π, π}) β {π, π} β (πΌβπΎ))) |
29 | 28 | adantld 492 |
. . . . . . . . . . . . . 14
β’ (π β (((π β (VtxβπΊ) β§ π β (VtxβπΊ)) β§ (π β π β§ (πΌβπ½) = {π, π})) β {π, π} β (πΌβπΎ))) |
30 | 29 | 3impib 1117 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β (VtxβπΊ) β§ π β (VtxβπΊ)) β§ (π β π β§ (πΌβπ½) = {π, π})) β {π, π} β (πΌβπΎ)) |
31 | 24, 30 | jca 513 |
. . . . . . . . . . . 12
β’ ((π β§ (π β (VtxβπΊ) β§ π β (VtxβπΊ)) β§ (π β π β§ (πΌβπ½) = {π, π})) β ({π, π} β (πΌβπ½) β§ {π, π} β (πΌβπΎ))) |
32 | | umgr2cycllem.5 |
. . . . . . . . . . . . 13
β’ (π β π½ β πΎ) |
33 | 32 | 3ad2ant1 1134 |
. . . . . . . . . . . 12
β’ ((π β§ (π β (VtxβπΊ) β§ π β (VtxβπΊ)) β§ (π β π β§ (πΌβπ½) = {π, π})) β π½ β πΎ) |
34 | 18, 19, 20, 21, 31, 9, 3, 33 | 2cycl2d 34130 |
. . . . . . . . . . 11
β’ ((π β§ (π β (VtxβπΊ) β§ π β (VtxβπΊ)) β§ (π β π β§ (πΌβπ½) = {π, π})) β πΉ(CyclesβπΊ)β¨βπππββ©) |
35 | 34 | 3expib 1123 |
. . . . . . . . . 10
β’ (π β (((π β (VtxβπΊ) β§ π β (VtxβπΊ)) β§ (π β π β§ (πΌβπ½) = {π, π})) β πΉ(CyclesβπΊ)β¨βπππββ©)) |
36 | 35 | exp4c 434 |
. . . . . . . . 9
β’ (π β (π β (VtxβπΊ) β (π β (VtxβπΊ) β ((π β π β§ (πΌβπ½) = {π, π}) β πΉ(CyclesβπΊ)β¨βπππββ©)))) |
37 | 36 | com23 86 |
. . . . . . . 8
β’ (π β (π β (VtxβπΊ) β (π β (VtxβπΊ) β ((π β π β§ (πΌβπ½) = {π, π}) β πΉ(CyclesβπΊ)β¨βπππββ©)))) |
38 | 37 | imp4a 424 |
. . . . . . 7
β’ (π β (π β (VtxβπΊ) β ((π β (VtxβπΊ) β§ (π β π β§ (πΌβπ½) = {π, π})) β πΉ(CyclesβπΊ)β¨βπππββ©))) |
39 | | s3cli 14832 |
. . . . . . . . 9
β’
β¨βπππββ© β Word V |
40 | | breq2 5153 |
. . . . . . . . . 10
β’ (π = β¨βπππββ© β (πΉ(CyclesβπΊ)π β πΉ(CyclesβπΊ)β¨βπππββ©)) |
41 | 40 | rspcev 3613 |
. . . . . . . . 9
β’
((β¨βπππββ© β Word V β§ πΉ(CyclesβπΊ)β¨βπππββ©) β βπ β Word VπΉ(CyclesβπΊ)π) |
42 | 39, 41 | mpan 689 |
. . . . . . . 8
β’ (πΉ(CyclesβπΊ)β¨βπππββ© β βπ β Word VπΉ(CyclesβπΊ)π) |
43 | | rexex 3077 |
. . . . . . . 8
β’
(βπ β
Word VπΉ(CyclesβπΊ)π β βπ πΉ(CyclesβπΊ)π) |
44 | 42, 43 | syl 17 |
. . . . . . 7
β’ (πΉ(CyclesβπΊ)β¨βπππββ© β βπ πΉ(CyclesβπΊ)π) |
45 | 38, 44 | syl8 76 |
. . . . . 6
β’ (π β (π β (VtxβπΊ) β ((π β (VtxβπΊ) β§ (π β π β§ (πΌβπ½) = {π, π})) β βπ πΉ(CyclesβπΊ)π))) |
46 | 45 | rexlimdv 3154 |
. . . . 5
β’ (π β (βπ β (VtxβπΊ)(π β (VtxβπΊ) β§ (π β π β§ (πΌβπ½) = {π, π})) β βπ πΉ(CyclesβπΊ)π)) |
47 | 17, 46 | syl5 34 |
. . . 4
β’ (π β ((π β (VtxβπΊ) β§ βπ β (VtxβπΊ)(π β π β§ (πΌβπ½) = {π, π})) β βπ πΉ(CyclesβπΊ)π)) |
48 | 47 | expd 417 |
. . 3
β’ (π β (π β (VtxβπΊ) β (βπ β (VtxβπΊ)(π β π β§ (πΌβπ½) = {π, π}) β βπ πΉ(CyclesβπΊ)π))) |
49 | 48 | rexlimdv 3154 |
. 2
β’ (π β (βπ β (VtxβπΊ)βπ β (VtxβπΊ)(π β π β§ (πΌβπ½) = {π, π}) β βπ πΉ(CyclesβπΊ)π)) |
50 | 12, 49 | mpd 15 |
1
β’ (π β βπ πΉ(CyclesβπΊ)π) |