Step | Hyp | Ref
| Expression |
1 | | nbgr2vtx1edg.v |
. . . 4
⊢ 𝑉 = (Vtx‘𝐺) |
2 | | nbgr2vtx1edg.e |
. . . 4
⊢ 𝐸 = (Edg‘𝐺) |
3 | 1, 2 | nbgrel 27274 |
. . 3
⊢ (𝑎 ∈ (𝐺 NeighbVtx 𝑏) ↔ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑎 ≠ 𝑏 ∧ ∃𝑒 ∈ 𝐸 {𝑏, 𝑎} ⊆ 𝑒)) |
4 | 2 | eleq2i 2824 |
. . . . . . . . . 10
⊢ (𝑒 ∈ 𝐸 ↔ 𝑒 ∈ (Edg‘𝐺)) |
5 | | edguhgr 27066 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ UHGraph ∧ 𝑒 ∈ (Edg‘𝐺)) → 𝑒 ∈ 𝒫 (Vtx‘𝐺)) |
6 | 4, 5 | sylan2b 597 |
. . . . . . . . 9
⊢ ((𝐺 ∈ UHGraph ∧ 𝑒 ∈ 𝐸) → 𝑒 ∈ 𝒫 (Vtx‘𝐺)) |
7 | 1 | eqeq1i 2743 |
. . . . . . . . . . . . 13
⊢ (𝑉 = {𝑎, 𝑏} ↔ (Vtx‘𝐺) = {𝑎, 𝑏}) |
8 | | pweq 4501 |
. . . . . . . . . . . . . . 15
⊢
((Vtx‘𝐺) =
{𝑎, 𝑏} → 𝒫 (Vtx‘𝐺) = 𝒫 {𝑎, 𝑏}) |
9 | 8 | eleq2d 2818 |
. . . . . . . . . . . . . 14
⊢
((Vtx‘𝐺) =
{𝑎, 𝑏} → (𝑒 ∈ 𝒫 (Vtx‘𝐺) ↔ 𝑒 ∈ 𝒫 {𝑎, 𝑏})) |
10 | | velpw 4490 |
. . . . . . . . . . . . . 14
⊢ (𝑒 ∈ 𝒫 {𝑎, 𝑏} ↔ 𝑒 ⊆ {𝑎, 𝑏}) |
11 | 9, 10 | bitrdi 290 |
. . . . . . . . . . . . 13
⊢
((Vtx‘𝐺) =
{𝑎, 𝑏} → (𝑒 ∈ 𝒫 (Vtx‘𝐺) ↔ 𝑒 ⊆ {𝑎, 𝑏})) |
12 | 7, 11 | sylbi 220 |
. . . . . . . . . . . 12
⊢ (𝑉 = {𝑎, 𝑏} → (𝑒 ∈ 𝒫 (Vtx‘𝐺) ↔ 𝑒 ⊆ {𝑎, 𝑏})) |
13 | 12 | adantl 485 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ UHGraph ∧ 𝑒 ∈ 𝐸) ∧ 𝑉 = {𝑎, 𝑏}) → (𝑒 ∈ 𝒫 (Vtx‘𝐺) ↔ 𝑒 ⊆ {𝑎, 𝑏})) |
14 | | prcom 4620 |
. . . . . . . . . . . . . . 15
⊢ {𝑏, 𝑎} = {𝑎, 𝑏} |
15 | 14 | sseq1i 3903 |
. . . . . . . . . . . . . 14
⊢ ({𝑏, 𝑎} ⊆ 𝑒 ↔ {𝑎, 𝑏} ⊆ 𝑒) |
16 | | eqss 3890 |
. . . . . . . . . . . . . . . 16
⊢ ({𝑎, 𝑏} = 𝑒 ↔ ({𝑎, 𝑏} ⊆ 𝑒 ∧ 𝑒 ⊆ {𝑎, 𝑏})) |
17 | | eleq1a 2828 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑒 ∈ 𝐸 → ({𝑎, 𝑏} = 𝑒 → {𝑎, 𝑏} ∈ 𝐸)) |
18 | 17 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑎 ≠ 𝑏) → (𝑒 ∈ 𝐸 → ({𝑎, 𝑏} = 𝑒 → {𝑎, 𝑏} ∈ 𝐸))) |
19 | 18 | com13 88 |
. . . . . . . . . . . . . . . 16
⊢ ({𝑎, 𝑏} = 𝑒 → (𝑒 ∈ 𝐸 → (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑎 ≠ 𝑏) → {𝑎, 𝑏} ∈ 𝐸))) |
20 | 16, 19 | sylbir 238 |
. . . . . . . . . . . . . . 15
⊢ (({𝑎, 𝑏} ⊆ 𝑒 ∧ 𝑒 ⊆ {𝑎, 𝑏}) → (𝑒 ∈ 𝐸 → (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑎 ≠ 𝑏) → {𝑎, 𝑏} ∈ 𝐸))) |
21 | 20 | ex 416 |
. . . . . . . . . . . . . 14
⊢ ({𝑎, 𝑏} ⊆ 𝑒 → (𝑒 ⊆ {𝑎, 𝑏} → (𝑒 ∈ 𝐸 → (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑎 ≠ 𝑏) → {𝑎, 𝑏} ∈ 𝐸)))) |
22 | 15, 21 | sylbi 220 |
. . . . . . . . . . . . 13
⊢ ({𝑏, 𝑎} ⊆ 𝑒 → (𝑒 ⊆ {𝑎, 𝑏} → (𝑒 ∈ 𝐸 → (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑎 ≠ 𝑏) → {𝑎, 𝑏} ∈ 𝐸)))) |
23 | 22 | com13 88 |
. . . . . . . . . . . 12
⊢ (𝑒 ∈ 𝐸 → (𝑒 ⊆ {𝑎, 𝑏} → ({𝑏, 𝑎} ⊆ 𝑒 → (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑎 ≠ 𝑏) → {𝑎, 𝑏} ∈ 𝐸)))) |
24 | 23 | ad2antlr 727 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ UHGraph ∧ 𝑒 ∈ 𝐸) ∧ 𝑉 = {𝑎, 𝑏}) → (𝑒 ⊆ {𝑎, 𝑏} → ({𝑏, 𝑎} ⊆ 𝑒 → (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑎 ≠ 𝑏) → {𝑎, 𝑏} ∈ 𝐸)))) |
25 | 13, 24 | sylbid 243 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ UHGraph ∧ 𝑒 ∈ 𝐸) ∧ 𝑉 = {𝑎, 𝑏}) → (𝑒 ∈ 𝒫 (Vtx‘𝐺) → ({𝑏, 𝑎} ⊆ 𝑒 → (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑎 ≠ 𝑏) → {𝑎, 𝑏} ∈ 𝐸)))) |
26 | 25 | ex 416 |
. . . . . . . . 9
⊢ ((𝐺 ∈ UHGraph ∧ 𝑒 ∈ 𝐸) → (𝑉 = {𝑎, 𝑏} → (𝑒 ∈ 𝒫 (Vtx‘𝐺) → ({𝑏, 𝑎} ⊆ 𝑒 → (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑎 ≠ 𝑏) → {𝑎, 𝑏} ∈ 𝐸))))) |
27 | 6, 26 | mpid 44 |
. . . . . . . 8
⊢ ((𝐺 ∈ UHGraph ∧ 𝑒 ∈ 𝐸) → (𝑉 = {𝑎, 𝑏} → ({𝑏, 𝑎} ⊆ 𝑒 → (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑎 ≠ 𝑏) → {𝑎, 𝑏} ∈ 𝐸)))) |
28 | 27 | impancom 455 |
. . . . . . 7
⊢ ((𝐺 ∈ UHGraph ∧ 𝑉 = {𝑎, 𝑏}) → (𝑒 ∈ 𝐸 → ({𝑏, 𝑎} ⊆ 𝑒 → (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑎 ≠ 𝑏) → {𝑎, 𝑏} ∈ 𝐸)))) |
29 | 28 | com14 96 |
. . . . . 6
⊢ (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑎 ≠ 𝑏) → (𝑒 ∈ 𝐸 → ({𝑏, 𝑎} ⊆ 𝑒 → ((𝐺 ∈ UHGraph ∧ 𝑉 = {𝑎, 𝑏}) → {𝑎, 𝑏} ∈ 𝐸)))) |
30 | 29 | rexlimdv 3192 |
. . . . 5
⊢ (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑎 ≠ 𝑏) → (∃𝑒 ∈ 𝐸 {𝑏, 𝑎} ⊆ 𝑒 → ((𝐺 ∈ UHGraph ∧ 𝑉 = {𝑎, 𝑏}) → {𝑎, 𝑏} ∈ 𝐸))) |
31 | 30 | 3impia 1118 |
. . . 4
⊢ (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑎 ≠ 𝑏 ∧ ∃𝑒 ∈ 𝐸 {𝑏, 𝑎} ⊆ 𝑒) → ((𝐺 ∈ UHGraph ∧ 𝑉 = {𝑎, 𝑏}) → {𝑎, 𝑏} ∈ 𝐸)) |
32 | 31 | com12 32 |
. . 3
⊢ ((𝐺 ∈ UHGraph ∧ 𝑉 = {𝑎, 𝑏}) → (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑎 ≠ 𝑏 ∧ ∃𝑒 ∈ 𝐸 {𝑏, 𝑎} ⊆ 𝑒) → {𝑎, 𝑏} ∈ 𝐸)) |
33 | 3, 32 | syl5bi 245 |
. 2
⊢ ((𝐺 ∈ UHGraph ∧ 𝑉 = {𝑎, 𝑏}) → (𝑎 ∈ (𝐺 NeighbVtx 𝑏) → {𝑎, 𝑏} ∈ 𝐸)) |
34 | 33 | 3impia 1118 |
1
⊢ ((𝐺 ∈ UHGraph ∧ 𝑉 = {𝑎, 𝑏} ∧ 𝑎 ∈ (𝐺 NeighbVtx 𝑏)) → {𝑎, 𝑏} ∈ 𝐸) |