Step | Hyp | Ref
| Expression |
1 | | frgrncvvdeq.ny |
. . 3
⊢ 𝑁 = (𝐺 NeighbVtx 𝑌) |
2 | 1 | ineq2i 3773 |
. 2
⊢ ((𝐺 NeighbVtx 𝑥) ∩ 𝑁) = ((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) |
3 | | frgrncvvdeq.nx |
. . . . . . 7
⊢ 𝐷 = (𝐺 NeighbVtx 𝑋) |
4 | 3 | eleq2i 2680 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 ↔ 𝑥 ∈ (𝐺 NeighbVtx 𝑋)) |
5 | | frgrncvvdeq.f |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ FriendGraph ) |
6 | | frgrusgr 41432 |
. . . . . . . 8
⊢ (𝐺 ∈ FriendGraph → 𝐺 ∈ USGraph
) |
7 | 5, 6 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐺 ∈ USGraph ) |
8 | | frgrncvvdeq.v1 |
. . . . . . . . 9
⊢ 𝑉 = (Vtx‘𝐺) |
9 | 8 | nbgrisvtx 40581 |
. . . . . . . 8
⊢ ((𝐺 ∈ USGraph ∧ 𝑥 ∈ (𝐺 NeighbVtx 𝑋)) → 𝑥 ∈ 𝑉) |
10 | 9 | ex 449 |
. . . . . . 7
⊢ (𝐺 ∈ USGraph → (𝑥 ∈ (𝐺 NeighbVtx 𝑋) → 𝑥 ∈ 𝑉)) |
11 | 7, 10 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (𝐺 NeighbVtx 𝑋) → 𝑥 ∈ 𝑉)) |
12 | 4, 11 | syl5bi 231 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝐷 → 𝑥 ∈ 𝑉)) |
13 | 12 | imp 444 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ 𝑉) |
14 | | frgrncvvdeq.e |
. . . . 5
⊢ 𝐸 = (Edg‘𝐺) |
15 | | frgrncvvdeq.x |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
16 | | frgrncvvdeq.y |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ 𝑉) |
17 | | frgrncvvdeq.ne |
. . . . 5
⊢ (𝜑 → 𝑋 ≠ 𝑌) |
18 | | frgrncvvdeq.xy |
. . . . 5
⊢ (𝜑 → 𝑌 ∉ 𝐷) |
19 | | frgrncvvdeq.a |
. . . . 5
⊢ 𝐴 = (𝑥 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)) |
20 | 8, 14, 3, 1, 15, 16, 17, 18, 5, 19 | frgrncvvdeqlem1 41469 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝑌 ∈ (𝑉 ∖ {𝑥})) |
21 | 5 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐺 ∈ FriendGraph ) |
22 | 8, 14 | frcond3 41440 |
. . . . 5
⊢ (𝐺 ∈ FriendGraph →
∀𝑎 ∈ 𝑉 ∀𝑏 ∈ (𝑉 ∖ {𝑎})∃𝑛 ∈ 𝑉 ((𝐺 NeighbVtx 𝑎) ∩ (𝐺 NeighbVtx 𝑏)) = {𝑛}) |
23 | 21, 22 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ (𝑉 ∖ {𝑎})∃𝑛 ∈ 𝑉 ((𝐺 NeighbVtx 𝑎) ∩ (𝐺 NeighbVtx 𝑏)) = {𝑛}) |
24 | 13, 20, 23 | jca31 555 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((𝑥 ∈ 𝑉 ∧ 𝑌 ∈ (𝑉 ∖ {𝑥})) ∧ ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ (𝑉 ∖ {𝑎})∃𝑛 ∈ 𝑉 ((𝐺 NeighbVtx 𝑎) ∩ (𝐺 NeighbVtx 𝑏)) = {𝑛})) |
25 | | sneq 4135 |
. . . . . . . . 9
⊢ (𝑎 = 𝑥 → {𝑎} = {𝑥}) |
26 | 25 | difeq2d 3690 |
. . . . . . . 8
⊢ (𝑎 = 𝑥 → (𝑉 ∖ {𝑎}) = (𝑉 ∖ {𝑥})) |
27 | | oveq2 6557 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑥 → (𝐺 NeighbVtx 𝑎) = (𝐺 NeighbVtx 𝑥)) |
28 | 27 | ineq1d 3775 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑥 → ((𝐺 NeighbVtx 𝑎) ∩ (𝐺 NeighbVtx 𝑏)) = ((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑏))) |
29 | 28 | eqeq1d 2612 |
. . . . . . . . 9
⊢ (𝑎 = 𝑥 → (((𝐺 NeighbVtx 𝑎) ∩ (𝐺 NeighbVtx 𝑏)) = {𝑛} ↔ ((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑏)) = {𝑛})) |
30 | 29 | rexbidv 3034 |
. . . . . . . 8
⊢ (𝑎 = 𝑥 → (∃𝑛 ∈ 𝑉 ((𝐺 NeighbVtx 𝑎) ∩ (𝐺 NeighbVtx 𝑏)) = {𝑛} ↔ ∃𝑛 ∈ 𝑉 ((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑏)) = {𝑛})) |
31 | 26, 30 | raleqbidv 3129 |
. . . . . . 7
⊢ (𝑎 = 𝑥 → (∀𝑏 ∈ (𝑉 ∖ {𝑎})∃𝑛 ∈ 𝑉 ((𝐺 NeighbVtx 𝑎) ∩ (𝐺 NeighbVtx 𝑏)) = {𝑛} ↔ ∀𝑏 ∈ (𝑉 ∖ {𝑥})∃𝑛 ∈ 𝑉 ((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑏)) = {𝑛})) |
32 | 31 | rspcva 3280 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑉 ∧ ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ (𝑉 ∖ {𝑎})∃𝑛 ∈ 𝑉 ((𝐺 NeighbVtx 𝑎) ∩ (𝐺 NeighbVtx 𝑏)) = {𝑛}) → ∀𝑏 ∈ (𝑉 ∖ {𝑥})∃𝑛 ∈ 𝑉 ((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑏)) = {𝑛}) |
33 | | oveq2 6557 |
. . . . . . . . . . . 12
⊢ (𝑏 = 𝑌 → (𝐺 NeighbVtx 𝑏) = (𝐺 NeighbVtx 𝑌)) |
34 | 33 | ineq2d 3776 |
. . . . . . . . . . 11
⊢ (𝑏 = 𝑌 → ((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑏)) = ((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌))) |
35 | 34 | eqeq1d 2612 |
. . . . . . . . . 10
⊢ (𝑏 = 𝑌 → (((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑏)) = {𝑛} ↔ ((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {𝑛})) |
36 | 35 | rexbidv 3034 |
. . . . . . . . 9
⊢ (𝑏 = 𝑌 → (∃𝑛 ∈ 𝑉 ((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑏)) = {𝑛} ↔ ∃𝑛 ∈ 𝑉 ((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {𝑛})) |
37 | 36 | rspcva 3280 |
. . . . . . . 8
⊢ ((𝑌 ∈ (𝑉 ∖ {𝑥}) ∧ ∀𝑏 ∈ (𝑉 ∖ {𝑥})∃𝑛 ∈ 𝑉 ((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑏)) = {𝑛}) → ∃𝑛 ∈ 𝑉 ((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {𝑛}) |
38 | | vsnid 4156 |
. . . . . . . . . . . . . . 15
⊢ 𝑛 ∈ {𝑛} |
39 | | eleq2 2677 |
. . . . . . . . . . . . . . . . 17
⊢ ({𝑛} = ((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) → (𝑛 ∈ {𝑛} ↔ 𝑛 ∈ ((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)))) |
40 | 39 | eqcoms 2618 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {𝑛} → (𝑛 ∈ {𝑛} ↔ 𝑛 ∈ ((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)))) |
41 | | elin 3758 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) ↔ (𝑛 ∈ (𝐺 NeighbVtx 𝑥) ∧ 𝑛 ∈ (𝐺 NeighbVtx 𝑌))) |
42 | 41 | biimpi 205 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) → (𝑛 ∈ (𝐺 NeighbVtx 𝑥) ∧ 𝑛 ∈ (𝐺 NeighbVtx 𝑌))) |
43 | 40, 42 | syl6bi 242 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {𝑛} → (𝑛 ∈ {𝑛} → (𝑛 ∈ (𝐺 NeighbVtx 𝑥) ∧ 𝑛 ∈ (𝐺 NeighbVtx 𝑌)))) |
44 | 38, 43 | mpi 20 |
. . . . . . . . . . . . . 14
⊢ (((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {𝑛} → (𝑛 ∈ (𝐺 NeighbVtx 𝑥) ∧ 𝑛 ∈ (𝐺 NeighbVtx 𝑌))) |
45 | 14 | nbusgreledg 40575 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐺 ∈ USGraph → (𝑛 ∈ (𝐺 NeighbVtx 𝑥) ↔ {𝑛, 𝑥} ∈ 𝐸)) |
46 | | prcom 4211 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ {𝑛, 𝑥} = {𝑥, 𝑛} |
47 | 46 | eleq1i 2679 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ({𝑛, 𝑥} ∈ 𝐸 ↔ {𝑥, 𝑛} ∈ 𝐸) |
48 | 45, 47 | syl6bb 275 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐺 ∈ USGraph → (𝑛 ∈ (𝐺 NeighbVtx 𝑥) ↔ {𝑥, 𝑛} ∈ 𝐸)) |
49 | 48 | biimpd 218 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐺 ∈ USGraph → (𝑛 ∈ (𝐺 NeighbVtx 𝑥) → {𝑥, 𝑛} ∈ 𝐸)) |
50 | 7, 49 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑛 ∈ (𝐺 NeighbVtx 𝑥) → {𝑥, 𝑛} ∈ 𝐸)) |
51 | 50 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝑛 ∈ (𝐺 NeighbVtx 𝑥) → {𝑥, 𝑛} ∈ 𝐸)) |
52 | 51 | com12 32 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ (𝐺 NeighbVtx 𝑥) → ((𝜑 ∧ 𝑥 ∈ 𝐷) → {𝑥, 𝑛} ∈ 𝐸)) |
53 | 52 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈ (𝐺 NeighbVtx 𝑥) ∧ 𝑛 ∈ (𝐺 NeighbVtx 𝑌)) → ((𝜑 ∧ 𝑥 ∈ 𝐷) → {𝑥, 𝑛} ∈ 𝐸)) |
54 | 53 | imp 444 |
. . . . . . . . . . . . . . 15
⊢ (((𝑛 ∈ (𝐺 NeighbVtx 𝑥) ∧ 𝑛 ∈ (𝐺 NeighbVtx 𝑌)) ∧ (𝜑 ∧ 𝑥 ∈ 𝐷)) → {𝑥, 𝑛} ∈ 𝐸) |
55 | 1 | eqcomi 2619 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐺 NeighbVtx 𝑌) = 𝑁 |
56 | 55 | eleq2i 2680 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ (𝐺 NeighbVtx 𝑌) ↔ 𝑛 ∈ 𝑁) |
57 | 56 | biimpi 205 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ (𝐺 NeighbVtx 𝑌) → 𝑛 ∈ 𝑁) |
58 | 57 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈ (𝐺 NeighbVtx 𝑥) ∧ 𝑛 ∈ (𝐺 NeighbVtx 𝑌)) → 𝑛 ∈ 𝑁) |
59 | 8, 14, 3, 1, 15, 16, 17, 18, 5, 19 | frgrncvvdeqlem3 41471 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ∃!𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸) |
60 | | preq2 4213 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝑛 → {𝑥, 𝑦} = {𝑥, 𝑛}) |
61 | 60 | eleq1d 2672 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑛 → ({𝑥, 𝑦} ∈ 𝐸 ↔ {𝑥, 𝑛} ∈ 𝐸)) |
62 | 61 | riota2 6533 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈ 𝑁 ∧ ∃!𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸) → ({𝑥, 𝑛} ∈ 𝐸 ↔ (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸) = 𝑛)) |
63 | 58, 59, 62 | syl2an 493 |
. . . . . . . . . . . . . . 15
⊢ (((𝑛 ∈ (𝐺 NeighbVtx 𝑥) ∧ 𝑛 ∈ (𝐺 NeighbVtx 𝑌)) ∧ (𝜑 ∧ 𝑥 ∈ 𝐷)) → ({𝑥, 𝑛} ∈ 𝐸 ↔ (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸) = 𝑛)) |
64 | 54, 63 | mpbid 221 |
. . . . . . . . . . . . . 14
⊢ (((𝑛 ∈ (𝐺 NeighbVtx 𝑥) ∧ 𝑛 ∈ (𝐺 NeighbVtx 𝑌)) ∧ (𝜑 ∧ 𝑥 ∈ 𝐷)) → (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸) = 𝑛) |
65 | 44, 64 | sylan 487 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {𝑛} ∧ (𝜑 ∧ 𝑥 ∈ 𝐷)) → (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸) = 𝑛) |
66 | 65 | eqcomd 2616 |
. . . . . . . . . . . 12
⊢ ((((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {𝑛} ∧ (𝜑 ∧ 𝑥 ∈ 𝐷)) → 𝑛 = (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)) |
67 | 66 | sneqd 4137 |
. . . . . . . . . . 11
⊢ ((((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {𝑛} ∧ (𝜑 ∧ 𝑥 ∈ 𝐷)) → {𝑛} = {(℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)}) |
68 | | eqeq1 2614 |
. . . . . . . . . . . 12
⊢ (((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {𝑛} → (((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {(℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)} ↔ {𝑛} = {(℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)})) |
69 | 68 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {𝑛} ∧ (𝜑 ∧ 𝑥 ∈ 𝐷)) → (((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {(℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)} ↔ {𝑛} = {(℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)})) |
70 | 67, 69 | mpbird 246 |
. . . . . . . . . 10
⊢ ((((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {𝑛} ∧ (𝜑 ∧ 𝑥 ∈ 𝐷)) → ((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {(℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)}) |
71 | 70 | ex 449 |
. . . . . . . . 9
⊢ (((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {𝑛} → ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {(℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)})) |
72 | 71 | rexlimivw 3011 |
. . . . . . . 8
⊢
(∃𝑛 ∈
𝑉 ((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {𝑛} → ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {(℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)})) |
73 | 37, 72 | syl 17 |
. . . . . . 7
⊢ ((𝑌 ∈ (𝑉 ∖ {𝑥}) ∧ ∀𝑏 ∈ (𝑉 ∖ {𝑥})∃𝑛 ∈ 𝑉 ((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑏)) = {𝑛}) → ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {(℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)})) |
74 | 73 | expcom 450 |
. . . . . 6
⊢
(∀𝑏 ∈
(𝑉 ∖ {𝑥})∃𝑛 ∈ 𝑉 ((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑏)) = {𝑛} → (𝑌 ∈ (𝑉 ∖ {𝑥}) → ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {(℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)}))) |
75 | 32, 74 | syl 17 |
. . . . 5
⊢ ((𝑥 ∈ 𝑉 ∧ ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ (𝑉 ∖ {𝑎})∃𝑛 ∈ 𝑉 ((𝐺 NeighbVtx 𝑎) ∩ (𝐺 NeighbVtx 𝑏)) = {𝑛}) → (𝑌 ∈ (𝑉 ∖ {𝑥}) → ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {(℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)}))) |
76 | 75 | impancom 455 |
. . . 4
⊢ ((𝑥 ∈ 𝑉 ∧ 𝑌 ∈ (𝑉 ∖ {𝑥})) → (∀𝑎 ∈ 𝑉 ∀𝑏 ∈ (𝑉 ∖ {𝑎})∃𝑛 ∈ 𝑉 ((𝐺 NeighbVtx 𝑎) ∩ (𝐺 NeighbVtx 𝑏)) = {𝑛} → ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {(℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)}))) |
77 | 76 | imp 444 |
. . 3
⊢ (((𝑥 ∈ 𝑉 ∧ 𝑌 ∈ (𝑉 ∖ {𝑥})) ∧ ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ (𝑉 ∖ {𝑎})∃𝑛 ∈ 𝑉 ((𝐺 NeighbVtx 𝑎) ∩ (𝐺 NeighbVtx 𝑏)) = {𝑛}) → ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {(℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)})) |
78 | 24, 77 | mpcom 37 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((𝐺 NeighbVtx 𝑥) ∩ (𝐺 NeighbVtx 𝑌)) = {(℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)}) |
79 | 2, 78 | syl5req 2657 |
1
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → {(℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)} = ((𝐺 NeighbVtx 𝑥) ∩ 𝑁)) |