Step | Hyp | Ref
| Expression |
1 | | ax-5 1914 |
. . . . . . 7
β’ (π β dom πΌ β βπ π β dom πΌ) |
2 | | alral 3076 |
. . . . . . 7
β’
(βπ π β dom πΌ β βπ β dom πΌ π β dom πΌ) |
3 | 1, 2 | syl 17 |
. . . . . 6
β’ (π β dom πΌ β βπ β dom πΌ π β dom πΌ) |
4 | | r19.29 3115 |
. . . . . 6
β’
((βπ β
dom πΌ π β dom πΌ β§ βπ β dom πΌ((πΌβπ) = (πΌβπ) β§ π β π)) β βπ β dom πΌ(π β dom πΌ β§ ((πΌβπ) = (πΌβπ) β§ π β π))) |
5 | 3, 4 | sylan 581 |
. . . . 5
β’ ((π β dom πΌ β§ βπ β dom πΌ((πΌβπ) = (πΌβπ) β§ π β π)) β βπ β dom πΌ(π β dom πΌ β§ ((πΌβπ) = (πΌβπ) β§ π β π))) |
6 | | eqid 2733 |
. . . . . . . . 9
β’
β¨βππββ© =
β¨βππββ© |
7 | | umgr2cycl.1 |
. . . . . . . . 9
β’ πΌ = (iEdgβπΊ) |
8 | | simp1 1137 |
. . . . . . . . 9
β’ ((πΊ β UMGraph β§ π β dom πΌ β§ ((πΌβπ) = (πΌβπ) β§ π β π)) β πΊ β UMGraph) |
9 | | simp2 1138 |
. . . . . . . . 9
β’ ((πΊ β UMGraph β§ π β dom πΌ β§ ((πΌβπ) = (πΌβπ) β§ π β π)) β π β dom πΌ) |
10 | | simp3r 1203 |
. . . . . . . . 9
β’ ((πΊ β UMGraph β§ π β dom πΌ β§ ((πΌβπ) = (πΌβπ) β§ π β π)) β π β π) |
11 | | simp3l 1202 |
. . . . . . . . 9
β’ ((πΊ β UMGraph β§ π β dom πΌ β§ ((πΌβπ) = (πΌβπ) β§ π β π)) β (πΌβπ) = (πΌβπ)) |
12 | 6, 7, 8, 9, 10, 11 | umgr2cycllem 34131 |
. . . . . . . 8
β’ ((πΊ β UMGraph β§ π β dom πΌ β§ ((πΌβπ) = (πΌβπ) β§ π β π)) β βπβ¨βππββ©(CyclesβπΊ)π) |
13 | | s2len 14840 |
. . . . . . . . 9
β’
(β―ββ¨βππββ©) = 2 |
14 | 13 | ax-gen 1798 |
. . . . . . . 8
β’
βπ(β―ββ¨βππββ©) = 2 |
15 | | 19.29r 1878 |
. . . . . . . . 9
β’
((βπβ¨βππββ©(CyclesβπΊ)π β§ βπ(β―ββ¨βππββ©) = 2) β βπ(β¨βππββ©(CyclesβπΊ)π β§ (β―ββ¨βππββ©) = 2)) |
16 | | s2cli 14831 |
. . . . . . . . . . . 12
β’
β¨βππββ© β Word
V |
17 | | breq1 5152 |
. . . . . . . . . . . . . 14
β’ (π = β¨βππββ© β (π(CyclesβπΊ)π β β¨βππββ©(CyclesβπΊ)π)) |
18 | | fveqeq2 6901 |
. . . . . . . . . . . . . 14
β’ (π = β¨βππββ© β ((β―βπ) = 2 β
(β―ββ¨βππββ©) = 2)) |
19 | 17, 18 | anbi12d 632 |
. . . . . . . . . . . . 13
β’ (π = β¨βππββ© β ((π(CyclesβπΊ)π β§ (β―βπ) = 2) β (β¨βππββ©(CyclesβπΊ)π β§ (β―ββ¨βππββ©) = 2))) |
20 | 19 | rspcev 3613 |
. . . . . . . . . . . 12
β’
((β¨βππββ© β Word V β§
(β¨βππββ©(CyclesβπΊ)π β§ (β―ββ¨βππββ©) = 2)) β βπ β Word V(π(CyclesβπΊ)π β§ (β―βπ) = 2)) |
21 | 16, 20 | mpan 689 |
. . . . . . . . . . 11
β’
((β¨βππββ©(CyclesβπΊ)π β§ (β―ββ¨βππββ©) = 2) β βπ β Word V(π(CyclesβπΊ)π β§ (β―βπ) = 2)) |
22 | | rexex 3077 |
. . . . . . . . . . 11
β’
(βπ β
Word V(π(CyclesβπΊ)π β§ (β―βπ) = 2) β βπ(π(CyclesβπΊ)π β§ (β―βπ) = 2)) |
23 | 21, 22 | syl 17 |
. . . . . . . . . 10
β’
((β¨βππββ©(CyclesβπΊ)π β§ (β―ββ¨βππββ©) = 2) β βπ(π(CyclesβπΊ)π β§ (β―βπ) = 2)) |
24 | 23 | eximi 1838 |
. . . . . . . . 9
β’
(βπ(β¨βππββ©(CyclesβπΊ)π β§ (β―ββ¨βππββ©) = 2) β βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 2)) |
25 | | excomim 2164 |
. . . . . . . . 9
β’
(βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 2) β βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 2)) |
26 | 15, 24, 25 | 3syl 18 |
. . . . . . . 8
β’
((βπβ¨βππββ©(CyclesβπΊ)π β§ βπ(β―ββ¨βππββ©) = 2) β βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 2)) |
27 | 12, 14, 26 | sylancl 587 |
. . . . . . 7
β’ ((πΊ β UMGraph β§ π β dom πΌ β§ ((πΌβπ) = (πΌβπ) β§ π β π)) β βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 2)) |
28 | 27 | 3expib 1123 |
. . . . . 6
β’ (πΊ β UMGraph β ((π β dom πΌ β§ ((πΌβπ) = (πΌβπ) β§ π β π)) β βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 2))) |
29 | 28 | rexlimdvw 3161 |
. . . . 5
β’ (πΊ β UMGraph β
(βπ β dom πΌ(π β dom πΌ β§ ((πΌβπ) = (πΌβπ) β§ π β π)) β βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 2))) |
30 | 5, 29 | syl5 34 |
. . . 4
β’ (πΊ β UMGraph β ((π β dom πΌ β§ βπ β dom πΌ((πΌβπ) = (πΌβπ) β§ π β π)) β βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 2))) |
31 | 30 | expd 417 |
. . 3
β’ (πΊ β UMGraph β (π β dom πΌ β (βπ β dom πΌ((πΌβπ) = (πΌβπ) β§ π β π) β βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 2)))) |
32 | 31 | rexlimdv 3154 |
. 2
β’ (πΊ β UMGraph β
(βπ β dom πΌβπ β dom πΌ((πΌβπ) = (πΌβπ) β§ π β π) β βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 2))) |
33 | 32 | imp 408 |
1
β’ ((πΊ β UMGraph β§
βπ β dom πΌβπ β dom πΌ((πΌβπ) = (πΌβπ) β§ π β π)) β βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 2)) |