Step | Hyp | Ref
| Expression |
1 | | fveq2 6847 |
. . . . . 6
β’ (π = π β (π·βπ) = (π·βπ)) |
2 | 1 | a1i 11 |
. . . . 5
β’ ((π β π β§ π β π) β (π = π β (π·βπ) = (π·βπ))) |
3 | 2 | necon3d 2965 |
. . . 4
β’ ((π β π β§ π β π) β ((π·βπ) β (π·βπ) β π β π)) |
4 | 3 | imp 408 |
. . 3
β’ (((π β π β§ π β π) β§ (π·βπ) β (π·βπ)) β π β π) |
5 | 4 | 3adant1 1131 |
. 2
β’ ((πΊ β FriendGraph β§ (π β π β§ π β π) β§ (π·βπ) β (π·βπ)) β π β π) |
6 | | frgrncvvdeq.v |
. . . . . . 7
β’ π = (VtxβπΊ) |
7 | | frgrncvvdeq.d |
. . . . . . 7
β’ π· = (VtxDegβπΊ) |
8 | 6, 7 | frgrncvvdeq 29295 |
. . . . . 6
β’ (πΊ β FriendGraph β
βπ₯ β π βπ¦ β (π β {π₯})(π¦ β (πΊ NeighbVtx π₯) β (π·βπ₯) = (π·βπ¦))) |
9 | | oveq2 7370 |
. . . . . . . . . . 11
β’ (π₯ = π β (πΊ NeighbVtx π₯) = (πΊ NeighbVtx π)) |
10 | | neleq2 3056 |
. . . . . . . . . . 11
β’ ((πΊ NeighbVtx π₯) = (πΊ NeighbVtx π) β (π¦ β (πΊ NeighbVtx π₯) β π¦ β (πΊ NeighbVtx π))) |
11 | 9, 10 | syl 17 |
. . . . . . . . . 10
β’ (π₯ = π β (π¦ β (πΊ NeighbVtx π₯) β π¦ β (πΊ NeighbVtx π))) |
12 | | fveqeq2 6856 |
. . . . . . . . . 10
β’ (π₯ = π β ((π·βπ₯) = (π·βπ¦) β (π·βπ) = (π·βπ¦))) |
13 | 11, 12 | imbi12d 345 |
. . . . . . . . 9
β’ (π₯ = π β ((π¦ β (πΊ NeighbVtx π₯) β (π·βπ₯) = (π·βπ¦)) β (π¦ β (πΊ NeighbVtx π) β (π·βπ) = (π·βπ¦)))) |
14 | | neleq1 3055 |
. . . . . . . . . 10
β’ (π¦ = π β (π¦ β (πΊ NeighbVtx π) β π β (πΊ NeighbVtx π))) |
15 | | fveq2 6847 |
. . . . . . . . . . 11
β’ (π¦ = π β (π·βπ¦) = (π·βπ)) |
16 | 15 | eqeq2d 2748 |
. . . . . . . . . 10
β’ (π¦ = π β ((π·βπ) = (π·βπ¦) β (π·βπ) = (π·βπ))) |
17 | 14, 16 | imbi12d 345 |
. . . . . . . . 9
β’ (π¦ = π β ((π¦ β (πΊ NeighbVtx π) β (π·βπ) = (π·βπ¦)) β (π β (πΊ NeighbVtx π) β (π·βπ) = (π·βπ)))) |
18 | | simpll 766 |
. . . . . . . . 9
β’ (((π β π β§ π β π) β§ π β π) β π β π) |
19 | | sneq 4601 |
. . . . . . . . . . 11
β’ (π₯ = π β {π₯} = {π}) |
20 | 19 | difeq2d 4087 |
. . . . . . . . . 10
β’ (π₯ = π β (π β {π₯}) = (π β {π})) |
21 | 20 | adantl 483 |
. . . . . . . . 9
β’ ((((π β π β§ π β π) β§ π β π) β§ π₯ = π) β (π β {π₯}) = (π β {π})) |
22 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π β π β§ π β π) β π β π) |
23 | | necom 2998 |
. . . . . . . . . . . 12
β’ (π β π β π β π) |
24 | 23 | biimpi 215 |
. . . . . . . . . . 11
β’ (π β π β π β π) |
25 | 22, 24 | anim12i 614 |
. . . . . . . . . 10
β’ (((π β π β§ π β π) β§ π β π) β (π β π β§ π β π)) |
26 | | eldifsn 4752 |
. . . . . . . . . 10
β’ (π β (π β {π}) β (π β π β§ π β π)) |
27 | 25, 26 | sylibr 233 |
. . . . . . . . 9
β’ (((π β π β§ π β π) β§ π β π) β π β (π β {π})) |
28 | 13, 17, 18, 21, 27 | rspc2vd 3911 |
. . . . . . . 8
β’ (((π β π β§ π β π) β§ π β π) β (βπ₯ β π βπ¦ β (π β {π₯})(π¦ β (πΊ NeighbVtx π₯) β (π·βπ₯) = (π·βπ¦)) β (π β (πΊ NeighbVtx π) β (π·βπ) = (π·βπ)))) |
29 | | nnel 3059 |
. . . . . . . . . . 11
β’ (Β¬
π β (πΊ NeighbVtx π) β π β (πΊ NeighbVtx π)) |
30 | | nbgrsym 28353 |
. . . . . . . . . . . . . . . 16
β’ (π β (πΊ NeighbVtx π) β π β (πΊ NeighbVtx π)) |
31 | | frgrusgr 29247 |
. . . . . . . . . . . . . . . . . 18
β’ (πΊ β FriendGraph β πΊ β
USGraph) |
32 | | frgrwopreglem4a.e |
. . . . . . . . . . . . . . . . . . 19
β’ πΈ = (EdgβπΊ) |
33 | 32 | nbusgreledg 28343 |
. . . . . . . . . . . . . . . . . 18
β’ (πΊ β USGraph β (π β (πΊ NeighbVtx π) β {π, π} β πΈ)) |
34 | 31, 33 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (πΊ β FriendGraph β
(π β (πΊ NeighbVtx π) β {π, π} β πΈ)) |
35 | 34 | biimpd 228 |
. . . . . . . . . . . . . . . 16
β’ (πΊ β FriendGraph β
(π β (πΊ NeighbVtx π) β {π, π} β πΈ)) |
36 | 30, 35 | biimtrid 241 |
. . . . . . . . . . . . . . 15
β’ (πΊ β FriendGraph β
(π β (πΊ NeighbVtx π) β {π, π} β πΈ)) |
37 | 36 | imp 408 |
. . . . . . . . . . . . . 14
β’ ((πΊ β FriendGraph β§ π β (πΊ NeighbVtx π)) β {π, π} β πΈ) |
38 | 37 | a1d 25 |
. . . . . . . . . . . . 13
β’ ((πΊ β FriendGraph β§ π β (πΊ NeighbVtx π)) β ((π·βπ) β (π·βπ) β {π, π} β πΈ)) |
39 | 38 | expcom 415 |
. . . . . . . . . . . 12
β’ (π β (πΊ NeighbVtx π) β (πΊ β FriendGraph β ((π·βπ) β (π·βπ) β {π, π} β πΈ))) |
40 | 39 | a1d 25 |
. . . . . . . . . . 11
β’ (π β (πΊ NeighbVtx π) β (((π β π β§ π β π) β§ π β π) β (πΊ β FriendGraph β ((π·βπ) β (π·βπ) β {π, π} β πΈ)))) |
41 | 29, 40 | sylbi 216 |
. . . . . . . . . 10
β’ (Β¬
π β (πΊ NeighbVtx π) β (((π β π β§ π β π) β§ π β π) β (πΊ β FriendGraph β ((π·βπ) β (π·βπ) β {π, π} β πΈ)))) |
42 | | eqneqall 2955 |
. . . . . . . . . . 11
β’ ((π·βπ) = (π·βπ) β ((π·βπ) β (π·βπ) β {π, π} β πΈ)) |
43 | 42 | 2a1d 26 |
. . . . . . . . . 10
β’ ((π·βπ) = (π·βπ) β (((π β π β§ π β π) β§ π β π) β (πΊ β FriendGraph β ((π·βπ) β (π·βπ) β {π, π} β πΈ)))) |
44 | 41, 43 | ja 186 |
. . . . . . . . 9
β’ ((π β (πΊ NeighbVtx π) β (π·βπ) = (π·βπ)) β (((π β π β§ π β π) β§ π β π) β (πΊ β FriendGraph β ((π·βπ) β (π·βπ) β {π, π} β πΈ)))) |
45 | 44 | com12 32 |
. . . . . . . 8
β’ (((π β π β§ π β π) β§ π β π) β ((π β (πΊ NeighbVtx π) β (π·βπ) = (π·βπ)) β (πΊ β FriendGraph β ((π·βπ) β (π·βπ) β {π, π} β πΈ)))) |
46 | 28, 45 | syld 47 |
. . . . . . 7
β’ (((π β π β§ π β π) β§ π β π) β (βπ₯ β π βπ¦ β (π β {π₯})(π¦ β (πΊ NeighbVtx π₯) β (π·βπ₯) = (π·βπ¦)) β (πΊ β FriendGraph β ((π·βπ) β (π·βπ) β {π, π} β πΈ)))) |
47 | 46 | com3l 89 |
. . . . . 6
β’
(βπ₯ β
π βπ¦ β (π β {π₯})(π¦ β (πΊ NeighbVtx π₯) β (π·βπ₯) = (π·βπ¦)) β (πΊ β FriendGraph β (((π β π β§ π β π) β§ π β π) β ((π·βπ) β (π·βπ) β {π, π} β πΈ)))) |
48 | 8, 47 | mpcom 38 |
. . . . 5
β’ (πΊ β FriendGraph β
(((π β π β§ π β π) β§ π β π) β ((π·βπ) β (π·βπ) β {π, π} β πΈ))) |
49 | 48 | expd 417 |
. . . 4
β’ (πΊ β FriendGraph β
((π β π β§ π β π) β (π β π β ((π·βπ) β (π·βπ) β {π, π} β πΈ)))) |
50 | 49 | com34 91 |
. . 3
β’ (πΊ β FriendGraph β
((π β π β§ π β π) β ((π·βπ) β (π·βπ) β (π β π β {π, π} β πΈ)))) |
51 | 50 | 3imp 1112 |
. 2
β’ ((πΊ β FriendGraph β§ (π β π β§ π β π) β§ (π·βπ) β (π·βπ)) β (π β π β {π, π} β πΈ)) |
52 | 5, 51 | mpd 15 |
1
β’ ((πΊ β FriendGraph β§ (π β π β§ π β π) β§ (π·βπ) β (π·βπ)) β {π, π} β πΈ) |