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