Step | Hyp | Ref
| Expression |
1 | | fveq2 6191 |
. . . . . 6
⊢ (𝑋 = 𝑌 → (𝐷‘𝑋) = (𝐷‘𝑌)) |
2 | 1 | a1i 11 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 = 𝑌 → (𝐷‘𝑋) = (𝐷‘𝑌))) |
3 | 2 | necon3d 2815 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ((𝐷‘𝑋) ≠ (𝐷‘𝑌) → 𝑋 ≠ 𝑌)) |
4 | 3 | imp 445 |
. . 3
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ≠ (𝐷‘𝑌)) → 𝑋 ≠ 𝑌) |
5 | 4 | 3adant1 1079 |
. 2
⊢ ((𝐺 ∈ FriendGraph ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ≠ (𝐷‘𝑌)) → 𝑋 ≠ 𝑌) |
6 | | frgrncvvdeq.v |
. . . . . . 7
⊢ 𝑉 = (Vtx‘𝐺) |
7 | | frgrncvvdeq.d |
. . . . . . 7
⊢ 𝐷 = (VtxDeg‘𝐺) |
8 | 6, 7 | frgrncvvdeq 27173 |
. . . . . 6
⊢ (𝐺 ∈ FriendGraph →
∀𝑥 ∈ 𝑉 ∀𝑦 ∈ (𝑉 ∖ {𝑥})(𝑦 ∉ (𝐺 NeighbVtx 𝑥) → (𝐷‘𝑥) = (𝐷‘𝑦))) |
9 | | oveq2 6658 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑋 → (𝐺 NeighbVtx 𝑥) = (𝐺 NeighbVtx 𝑋)) |
10 | | neleq2 2903 |
. . . . . . . . . . 11
⊢ ((𝐺 NeighbVtx 𝑥) = (𝐺 NeighbVtx 𝑋) → (𝑦 ∉ (𝐺 NeighbVtx 𝑥) ↔ 𝑦 ∉ (𝐺 NeighbVtx 𝑋))) |
11 | 9, 10 | syl 17 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑋 → (𝑦 ∉ (𝐺 NeighbVtx 𝑥) ↔ 𝑦 ∉ (𝐺 NeighbVtx 𝑋))) |
12 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑋 → (𝐷‘𝑥) = (𝐷‘𝑋)) |
13 | 12 | eqeq1d 2624 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑋 → ((𝐷‘𝑥) = (𝐷‘𝑦) ↔ (𝐷‘𝑋) = (𝐷‘𝑦))) |
14 | 11, 13 | imbi12d 334 |
. . . . . . . . 9
⊢ (𝑥 = 𝑋 → ((𝑦 ∉ (𝐺 NeighbVtx 𝑥) → (𝐷‘𝑥) = (𝐷‘𝑦)) ↔ (𝑦 ∉ (𝐺 NeighbVtx 𝑋) → (𝐷‘𝑋) = (𝐷‘𝑦)))) |
15 | | neleq1 2902 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑌 → (𝑦 ∉ (𝐺 NeighbVtx 𝑋) ↔ 𝑌 ∉ (𝐺 NeighbVtx 𝑋))) |
16 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑌 → (𝐷‘𝑦) = (𝐷‘𝑌)) |
17 | 16 | eqeq2d 2632 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑌 → ((𝐷‘𝑋) = (𝐷‘𝑦) ↔ (𝐷‘𝑋) = (𝐷‘𝑌))) |
18 | 15, 17 | imbi12d 334 |
. . . . . . . . 9
⊢ (𝑦 = 𝑌 → ((𝑦 ∉ (𝐺 NeighbVtx 𝑋) → (𝐷‘𝑋) = (𝐷‘𝑦)) ↔ (𝑌 ∉ (𝐺 NeighbVtx 𝑋) → (𝐷‘𝑋) = (𝐷‘𝑌)))) |
19 | | simpll 790 |
. . . . . . . . 9
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ 𝑋 ≠ 𝑌) → 𝑋 ∈ 𝑉) |
20 | | sneq 4187 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑋 → {𝑥} = {𝑋}) |
21 | 20 | difeq2d 3728 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑋 → (𝑉 ∖ {𝑥}) = (𝑉 ∖ {𝑋})) |
22 | 21 | adantl 482 |
. . . . . . . . 9
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ 𝑋 ≠ 𝑌) ∧ 𝑥 = 𝑋) → (𝑉 ∖ {𝑥}) = (𝑉 ∖ {𝑋})) |
23 | | simpr 477 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → 𝑌 ∈ 𝑉) |
24 | | necom 2847 |
. . . . . . . . . . . 12
⊢ (𝑋 ≠ 𝑌 ↔ 𝑌 ≠ 𝑋) |
25 | 24 | biimpi 206 |
. . . . . . . . . . 11
⊢ (𝑋 ≠ 𝑌 → 𝑌 ≠ 𝑋) |
26 | 23, 25 | anim12i 590 |
. . . . . . . . . 10
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ 𝑋 ≠ 𝑌) → (𝑌 ∈ 𝑉 ∧ 𝑌 ≠ 𝑋)) |
27 | | eldifsn 4317 |
. . . . . . . . . 10
⊢ (𝑌 ∈ (𝑉 ∖ {𝑋}) ↔ (𝑌 ∈ 𝑉 ∧ 𝑌 ≠ 𝑋)) |
28 | 26, 27 | sylibr 224 |
. . . . . . . . 9
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ 𝑋 ≠ 𝑌) → 𝑌 ∈ (𝑉 ∖ {𝑋})) |
29 | 14, 18, 19, 22, 28 | rspc2vd 27129 |
. . . . . . . 8
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ 𝑋 ≠ 𝑌) → (∀𝑥 ∈ 𝑉 ∀𝑦 ∈ (𝑉 ∖ {𝑥})(𝑦 ∉ (𝐺 NeighbVtx 𝑥) → (𝐷‘𝑥) = (𝐷‘𝑦)) → (𝑌 ∉ (𝐺 NeighbVtx 𝑋) → (𝐷‘𝑋) = (𝐷‘𝑌)))) |
30 | | nnel 2906 |
. . . . . . . . . . 11
⊢ (¬
𝑌 ∉ (𝐺 NeighbVtx 𝑋) ↔ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) |
31 | | nbgrsym 26265 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ FriendGraph →
(𝑌 ∈ (𝐺 NeighbVtx 𝑋) ↔ 𝑋 ∈ (𝐺 NeighbVtx 𝑌))) |
32 | | frgrusgr 27124 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐺 ∈ FriendGraph → 𝐺 ∈ USGraph
) |
33 | | frgrwopreglem4a.e |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝐸 = (Edg‘𝐺) |
34 | 33 | nbusgreledg 26249 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐺 ∈ USGraph → (𝑋 ∈ (𝐺 NeighbVtx 𝑌) ↔ {𝑋, 𝑌} ∈ 𝐸)) |
35 | 32, 34 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐺 ∈ FriendGraph →
(𝑋 ∈ (𝐺 NeighbVtx 𝑌) ↔ {𝑋, 𝑌} ∈ 𝐸)) |
36 | 35 | biimpd 219 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ FriendGraph →
(𝑋 ∈ (𝐺 NeighbVtx 𝑌) → {𝑋, 𝑌} ∈ 𝐸)) |
37 | 31, 36 | sylbid 230 |
. . . . . . . . . . . . . . 15
⊢ (𝐺 ∈ FriendGraph →
(𝑌 ∈ (𝐺 NeighbVtx 𝑋) → {𝑋, 𝑌} ∈ 𝐸)) |
38 | 37 | imp 445 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) → {𝑋, 𝑌} ∈ 𝐸) |
39 | 38 | a1d 25 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) → ((𝐷‘𝑋) ≠ (𝐷‘𝑌) → {𝑋, 𝑌} ∈ 𝐸)) |
40 | 39 | expcom 451 |
. . . . . . . . . . . 12
⊢ (𝑌 ∈ (𝐺 NeighbVtx 𝑋) → (𝐺 ∈ FriendGraph → ((𝐷‘𝑋) ≠ (𝐷‘𝑌) → {𝑋, 𝑌} ∈ 𝐸))) |
41 | 40 | a1d 25 |
. . . . . . . . . . 11
⊢ (𝑌 ∈ (𝐺 NeighbVtx 𝑋) → (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ 𝑋 ≠ 𝑌) → (𝐺 ∈ FriendGraph → ((𝐷‘𝑋) ≠ (𝐷‘𝑌) → {𝑋, 𝑌} ∈ 𝐸)))) |
42 | 30, 41 | sylbi 207 |
. . . . . . . . . 10
⊢ (¬
𝑌 ∉ (𝐺 NeighbVtx 𝑋) → (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ 𝑋 ≠ 𝑌) → (𝐺 ∈ FriendGraph → ((𝐷‘𝑋) ≠ (𝐷‘𝑌) → {𝑋, 𝑌} ∈ 𝐸)))) |
43 | | eqneqall 2805 |
. . . . . . . . . . 11
⊢ ((𝐷‘𝑋) = (𝐷‘𝑌) → ((𝐷‘𝑋) ≠ (𝐷‘𝑌) → {𝑋, 𝑌} ∈ 𝐸)) |
44 | 43 | 2a1d 26 |
. . . . . . . . . 10
⊢ ((𝐷‘𝑋) = (𝐷‘𝑌) → (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ 𝑋 ≠ 𝑌) → (𝐺 ∈ FriendGraph → ((𝐷‘𝑋) ≠ (𝐷‘𝑌) → {𝑋, 𝑌} ∈ 𝐸)))) |
45 | 42, 44 | ja 173 |
. . . . . . . . 9
⊢ ((𝑌 ∉ (𝐺 NeighbVtx 𝑋) → (𝐷‘𝑋) = (𝐷‘𝑌)) → (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ 𝑋 ≠ 𝑌) → (𝐺 ∈ FriendGraph → ((𝐷‘𝑋) ≠ (𝐷‘𝑌) → {𝑋, 𝑌} ∈ 𝐸)))) |
46 | 45 | com12 32 |
. . . . . . . 8
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ 𝑋 ≠ 𝑌) → ((𝑌 ∉ (𝐺 NeighbVtx 𝑋) → (𝐷‘𝑋) = (𝐷‘𝑌)) → (𝐺 ∈ FriendGraph → ((𝐷‘𝑋) ≠ (𝐷‘𝑌) → {𝑋, 𝑌} ∈ 𝐸)))) |
47 | 29, 46 | syld 47 |
. . . . . . 7
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ 𝑋 ≠ 𝑌) → (∀𝑥 ∈ 𝑉 ∀𝑦 ∈ (𝑉 ∖ {𝑥})(𝑦 ∉ (𝐺 NeighbVtx 𝑥) → (𝐷‘𝑥) = (𝐷‘𝑦)) → (𝐺 ∈ FriendGraph → ((𝐷‘𝑋) ≠ (𝐷‘𝑌) → {𝑋, 𝑌} ∈ 𝐸)))) |
48 | 47 | com3l 89 |
. . . . . 6
⊢
(∀𝑥 ∈
𝑉 ∀𝑦 ∈ (𝑉 ∖ {𝑥})(𝑦 ∉ (𝐺 NeighbVtx 𝑥) → (𝐷‘𝑥) = (𝐷‘𝑦)) → (𝐺 ∈ FriendGraph → (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ 𝑋 ≠ 𝑌) → ((𝐷‘𝑋) ≠ (𝐷‘𝑌) → {𝑋, 𝑌} ∈ 𝐸)))) |
49 | 8, 48 | mpcom 38 |
. . . . 5
⊢ (𝐺 ∈ FriendGraph →
(((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ 𝑋 ≠ 𝑌) → ((𝐷‘𝑋) ≠ (𝐷‘𝑌) → {𝑋, 𝑌} ∈ 𝐸))) |
50 | 49 | expd 452 |
. . . 4
⊢ (𝐺 ∈ FriendGraph →
((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 ≠ 𝑌 → ((𝐷‘𝑋) ≠ (𝐷‘𝑌) → {𝑋, 𝑌} ∈ 𝐸)))) |
51 | 50 | com34 91 |
. . 3
⊢ (𝐺 ∈ FriendGraph →
((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ((𝐷‘𝑋) ≠ (𝐷‘𝑌) → (𝑋 ≠ 𝑌 → {𝑋, 𝑌} ∈ 𝐸)))) |
52 | 51 | 3imp 1256 |
. 2
⊢ ((𝐺 ∈ FriendGraph ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ≠ (𝐷‘𝑌)) → (𝑋 ≠ 𝑌 → {𝑋, 𝑌} ∈ 𝐸)) |
53 | 5, 52 | mpd 15 |
1
⊢ ((𝐺 ∈ FriendGraph ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ≠ (𝐷‘𝑌)) → {𝑋, 𝑌} ∈ 𝐸) |