Step | Hyp | Ref
| Expression |
1 | | umgr2v2evtx.g |
. . . 4
⊢ 𝐺 = ⟨𝑉, {⟨0, {𝐴, 𝐵}⟩, ⟨1, {𝐴, 𝐵}⟩}⟩ |
2 | 1 | umgr2v2e 28515 |
. . 3
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → 𝐺 ∈ UMGraph) |
3 | 1 | umgr2v2evtxel 28512 |
. . . . 5
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉) → 𝐴 ∈ (Vtx‘𝐺)) |
4 | 3 | 3adant3 1133 |
. . . 4
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ (Vtx‘𝐺)) |
5 | 4 | adantr 482 |
. . 3
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → 𝐴 ∈ (Vtx‘𝐺)) |
6 | | eqid 2733 |
. . . 4
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
7 | | eqid 2733 |
. . . 4
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
8 | 6, 7 | nbumgrvtx 28336 |
. . 3
⊢ ((𝐺 ∈ UMGraph ∧ 𝐴 ∈ (Vtx‘𝐺)) → (𝐺 NeighbVtx 𝐴) = {𝑥 ∈ (Vtx‘𝐺) ∣ {𝐴, 𝑥} ∈ (Edg‘𝐺)}) |
9 | 2, 5, 8 | syl2anc 585 |
. 2
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → (𝐺 NeighbVtx 𝐴) = {𝑥 ∈ (Vtx‘𝐺) ∣ {𝐴, 𝑥} ∈ (Edg‘𝐺)}) |
10 | 1 | umgr2v2eedg 28514 |
. . . . . . . . . . 11
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (Edg‘𝐺) = {{𝐴, 𝐵}}) |
11 | 10 | eleq2d 2820 |
. . . . . . . . . 10
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ({𝐴, 𝑥} ∈ (Edg‘𝐺) ↔ {𝐴, 𝑥} ∈ {{𝐴, 𝐵}})) |
12 | 11 | adantr 482 |
. . . . . . . . 9
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → ({𝐴, 𝑥} ∈ (Edg‘𝐺) ↔ {𝐴, 𝑥} ∈ {{𝐴, 𝐵}})) |
13 | 12 | adantr 482 |
. . . . . . . 8
⊢ ((((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) ∧ 𝑥 ∈ (Vtx‘𝐺)) → ({𝐴, 𝑥} ∈ (Edg‘𝐺) ↔ {𝐴, 𝑥} ∈ {{𝐴, 𝐵}})) |
14 | | prex 5390 |
. . . . . . . . 9
⊢ {𝐴, 𝑥} ∈ V |
15 | 14 | elsn 4602 |
. . . . . . . 8
⊢ ({𝐴, 𝑥} ∈ {{𝐴, 𝐵}} ↔ {𝐴, 𝑥} = {𝐴, 𝐵}) |
16 | 13, 15 | bitrdi 287 |
. . . . . . 7
⊢ ((((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) ∧ 𝑥 ∈ (Vtx‘𝐺)) → ({𝐴, 𝑥} ∈ (Edg‘𝐺) ↔ {𝐴, 𝑥} = {𝐴, 𝐵})) |
17 | | simpr 486 |
. . . . . . . 8
⊢ ((((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) ∧ 𝑥 ∈ (Vtx‘𝐺)) → 𝑥 ∈ (Vtx‘𝐺)) |
18 | | simpll3 1215 |
. . . . . . . 8
⊢ ((((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) ∧ 𝑥 ∈ (Vtx‘𝐺)) → 𝐵 ∈ 𝑉) |
19 | 17, 18 | preq2b 4806 |
. . . . . . 7
⊢ ((((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) ∧ 𝑥 ∈ (Vtx‘𝐺)) → ({𝐴, 𝑥} = {𝐴, 𝐵} ↔ 𝑥 = 𝐵)) |
20 | 16, 19 | bitrd 279 |
. . . . . 6
⊢ ((((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) ∧ 𝑥 ∈ (Vtx‘𝐺)) → ({𝐴, 𝑥} ∈ (Edg‘𝐺) ↔ 𝑥 = 𝐵)) |
21 | 20 | pm5.32da 580 |
. . . . 5
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → ((𝑥 ∈ (Vtx‘𝐺) ∧ {𝐴, 𝑥} ∈ (Edg‘𝐺)) ↔ (𝑥 ∈ (Vtx‘𝐺) ∧ 𝑥 = 𝐵))) |
22 | 1 | umgr2v2evtx 28511 |
. . . . . . . . 9
⊢ (𝑉 ∈ 𝑊 → (Vtx‘𝐺) = 𝑉) |
23 | 22 | 3ad2ant1 1134 |
. . . . . . . 8
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (Vtx‘𝐺) = 𝑉) |
24 | | eleq12 2824 |
. . . . . . . . . . 11
⊢ ((𝑥 = 𝐵 ∧ (Vtx‘𝐺) = 𝑉) → (𝑥 ∈ (Vtx‘𝐺) ↔ 𝐵 ∈ 𝑉)) |
25 | 24 | exbiri 810 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐵 → ((Vtx‘𝐺) = 𝑉 → (𝐵 ∈ 𝑉 → 𝑥 ∈ (Vtx‘𝐺)))) |
26 | 25 | com13 88 |
. . . . . . . . 9
⊢ (𝐵 ∈ 𝑉 → ((Vtx‘𝐺) = 𝑉 → (𝑥 = 𝐵 → 𝑥 ∈ (Vtx‘𝐺)))) |
27 | 26 | 3ad2ant3 1136 |
. . . . . . . 8
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ((Vtx‘𝐺) = 𝑉 → (𝑥 = 𝐵 → 𝑥 ∈ (Vtx‘𝐺)))) |
28 | 23, 27 | mpd 15 |
. . . . . . 7
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝑥 = 𝐵 → 𝑥 ∈ (Vtx‘𝐺))) |
29 | 28 | adantr 482 |
. . . . . 6
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → (𝑥 = 𝐵 → 𝑥 ∈ (Vtx‘𝐺))) |
30 | 29 | pm4.71rd 564 |
. . . . 5
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → (𝑥 = 𝐵 ↔ (𝑥 ∈ (Vtx‘𝐺) ∧ 𝑥 = 𝐵))) |
31 | 21, 30 | bitr4d 282 |
. . . 4
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → ((𝑥 ∈ (Vtx‘𝐺) ∧ {𝐴, 𝑥} ∈ (Edg‘𝐺)) ↔ 𝑥 = 𝐵)) |
32 | 31 | alrimiv 1931 |
. . 3
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → ∀𝑥((𝑥 ∈ (Vtx‘𝐺) ∧ {𝐴, 𝑥} ∈ (Edg‘𝐺)) ↔ 𝑥 = 𝐵)) |
33 | | rabeqsn 4628 |
. . 3
⊢ ({𝑥 ∈ (Vtx‘𝐺) ∣ {𝐴, 𝑥} ∈ (Edg‘𝐺)} = {𝐵} ↔ ∀𝑥((𝑥 ∈ (Vtx‘𝐺) ∧ {𝐴, 𝑥} ∈ (Edg‘𝐺)) ↔ 𝑥 = 𝐵)) |
34 | 32, 33 | sylibr 233 |
. 2
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → {𝑥 ∈ (Vtx‘𝐺) ∣ {𝐴, 𝑥} ∈ (Edg‘𝐺)} = {𝐵}) |
35 | 9, 34 | eqtrd 2773 |
1
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → (𝐺 NeighbVtx 𝐴) = {𝐵}) |