Step | Hyp | Ref
| Expression |
1 | | ovexd 7397 |
. . . . . 6
β’ (((πΊ β FriendGraph β§ (π₯ β π β§ π¦ β (π β {π₯}))) β§ π¦ β (πΊ NeighbVtx π₯)) β (πΊ NeighbVtx π₯) β V) |
2 | | frgrncvvdeq.v |
. . . . . . 7
β’ π = (VtxβπΊ) |
3 | | eqid 2737 |
. . . . . . 7
β’
(EdgβπΊ) =
(EdgβπΊ) |
4 | | eqid 2737 |
. . . . . . 7
β’ (πΊ NeighbVtx π₯) = (πΊ NeighbVtx π₯) |
5 | | eqid 2737 |
. . . . . . 7
β’ (πΊ NeighbVtx π¦) = (πΊ NeighbVtx π¦) |
6 | | simpl 484 |
. . . . . . . 8
β’ ((π₯ β π β§ π¦ β (π β {π₯})) β π₯ β π) |
7 | 6 | ad2antlr 726 |
. . . . . . 7
β’ (((πΊ β FriendGraph β§ (π₯ β π β§ π¦ β (π β {π₯}))) β§ π¦ β (πΊ NeighbVtx π₯)) β π₯ β π) |
8 | | eldifi 4091 |
. . . . . . . . 9
β’ (π¦ β (π β {π₯}) β π¦ β π) |
9 | 8 | adantl 483 |
. . . . . . . 8
β’ ((π₯ β π β§ π¦ β (π β {π₯})) β π¦ β π) |
10 | 9 | ad2antlr 726 |
. . . . . . 7
β’ (((πΊ β FriendGraph β§ (π₯ β π β§ π¦ β (π β {π₯}))) β§ π¦ β (πΊ NeighbVtx π₯)) β π¦ β π) |
11 | | eldif 3925 |
. . . . . . . . . 10
β’ (π¦ β (π β {π₯}) β (π¦ β π β§ Β¬ π¦ β {π₯})) |
12 | | velsn 4607 |
. . . . . . . . . . . . 13
β’ (π¦ β {π₯} β π¦ = π₯) |
13 | 12 | biimpri 227 |
. . . . . . . . . . . 12
β’ (π¦ = π₯ β π¦ β {π₯}) |
14 | 13 | equcoms 2024 |
. . . . . . . . . . 11
β’ (π₯ = π¦ β π¦ β {π₯}) |
15 | 14 | necon3bi 2971 |
. . . . . . . . . 10
β’ (Β¬
π¦ β {π₯} β π₯ β π¦) |
16 | 11, 15 | simplbiim 506 |
. . . . . . . . 9
β’ (π¦ β (π β {π₯}) β π₯ β π¦) |
17 | 16 | adantl 483 |
. . . . . . . 8
β’ ((π₯ β π β§ π¦ β (π β {π₯})) β π₯ β π¦) |
18 | 17 | ad2antlr 726 |
. . . . . . 7
β’ (((πΊ β FriendGraph β§ (π₯ β π β§ π¦ β (π β {π₯}))) β§ π¦ β (πΊ NeighbVtx π₯)) β π₯ β π¦) |
19 | | simpr 486 |
. . . . . . 7
β’ (((πΊ β FriendGraph β§ (π₯ β π β§ π¦ β (π β {π₯}))) β§ π¦ β (πΊ NeighbVtx π₯)) β π¦ β (πΊ NeighbVtx π₯)) |
20 | | simpl 484 |
. . . . . . . 8
β’ ((πΊ β FriendGraph β§ (π₯ β π β§ π¦ β (π β {π₯}))) β πΊ β FriendGraph ) |
21 | 20 | adantr 482 |
. . . . . . 7
β’ (((πΊ β FriendGraph β§ (π₯ β π β§ π¦ β (π β {π₯}))) β§ π¦ β (πΊ NeighbVtx π₯)) β πΊ β FriendGraph ) |
22 | | eqid 2737 |
. . . . . . 7
β’ (π β (πΊ NeighbVtx π₯) β¦ (β©π β (πΊ NeighbVtx π¦){π, π} β (EdgβπΊ))) = (π β (πΊ NeighbVtx π₯) β¦ (β©π β (πΊ NeighbVtx π¦){π, π} β (EdgβπΊ))) |
23 | 2, 3, 4, 5, 7, 10,
18, 19, 21, 22 | frgrncvvdeqlem10 29294 |
. . . . . 6
β’ (((πΊ β FriendGraph β§ (π₯ β π β§ π¦ β (π β {π₯}))) β§ π¦ β (πΊ NeighbVtx π₯)) β (π β (πΊ NeighbVtx π₯) β¦ (β©π β (πΊ NeighbVtx π¦){π, π} β (EdgβπΊ))):(πΊ NeighbVtx π₯)β1-1-ontoβ(πΊ NeighbVtx π¦)) |
24 | 1, 23 | hasheqf1od 14260 |
. . . . 5
β’ (((πΊ β FriendGraph β§ (π₯ β π β§ π¦ β (π β {π₯}))) β§ π¦ β (πΊ NeighbVtx π₯)) β (β―β(πΊ NeighbVtx π₯)) = (β―β(πΊ NeighbVtx π¦))) |
25 | | frgrusgr 29247 |
. . . . . . . 8
β’ (πΊ β FriendGraph β πΊ β
USGraph) |
26 | 25, 6 | anim12i 614 |
. . . . . . 7
β’ ((πΊ β FriendGraph β§ (π₯ β π β§ π¦ β (π β {π₯}))) β (πΊ β USGraph β§ π₯ β π)) |
27 | 26 | adantr 482 |
. . . . . 6
β’ (((πΊ β FriendGraph β§ (π₯ β π β§ π¦ β (π β {π₯}))) β§ π¦ β (πΊ NeighbVtx π₯)) β (πΊ β USGraph β§ π₯ β π)) |
28 | 2 | hashnbusgrvd 28518 |
. . . . . 6
β’ ((πΊ β USGraph β§ π₯ β π) β (β―β(πΊ NeighbVtx π₯)) = ((VtxDegβπΊ)βπ₯)) |
29 | 27, 28 | syl 17 |
. . . . 5
β’ (((πΊ β FriendGraph β§ (π₯ β π β§ π¦ β (π β {π₯}))) β§ π¦ β (πΊ NeighbVtx π₯)) β (β―β(πΊ NeighbVtx π₯)) = ((VtxDegβπΊ)βπ₯)) |
30 | 25, 9 | anim12i 614 |
. . . . . . 7
β’ ((πΊ β FriendGraph β§ (π₯ β π β§ π¦ β (π β {π₯}))) β (πΊ β USGraph β§ π¦ β π)) |
31 | 30 | adantr 482 |
. . . . . 6
β’ (((πΊ β FriendGraph β§ (π₯ β π β§ π¦ β (π β {π₯}))) β§ π¦ β (πΊ NeighbVtx π₯)) β (πΊ β USGraph β§ π¦ β π)) |
32 | 2 | hashnbusgrvd 28518 |
. . . . . 6
β’ ((πΊ β USGraph β§ π¦ β π) β (β―β(πΊ NeighbVtx π¦)) = ((VtxDegβπΊ)βπ¦)) |
33 | 31, 32 | syl 17 |
. . . . 5
β’ (((πΊ β FriendGraph β§ (π₯ β π β§ π¦ β (π β {π₯}))) β§ π¦ β (πΊ NeighbVtx π₯)) β (β―β(πΊ NeighbVtx π¦)) = ((VtxDegβπΊ)βπ¦)) |
34 | 24, 29, 33 | 3eqtr3d 2785 |
. . . 4
β’ (((πΊ β FriendGraph β§ (π₯ β π β§ π¦ β (π β {π₯}))) β§ π¦ β (πΊ NeighbVtx π₯)) β ((VtxDegβπΊ)βπ₯) = ((VtxDegβπΊ)βπ¦)) |
35 | | frgrncvvdeq.d |
. . . . 5
β’ π· = (VtxDegβπΊ) |
36 | 35 | fveq1i 6848 |
. . . 4
β’ (π·βπ₯) = ((VtxDegβπΊ)βπ₯) |
37 | 35 | fveq1i 6848 |
. . . 4
β’ (π·βπ¦) = ((VtxDegβπΊ)βπ¦) |
38 | 34, 36, 37 | 3eqtr4g 2802 |
. . 3
β’ (((πΊ β FriendGraph β§ (π₯ β π β§ π¦ β (π β {π₯}))) β§ π¦ β (πΊ NeighbVtx π₯)) β (π·βπ₯) = (π·βπ¦)) |
39 | 38 | ex 414 |
. 2
β’ ((πΊ β FriendGraph β§ (π₯ β π β§ π¦ β (π β {π₯}))) β (π¦ β (πΊ NeighbVtx π₯) β (π·βπ₯) = (π·βπ¦))) |
40 | 39 | ralrimivva 3198 |
1
β’ (πΊ β FriendGraph β
βπ₯ β π βπ¦ β (π β {π₯})(π¦ β (πΊ NeighbVtx π₯) β (π·βπ₯) = (π·βπ¦))) |