Proof of Theorem dfvopnbgr2
| Step | Hyp | Ref
| Expression |
| 1 | | dfvopnbgr2.u |
. 2
⊢ 𝑈 = {𝑛 ∈ 𝑉 ∣ (𝑛 ∈ (𝐺 NeighbVtx 𝑁) ∨ ∃𝑒 ∈ 𝐸 (𝑁 = 𝑛 ∧ 𝑒 = {𝑁}))} |
| 2 | | dfvopnbgr2.v |
. . . . . . . 8
⊢ 𝑉 = (Vtx‘𝐺) |
| 3 | | dfvopnbgr2.e |
. . . . . . . 8
⊢ 𝐸 = (Edg‘𝐺) |
| 4 | 2, 3 | nbgrel 29357 |
. . . . . . 7
⊢ (𝑛 ∈ (𝐺 NeighbVtx 𝑁) ↔ ((𝑛 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ 𝑛 ≠ 𝑁 ∧ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒)) |
| 5 | 4 | a1i 11 |
. . . . . 6
⊢ ((𝑁 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉) → (𝑛 ∈ (𝐺 NeighbVtx 𝑁) ↔ ((𝑛 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ 𝑛 ≠ 𝑁 ∧ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒))) |
| 6 | 5 | orbi1d 917 |
. . . . 5
⊢ ((𝑁 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉) → ((𝑛 ∈ (𝐺 NeighbVtx 𝑁) ∨ ∃𝑒 ∈ 𝐸 (𝑁 = 𝑛 ∧ 𝑒 = {𝑁})) ↔ (((𝑛 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ 𝑛 ≠ 𝑁 ∧ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒) ∨ ∃𝑒 ∈ 𝐸 (𝑁 = 𝑛 ∧ 𝑒 = {𝑁})))) |
| 7 | | df-3an 1089 |
. . . . . . . . 9
⊢ (((𝑛 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ 𝑛 ≠ 𝑁 ∧ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒) ↔ (((𝑛 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ 𝑛 ≠ 𝑁) ∧ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒)) |
| 8 | | r19.42v 3191 |
. . . . . . . . 9
⊢
(∃𝑒 ∈
𝐸 (((𝑛 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ 𝑛 ≠ 𝑁) ∧ {𝑁, 𝑛} ⊆ 𝑒) ↔ (((𝑛 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ 𝑛 ≠ 𝑁) ∧ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒)) |
| 9 | 7, 8 | bitr4i 278 |
. . . . . . . 8
⊢ (((𝑛 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ 𝑛 ≠ 𝑁 ∧ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒) ↔ ∃𝑒 ∈ 𝐸 (((𝑛 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ 𝑛 ≠ 𝑁) ∧ {𝑁, 𝑛} ⊆ 𝑒)) |
| 10 | 9 | orbi1i 914 |
. . . . . . 7
⊢ ((((𝑛 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ 𝑛 ≠ 𝑁 ∧ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒) ∨ ∃𝑒 ∈ 𝐸 (𝑁 = 𝑛 ∧ 𝑒 = {𝑁})) ↔ (∃𝑒 ∈ 𝐸 (((𝑛 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ 𝑛 ≠ 𝑁) ∧ {𝑁, 𝑛} ⊆ 𝑒) ∨ ∃𝑒 ∈ 𝐸 (𝑁 = 𝑛 ∧ 𝑒 = {𝑁}))) |
| 11 | 10 | a1i 11 |
. . . . . 6
⊢ ((𝑁 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉) → ((((𝑛 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ 𝑛 ≠ 𝑁 ∧ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒) ∨ ∃𝑒 ∈ 𝐸 (𝑁 = 𝑛 ∧ 𝑒 = {𝑁})) ↔ (∃𝑒 ∈ 𝐸 (((𝑛 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ 𝑛 ≠ 𝑁) ∧ {𝑁, 𝑛} ⊆ 𝑒) ∨ ∃𝑒 ∈ 𝐸 (𝑁 = 𝑛 ∧ 𝑒 = {𝑁})))) |
| 12 | | r19.43 3122 |
. . . . . 6
⊢
(∃𝑒 ∈
𝐸 ((((𝑛 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ 𝑛 ≠ 𝑁) ∧ {𝑁, 𝑛} ⊆ 𝑒) ∨ (𝑁 = 𝑛 ∧ 𝑒 = {𝑁})) ↔ (∃𝑒 ∈ 𝐸 (((𝑛 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ 𝑛 ≠ 𝑁) ∧ {𝑁, 𝑛} ⊆ 𝑒) ∨ ∃𝑒 ∈ 𝐸 (𝑁 = 𝑛 ∧ 𝑒 = {𝑁}))) |
| 13 | 11, 12 | bitr4di 289 |
. . . . 5
⊢ ((𝑁 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉) → ((((𝑛 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ 𝑛 ≠ 𝑁 ∧ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒) ∨ ∃𝑒 ∈ 𝐸 (𝑁 = 𝑛 ∧ 𝑒 = {𝑁})) ↔ ∃𝑒 ∈ 𝐸 ((((𝑛 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ 𝑛 ≠ 𝑁) ∧ {𝑁, 𝑛} ⊆ 𝑒) ∨ (𝑁 = 𝑛 ∧ 𝑒 = {𝑁})))) |
| 14 | 6, 13 | bitrd 279 |
. . . 4
⊢ ((𝑁 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉) → ((𝑛 ∈ (𝐺 NeighbVtx 𝑁) ∨ ∃𝑒 ∈ 𝐸 (𝑁 = 𝑛 ∧ 𝑒 = {𝑁})) ↔ ∃𝑒 ∈ 𝐸 ((((𝑛 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ 𝑛 ≠ 𝑁) ∧ {𝑁, 𝑛} ⊆ 𝑒) ∨ (𝑁 = 𝑛 ∧ 𝑒 = {𝑁})))) |
| 15 | | anass 468 |
. . . . . . . 8
⊢ ((((𝑛 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ 𝑛 ≠ 𝑁) ∧ {𝑁, 𝑛} ⊆ 𝑒) ↔ ((𝑛 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ (𝑛 ≠ 𝑁 ∧ {𝑁, 𝑛} ⊆ 𝑒))) |
| 16 | 15 | a1i 11 |
. . . . . . 7
⊢ (((𝑁 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉) ∧ 𝑒 ∈ 𝐸) → ((((𝑛 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ 𝑛 ≠ 𝑁) ∧ {𝑁, 𝑛} ⊆ 𝑒) ↔ ((𝑛 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ (𝑛 ≠ 𝑁 ∧ {𝑁, 𝑛} ⊆ 𝑒)))) |
| 17 | | ibar 528 |
. . . . . . . . 9
⊢ ((𝑛 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) → ((𝑛 ≠ 𝑁 ∧ {𝑁, 𝑛} ⊆ 𝑒) ↔ ((𝑛 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ (𝑛 ≠ 𝑁 ∧ {𝑁, 𝑛} ⊆ 𝑒)))) |
| 18 | 17 | ancoms 458 |
. . . . . . . 8
⊢ ((𝑁 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉) → ((𝑛 ≠ 𝑁 ∧ {𝑁, 𝑛} ⊆ 𝑒) ↔ ((𝑛 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ (𝑛 ≠ 𝑁 ∧ {𝑁, 𝑛} ⊆ 𝑒)))) |
| 19 | 18 | adantr 480 |
. . . . . . 7
⊢ (((𝑁 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉) ∧ 𝑒 ∈ 𝐸) → ((𝑛 ≠ 𝑁 ∧ {𝑁, 𝑛} ⊆ 𝑒) ↔ ((𝑛 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ (𝑛 ≠ 𝑁 ∧ {𝑁, 𝑛} ⊆ 𝑒)))) |
| 20 | | prssg 4819 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉) → ((𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒) ↔ {𝑁, 𝑛} ⊆ 𝑒)) |
| 21 | 20 | bicomd 223 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉) → ({𝑁, 𝑛} ⊆ 𝑒 ↔ (𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒))) |
| 22 | 21 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑁 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉) ∧ 𝑒 ∈ 𝐸) → ({𝑁, 𝑛} ⊆ 𝑒 ↔ (𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒))) |
| 23 | 22 | anbi2d 630 |
. . . . . . . 8
⊢ (((𝑁 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉) ∧ 𝑒 ∈ 𝐸) → ((𝑛 ≠ 𝑁 ∧ {𝑁, 𝑛} ⊆ 𝑒) ↔ (𝑛 ≠ 𝑁 ∧ (𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒)))) |
| 24 | | 3anass 1095 |
. . . . . . . 8
⊢ ((𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒) ↔ (𝑛 ≠ 𝑁 ∧ (𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒))) |
| 25 | 23, 24 | bitr4di 289 |
. . . . . . 7
⊢ (((𝑁 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉) ∧ 𝑒 ∈ 𝐸) → ((𝑛 ≠ 𝑁 ∧ {𝑁, 𝑛} ⊆ 𝑒) ↔ (𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒))) |
| 26 | 16, 19, 25 | 3bitr2d 307 |
. . . . . 6
⊢ (((𝑁 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉) ∧ 𝑒 ∈ 𝐸) → ((((𝑛 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ 𝑛 ≠ 𝑁) ∧ {𝑁, 𝑛} ⊆ 𝑒) ↔ (𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒))) |
| 27 | | eqcom 2744 |
. . . . . . . . 9
⊢ (𝑁 = 𝑛 ↔ 𝑛 = 𝑁) |
| 28 | 27 | anbi1i 624 |
. . . . . . . 8
⊢ ((𝑁 = 𝑛 ∧ 𝑒 = {𝑁}) ↔ (𝑛 = 𝑁 ∧ 𝑒 = {𝑁})) |
| 29 | | sneq 4636 |
. . . . . . . . . . 11
⊢ (𝑁 = 𝑛 → {𝑁} = {𝑛}) |
| 30 | 29 | eqcoms 2745 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑁 → {𝑁} = {𝑛}) |
| 31 | 30 | eqeq2d 2748 |
. . . . . . . . 9
⊢ (𝑛 = 𝑁 → (𝑒 = {𝑁} ↔ 𝑒 = {𝑛})) |
| 32 | 31 | pm5.32i 574 |
. . . . . . . 8
⊢ ((𝑛 = 𝑁 ∧ 𝑒 = {𝑁}) ↔ (𝑛 = 𝑁 ∧ 𝑒 = {𝑛})) |
| 33 | 28, 32 | bitri 275 |
. . . . . . 7
⊢ ((𝑁 = 𝑛 ∧ 𝑒 = {𝑁}) ↔ (𝑛 = 𝑁 ∧ 𝑒 = {𝑛})) |
| 34 | 33 | a1i 11 |
. . . . . 6
⊢ (((𝑁 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉) ∧ 𝑒 ∈ 𝐸) → ((𝑁 = 𝑛 ∧ 𝑒 = {𝑁}) ↔ (𝑛 = 𝑁 ∧ 𝑒 = {𝑛}))) |
| 35 | 26, 34 | orbi12d 919 |
. . . . 5
⊢ (((𝑁 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉) ∧ 𝑒 ∈ 𝐸) → (((((𝑛 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ 𝑛 ≠ 𝑁) ∧ {𝑁, 𝑛} ⊆ 𝑒) ∨ (𝑁 = 𝑛 ∧ 𝑒 = {𝑁})) ↔ ((𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒) ∨ (𝑛 = 𝑁 ∧ 𝑒 = {𝑛})))) |
| 36 | 35 | rexbidva 3177 |
. . . 4
⊢ ((𝑁 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉) → (∃𝑒 ∈ 𝐸 ((((𝑛 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ 𝑛 ≠ 𝑁) ∧ {𝑁, 𝑛} ⊆ 𝑒) ∨ (𝑁 = 𝑛 ∧ 𝑒 = {𝑁})) ↔ ∃𝑒 ∈ 𝐸 ((𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒) ∨ (𝑛 = 𝑁 ∧ 𝑒 = {𝑛})))) |
| 37 | 14, 36 | bitrd 279 |
. . 3
⊢ ((𝑁 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉) → ((𝑛 ∈ (𝐺 NeighbVtx 𝑁) ∨ ∃𝑒 ∈ 𝐸 (𝑁 = 𝑛 ∧ 𝑒 = {𝑁})) ↔ ∃𝑒 ∈ 𝐸 ((𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒) ∨ (𝑛 = 𝑁 ∧ 𝑒 = {𝑛})))) |
| 38 | 37 | rabbidva 3443 |
. 2
⊢ (𝑁 ∈ 𝑉 → {𝑛 ∈ 𝑉 ∣ (𝑛 ∈ (𝐺 NeighbVtx 𝑁) ∨ ∃𝑒 ∈ 𝐸 (𝑁 = 𝑛 ∧ 𝑒 = {𝑁}))} = {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 ((𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒) ∨ (𝑛 = 𝑁 ∧ 𝑒 = {𝑛}))}) |
| 39 | 1, 38 | eqtrid 2789 |
1
⊢ (𝑁 ∈ 𝑉 → 𝑈 = {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 ((𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒) ∨ (𝑛 = 𝑁 ∧ 𝑒 = {𝑛}))}) |