| Step | Hyp | Ref
| Expression |
|---|
| 1 | | nbuhgr.v |
. . . 4
⊢ 𝑉 = (Vtx‘𝐺) |
| 2 | | nbuhgr.e |
. . . 4
⊢ 𝐸 = (Edg‘𝐺) |
| 3 | 1, 2 | nbgrval 29923 |
. . 3
⊢ (𝑁 ∈ 𝑉 → (𝐺 NeighbVtx 𝑁) = {𝑛 ∈ (𝑉 ∖ {𝑁}) ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒}) |
| 4 | 3 | adantl 487 |
. 2
⊢ ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) → (𝐺 NeighbVtx 𝑁) = {𝑛 ∈ (𝑉 ∖ {𝑁}) ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒}) |
| 5 | | simp-4l 795 |
. . . . . . . 8
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑁 ∈
𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑁})) ∧ 𝑒 ∈ 𝐸) ∧ {𝑁, 𝑛} ⊆ 𝑒) → 𝐺 ∈ UPGraph) |
| 6 | | simpr 490 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑁})) ∧ 𝑒 ∈ 𝐸) → 𝑒 ∈ 𝐸) |
| 7 | 6 | adantr 486 |
. . . . . . . 8
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑁 ∈
𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑁})) ∧ 𝑒 ∈ 𝐸) ∧ {𝑁, 𝑛} ⊆ 𝑒) → 𝑒 ∈ 𝐸) |
| 8 | | simpr 490 |
. . . . . . . 8
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑁 ∈
𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑁})) ∧ 𝑒 ∈ 𝐸) ∧ {𝑁, 𝑛} ⊆ 𝑒) → {𝑁, 𝑛} ⊆ 𝑒) |
| 9 | | simpr 490 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) → 𝑁 ∈ 𝑉) |
| 10 | 9 | adantr 486 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑁})) → 𝑁 ∈ 𝑉) |
| 11 | | vex 3454 |
. . . . . . . . . . . 12
⊢ 𝑛 ∈ V |
| 12 | 11 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑁})) → 𝑛 ∈ V) |
| 13 | | eldifsn 4744 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ (𝑉 ∖ {𝑁}) ↔ (𝑛 ∈ 𝑉 ∧ 𝑛 ≠ 𝑁)) |
| 14 | | simpr 490 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ 𝑉 ∧ 𝑛 ≠ 𝑁) → 𝑛 ≠ 𝑁) |
| 15 | 14 | necomd 3010 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ 𝑉 ∧ 𝑛 ≠ 𝑁) → 𝑁 ≠ 𝑛) |
| 16 | 13, 15 | sylbi 220 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ (𝑉 ∖ {𝑁}) → 𝑁 ≠ 𝑛) |
| 17 | 16 | adantl 487 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑁})) → 𝑁 ≠ 𝑛) |
| 18 | 10, 12, 17 | 3jca 1146 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑁})) → (𝑁 ∈ 𝑉 ∧ 𝑛 ∈ V ∧ 𝑁 ≠ 𝑛)) |
| 19 | 18 | adantr 486 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑁})) ∧ 𝑒 ∈ 𝐸) → (𝑁 ∈ 𝑉 ∧ 𝑛 ∈ V ∧ 𝑁 ≠ 𝑛)) |
| 20 | 19 | adantr 486 |
. . . . . . . 8
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑁 ∈
𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑁})) ∧ 𝑒 ∈ 𝐸) ∧ {𝑁, 𝑛} ⊆ 𝑒) → (𝑁 ∈ 𝑉 ∧ 𝑛 ∈ V ∧ 𝑁 ≠ 𝑛)) |
| 21 | 1, 2 | upgredgpr 29726 |
. . . . . . . 8
⊢ (((𝐺 ∈ UPGraph ∧ 𝑒 ∈ 𝐸 ∧ {𝑁, 𝑛} ⊆ 𝑒) ∧ (𝑁 ∈ 𝑉 ∧ 𝑛 ∈ V ∧ 𝑁 ≠ 𝑛)) → {𝑁, 𝑛} = 𝑒) |
| 22 | 5, 7, 8, 20, 21 | syl31anc 1400 |
. . . . . . 7
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑁 ∈
𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑁})) ∧ 𝑒 ∈ 𝐸) ∧ {𝑁, 𝑛} ⊆ 𝑒) → {𝑁, 𝑛} = 𝑒) |
| 23 | 22 | ex 418 |
. . . . . 6
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑁})) ∧ 𝑒 ∈ 𝐸) → ({𝑁, 𝑛} ⊆ 𝑒 → {𝑁, 𝑛} = 𝑒)) |
| 24 | | eleq1 2848 |
. . . . . . 7
⊢ ({𝑁, 𝑛} = 𝑒 → ({𝑁, 𝑛} ∈ 𝐸 ↔ 𝑒 ∈ 𝐸)) |
| 25 | 24 | biimprd 251 |
. . . . . 6
⊢ ({𝑁, 𝑛} = 𝑒 → (𝑒 ∈ 𝐸 → {𝑁, 𝑛} ∈ 𝐸)) |
| 26 | 23, 6, 25 | syl6ci 72 |
. . . . 5
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑁})) ∧ 𝑒 ∈ 𝐸) → ({𝑁, 𝑛} ⊆ 𝑒 → {𝑁, 𝑛} ∈ 𝐸)) |
| 27 | 26 | rexlimdva 3163 |
. . . 4
⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑁})) → (∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒 → {𝑁, 𝑛} ∈ 𝐸)) |
| 28 | | simpr 490 |
. . . . . 6
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑁})) ∧ {𝑁, 𝑛} ∈ 𝐸) → {𝑁, 𝑛} ∈ 𝐸) |
| 29 | | sseq2 3934 |
. . . . . . 7
⊢ (𝑒 = {𝑁, 𝑛} → ({𝑁, 𝑛} ⊆ 𝑒 ↔ {𝑁, 𝑛} ⊆ {𝑁, 𝑛})) |
| 30 | 29 | adantl 487 |
. . . . . 6
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑁 ∈
𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑁})) ∧ {𝑁, 𝑛} ∈ 𝐸) ∧ 𝑒 = {𝑁, 𝑛}) → ({𝑁, 𝑛} ⊆ 𝑒 ↔ {𝑁, 𝑛} ⊆ {𝑁, 𝑛})) |
| 31 | | ssidd 3931 |
. . . . . 6
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑁})) ∧ {𝑁, 𝑛} ∈ 𝐸) → {𝑁, 𝑛} ⊆ {𝑁, 𝑛}) |
| 32 | 28, 30, 31 | rspcedvd 3578 |
. . . . 5
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑁})) ∧ {𝑁, 𝑛} ∈ 𝐸) → ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒) |
| 33 | 32 | ex 418 |
. . . 4
⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑁})) → ({𝑁, 𝑛} ∈ 𝐸 → ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒)) |
| 34 | 27, 33 | impbid 215 |
. . 3
⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑁})) → (∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒 ↔ {𝑁, 𝑛} ∈ 𝐸)) |
| 35 | 34 | rabbidva 3418 |
. 2
⊢ ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) → {𝑛 ∈ (𝑉 ∖ {𝑁}) ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒} = {𝑛 ∈ (𝑉 ∖ {𝑁}) ∣ {𝑁, 𝑛} ∈ 𝐸}) |
| 36 | 4, 35 | eqtrd 2795 |
1
⊢ ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) → (𝐺 NeighbVtx 𝑁) = {𝑛 ∈ (𝑉 ∖ {𝑁}) ∣ {𝑁, 𝑛} ∈ 𝐸}) |
