Step | Hyp | Ref
| Expression |
1 | | 2pthfrgr.v |
. . 3
β’ π = (VtxβπΊ) |
2 | | eqid 2737 |
. . 3
β’
(EdgβπΊ) =
(EdgβπΊ) |
3 | 1, 2 | 2pthfrgrrn2 29269 |
. 2
β’ (πΊ β FriendGraph β
βπ β π βπ β (π β {π})βπ β π (({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ)) β§ (π β π β§ π β π))) |
4 | | frgrusgr 29247 |
. . . . . . . . . . . 12
β’ (πΊ β FriendGraph β πΊ β
USGraph) |
5 | | usgruhgr 28176 |
. . . . . . . . . . . 12
β’ (πΊ β USGraph β πΊ β
UHGraph) |
6 | 4, 5 | syl 17 |
. . . . . . . . . . 11
β’ (πΊ β FriendGraph β πΊ β
UHGraph) |
7 | 6 | adantr 482 |
. . . . . . . . . 10
β’ ((πΊ β FriendGraph β§ π β π) β πΊ β UHGraph) |
8 | 7 | adantr 482 |
. . . . . . . . 9
β’ (((πΊ β FriendGraph β§ π β π) β§ π β (π β {π})) β πΊ β UHGraph) |
9 | 8 | adantr 482 |
. . . . . . . 8
β’ ((((πΊ β FriendGraph β§ π β π) β§ π β (π β {π})) β§ π β π) β πΊ β UHGraph) |
10 | | simpllr 775 |
. . . . . . . . 9
β’ ((((πΊ β FriendGraph β§ π β π) β§ π β (π β {π})) β§ π β π) β π β π) |
11 | | simpr 486 |
. . . . . . . . 9
β’ ((((πΊ β FriendGraph β§ π β π) β§ π β (π β {π})) β§ π β π) β π β π) |
12 | | eldifi 4091 |
. . . . . . . . . 10
β’ (π β (π β {π}) β π β π) |
13 | 12 | ad2antlr 726 |
. . . . . . . . 9
β’ ((((πΊ β FriendGraph β§ π β π) β§ π β (π β {π})) β§ π β π) β π β π) |
14 | 10, 11, 13 | 3jca 1129 |
. . . . . . . 8
β’ ((((πΊ β FriendGraph β§ π β π) β§ π β (π β {π})) β§ π β π) β (π β π β§ π β π β§ π β π)) |
15 | 9, 14 | jca 513 |
. . . . . . 7
β’ ((((πΊ β FriendGraph β§ π β π) β§ π β (π β {π})) β§ π β π) β (πΊ β UHGraph β§ (π β π β§ π β π β§ π β π))) |
16 | 15 | adantr 482 |
. . . . . 6
β’
(((((πΊ β
FriendGraph β§ π β
π) β§ π β (π β {π})) β§ π β π) β§ (({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ)) β§ (π β π β§ π β π))) β (πΊ β UHGraph β§ (π β π β§ π β π β§ π β π))) |
17 | | simprrl 780 |
. . . . . 6
β’
(((((πΊ β
FriendGraph β§ π β
π) β§ π β (π β {π})) β§ π β π) β§ (({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ)) β§ (π β π β§ π β π))) β π β π) |
18 | | eldifsn 4752 |
. . . . . . . 8
β’ (π β (π β {π}) β (π β π β§ π β π)) |
19 | | necom 2998 |
. . . . . . . . 9
β’ (π β π β π β π) |
20 | 19 | biimpi 215 |
. . . . . . . 8
β’ (π β π β π β π) |
21 | 18, 20 | simplbiim 506 |
. . . . . . 7
β’ (π β (π β {π}) β π β π) |
22 | 21 | ad3antlr 730 |
. . . . . 6
β’
(((((πΊ β
FriendGraph β§ π β
π) β§ π β (π β {π})) β§ π β π) β§ (({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ)) β§ (π β π β§ π β π))) β π β π) |
23 | | simprrr 781 |
. . . . . 6
β’
(((((πΊ β
FriendGraph β§ π β
π) β§ π β (π β {π})) β§ π β π) β§ (({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ)) β§ (π β π β§ π β π))) β π β π) |
24 | | simprl 770 |
. . . . . 6
β’
(((((πΊ β
FriendGraph β§ π β
π) β§ π β (π β {π})) β§ π β π) β§ (({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ)) β§ (π β π β§ π β π))) β ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ))) |
25 | 1, 2 | 2pthon3v 28930 |
. . . . . 6
β’ (((πΊ β UHGraph β§ (π β π β§ π β π β§ π β π)) β§ (π β π β§ π β π β§ π β π) β§ ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ))) β βπβπ(π(π(SPathsOnβπΊ)π)π β§ (β―βπ) = 2)) |
26 | 16, 17, 22, 23, 24, 25 | syl131anc 1384 |
. . . . 5
β’
(((((πΊ β
FriendGraph β§ π β
π) β§ π β (π β {π})) β§ π β π) β§ (({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ)) β§ (π β π β§ π β π))) β βπβπ(π(π(SPathsOnβπΊ)π)π β§ (β―βπ) = 2)) |
27 | 26 | rexlimdva2 3155 |
. . . 4
β’ (((πΊ β FriendGraph β§ π β π) β§ π β (π β {π})) β (βπ β π (({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ)) β§ (π β π β§ π β π)) β βπβπ(π(π(SPathsOnβπΊ)π)π β§ (β―βπ) = 2))) |
28 | 27 | ralimdva 3165 |
. . 3
β’ ((πΊ β FriendGraph β§ π β π) β (βπ β (π β {π})βπ β π (({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ)) β§ (π β π β§ π β π)) β βπ β (π β {π})βπβπ(π(π(SPathsOnβπΊ)π)π β§ (β―βπ) = 2))) |
29 | 28 | ralimdva 3165 |
. 2
β’ (πΊ β FriendGraph β
(βπ β π βπ β (π β {π})βπ β π (({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ)) β§ (π β π β§ π β π)) β βπ β π βπ β (π β {π})βπβπ(π(π(SPathsOnβπΊ)π)π β§ (β―βπ) = 2))) |
30 | 3, 29 | mpd 15 |
1
β’ (πΊ β FriendGraph β
βπ β π βπ β (π β {π})βπβπ(π(π(SPathsOnβπΊ)π)π β§ (β―βπ) = 2)) |