Step | Hyp | Ref
| Expression |
1 | | umgrupgr 28057 |
. . . . . 6
β’ (πΊ β UMGraph β πΊ β
UPGraph) |
2 | 1 | adantr 482 |
. . . . 5
β’ ((πΊ β UMGraph β§ (π(CyclesβπΊ)π β§ (β―βπ) = 3)) β πΊ β UPGraph) |
3 | | simpl 484 |
. . . . . 6
β’ ((π(CyclesβπΊ)π β§ (β―βπ) = 3) β π(CyclesβπΊ)π) |
4 | 3 | adantl 483 |
. . . . 5
β’ ((πΊ β UMGraph β§ (π(CyclesβπΊ)π β§ (β―βπ) = 3)) β π(CyclesβπΊ)π) |
5 | | simpr 486 |
. . . . . 6
β’ ((π(CyclesβπΊ)π β§ (β―βπ) = 3) β (β―βπ) = 3) |
6 | 5 | adantl 483 |
. . . . 5
β’ ((πΊ β UMGraph β§ (π(CyclesβπΊ)π β§ (β―βπ) = 3)) β (β―βπ) = 3) |
7 | | uhgr3cyclex.e |
. . . . . . 7
β’ πΈ = (EdgβπΊ) |
8 | | uhgr3cyclex.v |
. . . . . . 7
β’ π = (VtxβπΊ) |
9 | 7, 8 | upgr3v3e3cycl 29127 |
. . . . . 6
β’ ((πΊ β UPGraph β§ π(CyclesβπΊ)π β§ (β―βπ) = 3) β βπ β π βπ β π βπ β π (({π, π} β πΈ β§ {π, π} β πΈ β§ {π, π} β πΈ) β§ (π β π β§ π β π β§ π β π))) |
10 | | simpl 484 |
. . . . . . . . 9
β’ ((({π, π} β πΈ β§ {π, π} β πΈ β§ {π, π} β πΈ) β§ (π β π β§ π β π β§ π β π)) β ({π, π} β πΈ β§ {π, π} β πΈ β§ {π, π} β πΈ)) |
11 | 10 | reximi 3088 |
. . . . . . . 8
β’
(βπ β
π (({π, π} β πΈ β§ {π, π} β πΈ β§ {π, π} β πΈ) β§ (π β π β§ π β π β§ π β π)) β βπ β π ({π, π} β πΈ β§ {π, π} β πΈ β§ {π, π} β πΈ)) |
12 | 11 | reximi 3088 |
. . . . . . 7
β’
(βπ β
π βπ β π (({π, π} β πΈ β§ {π, π} β πΈ β§ {π, π} β πΈ) β§ (π β π β§ π β π β§ π β π)) β βπ β π βπ β π ({π, π} β πΈ β§ {π, π} β πΈ β§ {π, π} β πΈ)) |
13 | 12 | reximi 3088 |
. . . . . 6
β’
(βπ β
π βπ β π βπ β π (({π, π} β πΈ β§ {π, π} β πΈ β§ {π, π} β πΈ) β§ (π β π β§ π β π β§ π β π)) β βπ β π βπ β π βπ β π ({π, π} β πΈ β§ {π, π} β πΈ β§ {π, π} β πΈ)) |
14 | 9, 13 | syl 17 |
. . . . 5
β’ ((πΊ β UPGraph β§ π(CyclesβπΊ)π β§ (β―βπ) = 3) β βπ β π βπ β π βπ β π ({π, π} β πΈ β§ {π, π} β πΈ β§ {π, π} β πΈ)) |
15 | 2, 4, 6, 14 | syl3anc 1372 |
. . . 4
β’ ((πΊ β UMGraph β§ (π(CyclesβπΊ)π β§ (β―βπ) = 3)) β βπ β π βπ β π βπ β π ({π, π} β πΈ β§ {π, π} β πΈ β§ {π, π} β πΈ)) |
16 | 15 | ex 414 |
. . 3
β’ (πΊ β UMGraph β ((π(CyclesβπΊ)π β§ (β―βπ) = 3) β βπ β π βπ β π βπ β π ({π, π} β πΈ β§ {π, π} β πΈ β§ {π, π} β πΈ))) |
17 | 16 | exlimdvv 1938 |
. 2
β’ (πΊ β UMGraph β
(βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 3) β βπ β π βπ β π βπ β π ({π, π} β πΈ β§ {π, π} β πΈ β§ {π, π} β πΈ))) |
18 | | simplll 774 |
. . . . 5
β’ ((((πΊ β UMGraph β§ (π β π β§ π β π)) β§ π β π) β§ ({π, π} β πΈ β§ {π, π} β πΈ β§ {π, π} β πΈ)) β πΊ β UMGraph) |
19 | | df-3an 1090 |
. . . . . . 7
β’ ((π β π β§ π β π β§ π β π) β ((π β π β§ π β π) β§ π β π)) |
20 | 19 | biimpri 227 |
. . . . . 6
β’ (((π β π β§ π β π) β§ π β π) β (π β π β§ π β π β§ π β π)) |
21 | 20 | ad4ant23 752 |
. . . . 5
β’ ((((πΊ β UMGraph β§ (π β π β§ π β π)) β§ π β π) β§ ({π, π} β πΈ β§ {π, π} β πΈ β§ {π, π} β πΈ)) β (π β π β§ π β π β§ π β π)) |
22 | | simpr 486 |
. . . . 5
β’ ((((πΊ β UMGraph β§ (π β π β§ π β π)) β§ π β π) β§ ({π, π} β πΈ β§ {π, π} β πΈ β§ {π, π} β πΈ)) β ({π, π} β πΈ β§ {π, π} β πΈ β§ {π, π} β πΈ)) |
23 | 8, 7 | umgr3cyclex 29130 |
. . . . . 6
β’ ((πΊ β UMGraph β§ (π β π β§ π β π β§ π β π) β§ ({π, π} β πΈ β§ {π, π} β πΈ β§ {π, π} β πΈ)) β βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 3 β§ (πβ0) = π)) |
24 | | 3simpa 1149 |
. . . . . . 7
β’ ((π(CyclesβπΊ)π β§ (β―βπ) = 3 β§ (πβ0) = π) β (π(CyclesβπΊ)π β§ (β―βπ) = 3)) |
25 | 24 | 2eximi 1839 |
. . . . . 6
β’
(βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 3 β§ (πβ0) = π) β βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 3)) |
26 | 23, 25 | syl 17 |
. . . . 5
β’ ((πΊ β UMGraph β§ (π β π β§ π β π β§ π β π) β§ ({π, π} β πΈ β§ {π, π} β πΈ β§ {π, π} β πΈ)) β βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 3)) |
27 | 18, 21, 22, 26 | syl3anc 1372 |
. . . 4
β’ ((((πΊ β UMGraph β§ (π β π β§ π β π)) β§ π β π) β§ ({π, π} β πΈ β§ {π, π} β πΈ β§ {π, π} β πΈ)) β βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 3)) |
28 | 27 | rexlimdva2 3155 |
. . 3
β’ ((πΊ β UMGraph β§ (π β π β§ π β π)) β (βπ β π ({π, π} β πΈ β§ {π, π} β πΈ β§ {π, π} β πΈ) β βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 3))) |
29 | 28 | rexlimdvva 3206 |
. 2
β’ (πΊ β UMGraph β
(βπ β π βπ β π βπ β π ({π, π} β πΈ β§ {π, π} β πΈ β§ {π, π} β πΈ) β βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 3))) |
30 | 17, 29 | impbid 211 |
1
β’ (πΊ β UMGraph β
(βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 3) β βπ β π βπ β π βπ β π ({π, π} β πΈ β§ {π, π} β πΈ β§ {π, π} β πΈ))) |