Step | Hyp | Ref
| Expression |
1 | | prid1g 4239 |
. . . . . . . 8
⊢ (𝐵 ∈ 𝑌 → 𝐵 ∈ {𝐵, 𝐶}) |
2 | 1 | 3ad2ant2 1076 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → 𝐵 ∈ {𝐵, 𝐶}) |
3 | 2 | adantr 480 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) → 𝐵 ∈ {𝐵, 𝐶}) |
4 | 3 | adantr 480 |
. . . . 5
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) ∧ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶}) → 𝐵 ∈ {𝐵, 𝐶}) |
5 | | eleq2 2677 |
. . . . . . 7
⊢ ({𝐵, 𝐶} = (〈𝑉, 𝐸〉 Neighbors 𝐴) → (𝐵 ∈ {𝐵, 𝐶} ↔ 𝐵 ∈ (〈𝑉, 𝐸〉 Neighbors 𝐴))) |
6 | 5 | eqcoms 2618 |
. . . . . 6
⊢
((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶} → (𝐵 ∈ {𝐵, 𝐶} ↔ 𝐵 ∈ (〈𝑉, 𝐸〉 Neighbors 𝐴))) |
7 | 6 | adantl 481 |
. . . . 5
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) ∧ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶}) → (𝐵 ∈ {𝐵, 𝐶} ↔ 𝐵 ∈ (〈𝑉, 𝐸〉 Neighbors 𝐴))) |
8 | 4, 7 | mpbid 221 |
. . . 4
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) ∧ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶}) → 𝐵 ∈ (〈𝑉, 𝐸〉 Neighbors 𝐴)) |
9 | | nbgraeledg 25959 |
. . . . . . 7
⊢ (𝑉 USGrph 𝐸 → (𝐵 ∈ (〈𝑉, 𝐸〉 Neighbors 𝐴) ↔ {𝐵, 𝐴} ∈ ran 𝐸)) |
10 | | prcom 4211 |
. . . . . . . . 9
⊢ {𝐵, 𝐴} = {𝐴, 𝐵} |
11 | 10 | a1i 11 |
. . . . . . . 8
⊢ (𝑉 USGrph 𝐸 → {𝐵, 𝐴} = {𝐴, 𝐵}) |
12 | 11 | eleq1d 2672 |
. . . . . . 7
⊢ (𝑉 USGrph 𝐸 → ({𝐵, 𝐴} ∈ ran 𝐸 ↔ {𝐴, 𝐵} ∈ ran 𝐸)) |
13 | 9, 12 | bitrd 267 |
. . . . . 6
⊢ (𝑉 USGrph 𝐸 → (𝐵 ∈ (〈𝑉, 𝐸〉 Neighbors 𝐴) ↔ {𝐴, 𝐵} ∈ ran 𝐸)) |
14 | 13 | adantl 481 |
. . . . 5
⊢ ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) → (𝐵 ∈ (〈𝑉, 𝐸〉 Neighbors 𝐴) ↔ {𝐴, 𝐵} ∈ ran 𝐸)) |
15 | 14 | ad2antlr 759 |
. . . 4
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) ∧ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶}) → (𝐵 ∈ (〈𝑉, 𝐸〉 Neighbors 𝐴) ↔ {𝐴, 𝐵} ∈ ran 𝐸)) |
16 | 8, 15 | mpbid 221 |
. . 3
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) ∧ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶}) → {𝐴, 𝐵} ∈ ran 𝐸) |
17 | | prid2g 4240 |
. . . . . . . 8
⊢ (𝐶 ∈ 𝑍 → 𝐶 ∈ {𝐵, 𝐶}) |
18 | 17 | 3ad2ant3 1077 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → 𝐶 ∈ {𝐵, 𝐶}) |
19 | 18 | adantr 480 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) → 𝐶 ∈ {𝐵, 𝐶}) |
20 | 19 | adantr 480 |
. . . . 5
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) ∧ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶}) → 𝐶 ∈ {𝐵, 𝐶}) |
21 | | eleq2 2677 |
. . . . . . 7
⊢ ({𝐵, 𝐶} = (〈𝑉, 𝐸〉 Neighbors 𝐴) → (𝐶 ∈ {𝐵, 𝐶} ↔ 𝐶 ∈ (〈𝑉, 𝐸〉 Neighbors 𝐴))) |
22 | 21 | eqcoms 2618 |
. . . . . 6
⊢
((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶} → (𝐶 ∈ {𝐵, 𝐶} ↔ 𝐶 ∈ (〈𝑉, 𝐸〉 Neighbors 𝐴))) |
23 | 22 | adantl 481 |
. . . . 5
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) ∧ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶}) → (𝐶 ∈ {𝐵, 𝐶} ↔ 𝐶 ∈ (〈𝑉, 𝐸〉 Neighbors 𝐴))) |
24 | 20, 23 | mpbid 221 |
. . . 4
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) ∧ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶}) → 𝐶 ∈ (〈𝑉, 𝐸〉 Neighbors 𝐴)) |
25 | | nbgraeledg 25959 |
. . . . . . 7
⊢ (𝑉 USGrph 𝐸 → (𝐶 ∈ (〈𝑉, 𝐸〉 Neighbors 𝐴) ↔ {𝐶, 𝐴} ∈ ran 𝐸)) |
26 | | prcom 4211 |
. . . . . . . . 9
⊢ {𝐶, 𝐴} = {𝐴, 𝐶} |
27 | 26 | a1i 11 |
. . . . . . . 8
⊢ (𝑉 USGrph 𝐸 → {𝐶, 𝐴} = {𝐴, 𝐶}) |
28 | 27 | eleq1d 2672 |
. . . . . . 7
⊢ (𝑉 USGrph 𝐸 → ({𝐶, 𝐴} ∈ ran 𝐸 ↔ {𝐴, 𝐶} ∈ ran 𝐸)) |
29 | 25, 28 | bitrd 267 |
. . . . . 6
⊢ (𝑉 USGrph 𝐸 → (𝐶 ∈ (〈𝑉, 𝐸〉 Neighbors 𝐴) ↔ {𝐴, 𝐶} ∈ ran 𝐸)) |
30 | 29 | adantl 481 |
. . . . 5
⊢ ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) → (𝐶 ∈ (〈𝑉, 𝐸〉 Neighbors 𝐴) ↔ {𝐴, 𝐶} ∈ ran 𝐸)) |
31 | 30 | ad2antlr 759 |
. . . 4
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) ∧ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶}) → (𝐶 ∈ (〈𝑉, 𝐸〉 Neighbors 𝐴) ↔ {𝐴, 𝐶} ∈ ran 𝐸)) |
32 | 24, 31 | mpbid 221 |
. . 3
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) ∧ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶}) → {𝐴, 𝐶} ∈ ran 𝐸) |
33 | 16, 32 | jca 553 |
. 2
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) ∧ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶}) → ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸)) |
34 | | nbusgra 25957 |
. . . . 5
⊢ (𝑉 USGrph 𝐸 → (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝑣 ∈ 𝑉 ∣ {𝐴, 𝑣} ∈ ran 𝐸}) |
35 | 34 | ad2antll 761 |
. . . 4
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) → (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝑣 ∈ 𝑉 ∣ {𝐴, 𝑣} ∈ ran 𝐸}) |
36 | 35 | adantr 480 |
. . 3
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸)) → (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝑣 ∈ 𝑉 ∣ {𝐴, 𝑣} ∈ ran 𝐸}) |
37 | | eleq2 2677 |
. . . . . . . . . 10
⊢ (𝑉 = {𝐴, 𝐵, 𝐶} → (𝑣 ∈ 𝑉 ↔ 𝑣 ∈ {𝐴, 𝐵, 𝐶})) |
38 | 37 | ad2antrl 760 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) → (𝑣 ∈ 𝑉 ↔ 𝑣 ∈ {𝐴, 𝐵, 𝐶})) |
39 | 38 | adantr 480 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸)) → (𝑣 ∈ 𝑉 ↔ 𝑣 ∈ {𝐴, 𝐵, 𝐶})) |
40 | | vex 3176 |
. . . . . . . . . . 11
⊢ 𝑣 ∈ V |
41 | 40 | eltp 4177 |
. . . . . . . . . 10
⊢ (𝑣 ∈ {𝐴, 𝐵, 𝐶} ↔ (𝑣 = 𝐴 ∨ 𝑣 = 𝐵 ∨ 𝑣 = 𝐶)) |
42 | | usgraedgrn 25910 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑉 USGrph 𝐸 ∧ {𝐴, 𝑣} ∈ ran 𝐸) → 𝐴 ≠ 𝑣) |
43 | | df-ne 2782 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ≠ 𝑣 ↔ ¬ 𝐴 = 𝑣) |
44 | | pm2.24 120 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 = 𝑣 → (¬ 𝐴 = 𝑣 → (𝑣 = 𝐵 ∨ 𝑣 = 𝐶))) |
45 | 44 | eqcoms 2618 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 = 𝐴 → (¬ 𝐴 = 𝑣 → (𝑣 = 𝐵 ∨ 𝑣 = 𝐶))) |
46 | 45 | com12 32 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
𝐴 = 𝑣 → (𝑣 = 𝐴 → (𝑣 = 𝐵 ∨ 𝑣 = 𝐶))) |
47 | 43, 46 | sylbi 206 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ≠ 𝑣 → (𝑣 = 𝐴 → (𝑣 = 𝐵 ∨ 𝑣 = 𝐶))) |
48 | 42, 47 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑉 USGrph 𝐸 ∧ {𝐴, 𝑣} ∈ ran 𝐸) → (𝑣 = 𝐴 → (𝑣 = 𝐵 ∨ 𝑣 = 𝐶))) |
49 | 48 | ex 449 |
. . . . . . . . . . . . . 14
⊢ (𝑉 USGrph 𝐸 → ({𝐴, 𝑣} ∈ ran 𝐸 → (𝑣 = 𝐴 → (𝑣 = 𝐵 ∨ 𝑣 = 𝐶)))) |
50 | 49 | ad2antll 761 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) → ({𝐴, 𝑣} ∈ ran 𝐸 → (𝑣 = 𝐴 → (𝑣 = 𝐵 ∨ 𝑣 = 𝐶)))) |
51 | 50 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸)) → ({𝐴, 𝑣} ∈ ran 𝐸 → (𝑣 = 𝐴 → (𝑣 = 𝐵 ∨ 𝑣 = 𝐶)))) |
52 | 51 | com3r 85 |
. . . . . . . . . . 11
⊢ (𝑣 = 𝐴 → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸)) → ({𝐴, 𝑣} ∈ ran 𝐸 → (𝑣 = 𝐵 ∨ 𝑣 = 𝐶)))) |
53 | | orc 399 |
. . . . . . . . . . . . 13
⊢ (𝑣 = 𝐵 → (𝑣 = 𝐵 ∨ 𝑣 = 𝐶)) |
54 | 53 | a1d 25 |
. . . . . . . . . . . 12
⊢ (𝑣 = 𝐵 → ({𝐴, 𝑣} ∈ ran 𝐸 → (𝑣 = 𝐵 ∨ 𝑣 = 𝐶))) |
55 | 54 | a1d 25 |
. . . . . . . . . . 11
⊢ (𝑣 = 𝐵 → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸)) → ({𝐴, 𝑣} ∈ ran 𝐸 → (𝑣 = 𝐵 ∨ 𝑣 = 𝐶)))) |
56 | | olc 398 |
. . . . . . . . . . . . 13
⊢ (𝑣 = 𝐶 → (𝑣 = 𝐵 ∨ 𝑣 = 𝐶)) |
57 | 56 | a1d 25 |
. . . . . . . . . . . 12
⊢ (𝑣 = 𝐶 → ({𝐴, 𝑣} ∈ ran 𝐸 → (𝑣 = 𝐵 ∨ 𝑣 = 𝐶))) |
58 | 57 | a1d 25 |
. . . . . . . . . . 11
⊢ (𝑣 = 𝐶 → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸)) → ({𝐴, 𝑣} ∈ ran 𝐸 → (𝑣 = 𝐵 ∨ 𝑣 = 𝐶)))) |
59 | 52, 55, 58 | 3jaoi 1383 |
. . . . . . . . . 10
⊢ ((𝑣 = 𝐴 ∨ 𝑣 = 𝐵 ∨ 𝑣 = 𝐶) → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸)) → ({𝐴, 𝑣} ∈ ran 𝐸 → (𝑣 = 𝐵 ∨ 𝑣 = 𝐶)))) |
60 | 41, 59 | sylbi 206 |
. . . . . . . . 9
⊢ (𝑣 ∈ {𝐴, 𝐵, 𝐶} → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸)) → ({𝐴, 𝑣} ∈ ran 𝐸 → (𝑣 = 𝐵 ∨ 𝑣 = 𝐶)))) |
61 | 60 | com12 32 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸)) → (𝑣 ∈ {𝐴, 𝐵, 𝐶} → ({𝐴, 𝑣} ∈ ran 𝐸 → (𝑣 = 𝐵 ∨ 𝑣 = 𝐶)))) |
62 | 39, 61 | sylbid 229 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸)) → (𝑣 ∈ 𝑉 → ({𝐴, 𝑣} ∈ ran 𝐸 → (𝑣 = 𝐵 ∨ 𝑣 = 𝐶)))) |
63 | 62 | impd 446 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸)) → ((𝑣 ∈ 𝑉 ∧ {𝐴, 𝑣} ∈ ran 𝐸) → (𝑣 = 𝐵 ∨ 𝑣 = 𝐶))) |
64 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝐵 = 𝐵 |
65 | 64 | 3mix2i 1227 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐵 = 𝐴 ∨ 𝐵 = 𝐵 ∨ 𝐵 = 𝐶) |
66 | | eltpg 4174 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐵 ∈ 𝑌 → (𝐵 ∈ {𝐴, 𝐵, 𝐶} ↔ (𝐵 = 𝐴 ∨ 𝐵 = 𝐵 ∨ 𝐵 = 𝐶))) |
67 | 65, 66 | mpbiri 247 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐵 ∈ 𝑌 → 𝐵 ∈ {𝐴, 𝐵, 𝐶}) |
68 | 67 | a1d 25 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐵 ∈ 𝑌 → ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) → 𝐵 ∈ {𝐴, 𝐵, 𝐶})) |
69 | 68 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) → 𝐵 ∈ {𝐴, 𝐵, 𝐶})) |
70 | 69 | imp 444 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) → 𝐵 ∈ {𝐴, 𝐵, 𝐶}) |
71 | 70 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) ∧ 𝑣 = 𝐵) → 𝐵 ∈ {𝐴, 𝐵, 𝐶}) |
72 | | eleq1 2676 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 = 𝐵 → (𝑣 ∈ {𝐴, 𝐵, 𝐶} ↔ 𝐵 ∈ {𝐴, 𝐵, 𝐶})) |
73 | 72 | bicomd 212 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 = 𝐵 → (𝐵 ∈ {𝐴, 𝐵, 𝐶} ↔ 𝑣 ∈ {𝐴, 𝐵, 𝐶})) |
74 | 73 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) ∧ 𝑣 = 𝐵) → (𝐵 ∈ {𝐴, 𝐵, 𝐶} ↔ 𝑣 ∈ {𝐴, 𝐵, 𝐶})) |
75 | 71, 74 | mpbid 221 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) ∧ 𝑣 = 𝐵) → 𝑣 ∈ {𝐴, 𝐵, 𝐶}) |
76 | 37 | bicomd 212 |
. . . . . . . . . . . . . . . 16
⊢ (𝑉 = {𝐴, 𝐵, 𝐶} → (𝑣 ∈ {𝐴, 𝐵, 𝐶} ↔ 𝑣 ∈ 𝑉)) |
77 | 76 | ad2antrl 760 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) → (𝑣 ∈ {𝐴, 𝐵, 𝐶} ↔ 𝑣 ∈ 𝑉)) |
78 | 77 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) ∧ 𝑣 = 𝐵) → (𝑣 ∈ {𝐴, 𝐵, 𝐶} ↔ 𝑣 ∈ 𝑉)) |
79 | 75, 78 | mpbid 221 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) ∧ 𝑣 = 𝐵) → 𝑣 ∈ 𝑉) |
80 | 79 | ex 449 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) → (𝑣 = 𝐵 → 𝑣 ∈ 𝑉)) |
81 | 80 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸)) → (𝑣 = 𝐵 → 𝑣 ∈ 𝑉)) |
82 | 81 | impcom 445 |
. . . . . . . . . 10
⊢ ((𝑣 = 𝐵 ∧ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸))) → 𝑣 ∈ 𝑉) |
83 | | preq2 4213 |
. . . . . . . . . . . . . . 15
⊢ (𝐵 = 𝑣 → {𝐴, 𝐵} = {𝐴, 𝑣}) |
84 | 83 | eleq1d 2672 |
. . . . . . . . . . . . . 14
⊢ (𝐵 = 𝑣 → ({𝐴, 𝐵} ∈ ran 𝐸 ↔ {𝐴, 𝑣} ∈ ran 𝐸)) |
85 | 84 | eqcoms 2618 |
. . . . . . . . . . . . 13
⊢ (𝑣 = 𝐵 → ({𝐴, 𝐵} ∈ ran 𝐸 ↔ {𝐴, 𝑣} ∈ ran 𝐸)) |
86 | 85 | biimpcd 238 |
. . . . . . . . . . . 12
⊢ ({𝐴, 𝐵} ∈ ran 𝐸 → (𝑣 = 𝐵 → {𝐴, 𝑣} ∈ ran 𝐸)) |
87 | 86 | ad2antrl 760 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸)) → (𝑣 = 𝐵 → {𝐴, 𝑣} ∈ ran 𝐸)) |
88 | 87 | impcom 445 |
. . . . . . . . . 10
⊢ ((𝑣 = 𝐵 ∧ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸))) → {𝐴, 𝑣} ∈ ran 𝐸) |
89 | 82, 88 | jca 553 |
. . . . . . . . 9
⊢ ((𝑣 = 𝐵 ∧ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸))) → (𝑣 ∈ 𝑉 ∧ {𝐴, 𝑣} ∈ ran 𝐸)) |
90 | 89 | ex 449 |
. . . . . . . 8
⊢ (𝑣 = 𝐵 → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸)) → (𝑣 ∈ 𝑉 ∧ {𝐴, 𝑣} ∈ ran 𝐸))) |
91 | | tpid3g 4248 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐶 ∈ 𝑍 → 𝐶 ∈ {𝐴, 𝐵, 𝐶}) |
92 | 91 | a1d 25 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐶 ∈ 𝑍 → ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) → 𝐶 ∈ {𝐴, 𝐵, 𝐶})) |
93 | 92 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) → 𝐶 ∈ {𝐴, 𝐵, 𝐶})) |
94 | 93 | imp 444 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) → 𝐶 ∈ {𝐴, 𝐵, 𝐶}) |
95 | 94 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) ∧ 𝑣 = 𝐶) → 𝐶 ∈ {𝐴, 𝐵, 𝐶}) |
96 | | eleq1 2676 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 = 𝐶 → (𝑣 ∈ {𝐴, 𝐵, 𝐶} ↔ 𝐶 ∈ {𝐴, 𝐵, 𝐶})) |
97 | 96 | bicomd 212 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 = 𝐶 → (𝐶 ∈ {𝐴, 𝐵, 𝐶} ↔ 𝑣 ∈ {𝐴, 𝐵, 𝐶})) |
98 | 97 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) ∧ 𝑣 = 𝐶) → (𝐶 ∈ {𝐴, 𝐵, 𝐶} ↔ 𝑣 ∈ {𝐴, 𝐵, 𝐶})) |
99 | 95, 98 | mpbid 221 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) ∧ 𝑣 = 𝐶) → 𝑣 ∈ {𝐴, 𝐵, 𝐶}) |
100 | 77 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) ∧ 𝑣 = 𝐶) → (𝑣 ∈ {𝐴, 𝐵, 𝐶} ↔ 𝑣 ∈ 𝑉)) |
101 | 99, 100 | mpbid 221 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) ∧ 𝑣 = 𝐶) → 𝑣 ∈ 𝑉) |
102 | 101 | ex 449 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) → (𝑣 = 𝐶 → 𝑣 ∈ 𝑉)) |
103 | 102 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸)) → (𝑣 = 𝐶 → 𝑣 ∈ 𝑉)) |
104 | 103 | impcom 445 |
. . . . . . . . . 10
⊢ ((𝑣 = 𝐶 ∧ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸))) → 𝑣 ∈ 𝑉) |
105 | | preq2 4213 |
. . . . . . . . . . . . . . 15
⊢ (𝐶 = 𝑣 → {𝐴, 𝐶} = {𝐴, 𝑣}) |
106 | 105 | eleq1d 2672 |
. . . . . . . . . . . . . 14
⊢ (𝐶 = 𝑣 → ({𝐴, 𝐶} ∈ ran 𝐸 ↔ {𝐴, 𝑣} ∈ ran 𝐸)) |
107 | 106 | eqcoms 2618 |
. . . . . . . . . . . . 13
⊢ (𝑣 = 𝐶 → ({𝐴, 𝐶} ∈ ran 𝐸 ↔ {𝐴, 𝑣} ∈ ran 𝐸)) |
108 | 107 | biimpcd 238 |
. . . . . . . . . . . 12
⊢ ({𝐴, 𝐶} ∈ ran 𝐸 → (𝑣 = 𝐶 → {𝐴, 𝑣} ∈ ran 𝐸)) |
109 | 108 | ad2antll 761 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸)) → (𝑣 = 𝐶 → {𝐴, 𝑣} ∈ ran 𝐸)) |
110 | 109 | impcom 445 |
. . . . . . . . . 10
⊢ ((𝑣 = 𝐶 ∧ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸))) → {𝐴, 𝑣} ∈ ran 𝐸) |
111 | 104, 110 | jca 553 |
. . . . . . . . 9
⊢ ((𝑣 = 𝐶 ∧ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸))) → (𝑣 ∈ 𝑉 ∧ {𝐴, 𝑣} ∈ ran 𝐸)) |
112 | 111 | ex 449 |
. . . . . . . 8
⊢ (𝑣 = 𝐶 → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸)) → (𝑣 ∈ 𝑉 ∧ {𝐴, 𝑣} ∈ ran 𝐸))) |
113 | 90, 112 | jaoi 393 |
. . . . . . 7
⊢ ((𝑣 = 𝐵 ∨ 𝑣 = 𝐶) → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸)) → (𝑣 ∈ 𝑉 ∧ {𝐴, 𝑣} ∈ ran 𝐸))) |
114 | 113 | com12 32 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸)) → ((𝑣 = 𝐵 ∨ 𝑣 = 𝐶) → (𝑣 ∈ 𝑉 ∧ {𝐴, 𝑣} ∈ ran 𝐸))) |
115 | 63, 114 | impbid 201 |
. . . . 5
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸)) → ((𝑣 ∈ 𝑉 ∧ {𝐴, 𝑣} ∈ ran 𝐸) ↔ (𝑣 = 𝐵 ∨ 𝑣 = 𝐶))) |
116 | 115 | abbidv 2728 |
. . . 4
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸)) → {𝑣 ∣ (𝑣 ∈ 𝑉 ∧ {𝐴, 𝑣} ∈ ran 𝐸)} = {𝑣 ∣ (𝑣 = 𝐵 ∨ 𝑣 = 𝐶)}) |
117 | | df-rab 2905 |
. . . 4
⊢ {𝑣 ∈ 𝑉 ∣ {𝐴, 𝑣} ∈ ran 𝐸} = {𝑣 ∣ (𝑣 ∈ 𝑉 ∧ {𝐴, 𝑣} ∈ ran 𝐸)} |
118 | | dfpr2 4143 |
. . . 4
⊢ {𝐵, 𝐶} = {𝑣 ∣ (𝑣 = 𝐵 ∨ 𝑣 = 𝐶)} |
119 | 116, 117,
118 | 3eqtr4g 2669 |
. . 3
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸)) → {𝑣 ∈ 𝑉 ∣ {𝐴, 𝑣} ∈ ran 𝐸} = {𝐵, 𝐶}) |
120 | 36, 119 | eqtrd 2644 |
. 2
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸)) → (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶}) |
121 | 33, 120 | impbida 873 |
1
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) → ((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶} ↔ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸))) |