Step | Hyp | Ref
| Expression |
1 | | 3cyclfrgr.v |
. . 3
β’ π = (VtxβπΊ) |
2 | | eqid 2737 |
. . 3
β’
(EdgβπΊ) =
(EdgβπΊ) |
3 | 1, 2 | 3cyclfrgrrn 29272 |
. 2
β’ ((πΊ β FriendGraph β§ 1 <
(β―βπ)) β
βπ£ β π βπ β π βπ β π ({π£, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ) β§ {π, π£} β (EdgβπΊ))) |
4 | | frgrusgr 29247 |
. . . . . . . 8
β’ (πΊ β FriendGraph β πΊ β
USGraph) |
5 | | usgrumgr 28172 |
. . . . . . . 8
β’ (πΊ β USGraph β πΊ β
UMGraph) |
6 | 4, 5 | syl 17 |
. . . . . . 7
β’ (πΊ β FriendGraph β πΊ β
UMGraph) |
7 | 6 | ad4antr 731 |
. . . . . 6
β’
(((((πΊ β
FriendGraph β§ 1 < (β―βπ)) β§ π£ β π) β§ (π β π β§ π β π)) β§ ({π£, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ) β§ {π, π£} β (EdgβπΊ))) β πΊ β UMGraph) |
8 | | simpr 486 |
. . . . . . . . 9
β’ (((πΊ β FriendGraph β§ 1 <
(β―βπ)) β§
π£ β π) β π£ β π) |
9 | 8 | anim1i 616 |
. . . . . . . 8
β’ ((((πΊ β FriendGraph β§ 1 <
(β―βπ)) β§
π£ β π) β§ (π β π β§ π β π)) β (π£ β π β§ (π β π β§ π β π))) |
10 | | 3anass 1096 |
. . . . . . . 8
β’ ((π£ β π β§ π β π β§ π β π) β (π£ β π β§ (π β π β§ π β π))) |
11 | 9, 10 | sylibr 233 |
. . . . . . 7
β’ ((((πΊ β FriendGraph β§ 1 <
(β―βπ)) β§
π£ β π) β§ (π β π β§ π β π)) β (π£ β π β§ π β π β§ π β π)) |
12 | 11 | adantr 482 |
. . . . . 6
β’
(((((πΊ β
FriendGraph β§ 1 < (β―βπ)) β§ π£ β π) β§ (π β π β§ π β π)) β§ ({π£, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ) β§ {π, π£} β (EdgβπΊ))) β (π£ β π β§ π β π β§ π β π)) |
13 | | simpr 486 |
. . . . . 6
β’
(((((πΊ β
FriendGraph β§ 1 < (β―βπ)) β§ π£ β π) β§ (π β π β§ π β π)) β§ ({π£, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ) β§ {π, π£} β (EdgβπΊ))) β ({π£, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ) β§ {π, π£} β (EdgβπΊ))) |
14 | 1, 2 | umgr3cyclex 29169 |
. . . . . 6
β’ ((πΊ β UMGraph β§ (π£ β π β§ π β π β§ π β π) β§ ({π£, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ) β§ {π, π£} β (EdgβπΊ))) β βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 3 β§ (πβ0) = π£)) |
15 | 7, 12, 13, 14 | syl3anc 1372 |
. . . . 5
β’
(((((πΊ β
FriendGraph β§ 1 < (β―βπ)) β§ π£ β π) β§ (π β π β§ π β π)) β§ ({π£, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ) β§ {π, π£} β (EdgβπΊ))) β βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 3 β§ (πβ0) = π£)) |
16 | 15 | ex 414 |
. . . 4
β’ ((((πΊ β FriendGraph β§ 1 <
(β―βπ)) β§
π£ β π) β§ (π β π β§ π β π)) β (({π£, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ) β§ {π, π£} β (EdgβπΊ)) β βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 3 β§ (πβ0) = π£))) |
17 | 16 | rexlimdvva 3206 |
. . 3
β’ (((πΊ β FriendGraph β§ 1 <
(β―βπ)) β§
π£ β π) β (βπ β π βπ β π ({π£, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ) β§ {π, π£} β (EdgβπΊ)) β βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 3 β§ (πβ0) = π£))) |
18 | 17 | ralimdva 3165 |
. 2
β’ ((πΊ β FriendGraph β§ 1 <
(β―βπ)) β
(βπ£ β π βπ β π βπ β π ({π£, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ) β§ {π, π£} β (EdgβπΊ)) β βπ£ β π βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 3 β§ (πβ0) = π£))) |
19 | 3, 18 | mpd 15 |
1
β’ ((πΊ β FriendGraph β§ 1 <
(β―βπ)) β
βπ£ β π βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 3 β§ (πβ0) = π£)) |