| Step | Hyp | Ref
| Expression |
|---|
| 1 | | ovexd 7446 |
. . . . . 6
β’ (((πΊ β FriendGraph β§ (π₯ β π β§ π¦ β (π β {π₯}))) β§ π¦ β (πΊ NeighbVtx π₯)) β (πΊ NeighbVtx π₯) β V) |
| 2 | | frgrncvvdeq.v |
. . . . . . 7
β’ π = (VtxβπΊ) |
| 3 | | eqid 2730 |
. . . . . . 7
β’
(EdgβπΊ) =
(EdgβπΊ) |
| 4 | | eqid 2730 |
. . . . . . 7
β’ (πΊ NeighbVtx π₯) = (πΊ NeighbVtx π₯) |
| 5 | | eqid 2730 |
. . . . . . 7
β’ (πΊ NeighbVtx π¦) = (πΊ NeighbVtx π¦) |
| 6 | | simpl 481 |
. . . . . . . 8
β’ ((π₯ β π β§ π¦ β (π β {π₯})) β π₯ β π) |
| 7 | 6 | ad2antlr 723 |
. . . . . . 7
β’ (((πΊ β FriendGraph β§ (π₯ β π β§ π¦ β (π β {π₯}))) β§ π¦ β (πΊ NeighbVtx π₯)) β π₯ β π) |
| 8 | | eldifi 4125 |
. . . . . . . . 9
β’ (π¦ β (π β {π₯}) β π¦ β π) |
| 9 | 8 | adantl 480 |
. . . . . . . 8
β’ ((π₯ β π β§ π¦ β (π β {π₯})) β π¦ β π) |
| 10 | 9 | ad2antlr 723 |
. . . . . . 7
β’ (((πΊ β FriendGraph β§ (π₯ β π β§ π¦ β (π β {π₯}))) β§ π¦ β (πΊ NeighbVtx π₯)) β π¦ β π) |
| 11 | | eldif 3957 |
. . . . . . . . . 10
β’ (π¦ β (π β {π₯}) β (π¦ β π β§ Β¬ π¦ β {π₯})) |
| 12 | | velsn 4643 |
. . . . . . . . . . . . 13
β’ (π¦ β {π₯} β π¦ = π₯) |
| 13 | 12 | biimpri 227 |
. . . . . . . . . . . 12
β’ (π¦ = π₯ β π¦ β {π₯}) |
| 14 | 13 | equcoms 2021 |
. . . . . . . . . . 11
β’ (π₯ = π¦ β π¦ β {π₯}) |
| 15 | 14 | necon3bi 2965 |
. . . . . . . . . 10
β’ (Β¬
π¦ β {π₯} β π₯ β π¦) |
| 16 | 11, 15 | simplbiim 503 |
. . . . . . . . 9
β’ (π¦ β (π β {π₯}) β π₯ β π¦) |
| 17 | 16 | adantl 480 |
. . . . . . . 8
β’ ((π₯ β π β§ π¦ β (π β {π₯})) β π₯ β π¦) |
| 18 | 17 | ad2antlr 723 |
. . . . . . 7
β’ (((πΊ β FriendGraph β§ (π₯ β π β§ π¦ β (π β {π₯}))) β§ π¦ β (πΊ NeighbVtx π₯)) β π₯ β π¦) |
| 19 | | simpr 483 |
. . . . . . 7
β’ (((πΊ β FriendGraph β§ (π₯ β π β§ π¦ β (π β {π₯}))) β§ π¦ β (πΊ NeighbVtx π₯)) β π¦ β (πΊ NeighbVtx π₯)) |
| 20 | | simpl 481 |
. . . . . . . 8
β’ ((πΊ β FriendGraph β§ (π₯ β π β§ π¦ β (π β {π₯}))) β πΊ β FriendGraph ) |
| 21 | 20 | adantr 479 |
. . . . . . 7
β’ (((πΊ β FriendGraph β§ (π₯ β π β§ π¦ β (π β {π₯}))) β§ π¦ β (πΊ NeighbVtx π₯)) β πΊ β FriendGraph ) |
| 22 | | eqid 2730 |
. . . . . . 7
β’ (π β (πΊ NeighbVtx π₯) β¦ (β©π β (πΊ NeighbVtx π¦){π, π} β (EdgβπΊ))) = (π β (πΊ NeighbVtx π₯) β¦ (β©π β (πΊ NeighbVtx π¦){π, π} β (EdgβπΊ))) |
| 23 | 2, 3, 4, 5, 7, 10,
18, 19, 21, 22 | frgrncvvdeqlem10 29828 |
. . . . . 6
β’ (((πΊ β FriendGraph β§ (π₯ β π β§ π¦ β (π β {π₯}))) β§ π¦ β (πΊ NeighbVtx π₯)) β (π β (πΊ NeighbVtx π₯) β¦ (β©π β (πΊ NeighbVtx π¦){π, π} β (EdgβπΊ))):(πΊ NeighbVtx π₯)β1-1-ontoβ(πΊ NeighbVtx π¦)) |
| 24 | 1, 23 | hasheqf1od 14317 |
. . . . 5
β’ (((πΊ β FriendGraph β§ (π₯ β π β§ π¦ β (π β {π₯}))) β§ π¦ β (πΊ NeighbVtx π₯)) β (β―β(πΊ NeighbVtx π₯)) = (β―β(πΊ NeighbVtx π¦))) |
| 25 | | frgrusgr 29781 |
. . . . . . . 8
β’ (πΊ β FriendGraph β πΊ β
USGraph) |
| 26 | 25, 6 | anim12i 611 |
. . . . . . 7
β’ ((πΊ β FriendGraph β§ (π₯ β π β§ π¦ β (π β {π₯}))) β (πΊ β USGraph β§ π₯ β π)) |
| 27 | 26 | adantr 479 |
. . . . . 6
β’ (((πΊ β FriendGraph β§ (π₯ β π β§ π¦ β (π β {π₯}))) β§ π¦ β (πΊ NeighbVtx π₯)) β (πΊ β USGraph β§ π₯ β π)) |
| 28 | 2 | hashnbusgrvd 29052 |
. . . . . 6
β’ ((πΊ β USGraph β§ π₯ β π) β (β―β(πΊ NeighbVtx π₯)) = ((VtxDegβπΊ)βπ₯)) |
| 29 | 27, 28 | syl 17 |
. . . . 5
β’ (((πΊ β FriendGraph β§ (π₯ β π β§ π¦ β (π β {π₯}))) β§ π¦ β (πΊ NeighbVtx π₯)) β (β―β(πΊ NeighbVtx π₯)) = ((VtxDegβπΊ)βπ₯)) |
| 30 | 25, 9 | anim12i 611 |
. . . . . . 7
β’ ((πΊ β FriendGraph β§ (π₯ β π β§ π¦ β (π β {π₯}))) β (πΊ β USGraph β§ π¦ β π)) |
| 31 | 30 | adantr 479 |
. . . . . 6
β’ (((πΊ β FriendGraph β§ (π₯ β π β§ π¦ β (π β {π₯}))) β§ π¦ β (πΊ NeighbVtx π₯)) β (πΊ β USGraph β§ π¦ β π)) |
| 32 | 2 | hashnbusgrvd 29052 |
. . . . . 6
β’ ((πΊ β USGraph β§ π¦ β π) β (β―β(πΊ NeighbVtx π¦)) = ((VtxDegβπΊ)βπ¦)) |
| 33 | 31, 32 | syl 17 |
. . . . 5
β’ (((πΊ β FriendGraph β§ (π₯ β π β§ π¦ β (π β {π₯}))) β§ π¦ β (πΊ NeighbVtx π₯)) β (β―β(πΊ NeighbVtx π¦)) = ((VtxDegβπΊ)βπ¦)) |
| 34 | 24, 29, 33 | 3eqtr3d 2778 |
. . . 4
β’ (((πΊ β FriendGraph β§ (π₯ β π β§ π¦ β (π β {π₯}))) β§ π¦ β (πΊ NeighbVtx π₯)) β ((VtxDegβπΊ)βπ₯) = ((VtxDegβπΊ)βπ¦)) |
| 35 | | frgrncvvdeq.d |
. . . . 5
β’ π· = (VtxDegβπΊ) |
| 36 | 35 | fveq1i 6891 |
. . . 4
β’ (π·βπ₯) = ((VtxDegβπΊ)βπ₯) |
| 37 | 35 | fveq1i 6891 |
. . . 4
β’ (π·βπ¦) = ((VtxDegβπΊ)βπ¦) |
| 38 | 34, 36, 37 | 3eqtr4g 2795 |
. . 3
β’ (((πΊ β FriendGraph β§ (π₯ β π β§ π¦ β (π β {π₯}))) β§ π¦ β (πΊ NeighbVtx π₯)) β (π·βπ₯) = (π·βπ¦)) |
| 39 | 38 | ex 411 |
. 2
β’ ((πΊ β FriendGraph β§ (π₯ β π β§ π¦ β (π β {π₯}))) β (π¦ β (πΊ NeighbVtx π₯) β (π·βπ₯) = (π·βπ¦))) |
| 40 | 39 | ralrimivva 3198 |
1
β’ (πΊ β FriendGraph β
βπ₯ β π βπ¦ β (π β {π₯})(π¦ β (πΊ NeighbVtx π₯) β (π·βπ₯) = (π·βπ¦))) |
