Step | Hyp | Ref
| Expression |
1 | | nbgrcl 40559 |
. . . . 5
⊢ (𝐾 ∈ (𝐺 NeighbVtx 𝑁) → 𝑁 ∈ (Vtx‘𝐺)) |
2 | | nbgrel.v |
. . . . 5
⊢ 𝑉 = (Vtx‘𝐺) |
3 | 1, 2 | syl6eleqr 2699 |
. . . 4
⊢ (𝐾 ∈ (𝐺 NeighbVtx 𝑁) → 𝑁 ∈ 𝑉) |
4 | 3 | a1i 11 |
. . 3
⊢ (𝐺 ∈ 𝑊 → (𝐾 ∈ (𝐺 NeighbVtx 𝑁) → 𝑁 ∈ 𝑉)) |
5 | 4 | pm4.71rd 665 |
. 2
⊢ (𝐺 ∈ 𝑊 → (𝐾 ∈ (𝐺 NeighbVtx 𝑁) ↔ (𝑁 ∈ 𝑉 ∧ 𝐾 ∈ (𝐺 NeighbVtx 𝑁)))) |
6 | | nbgrel.e |
. . . . . . . 8
⊢ 𝐸 = (Edg‘𝐺) |
7 | 2, 6 | nbgrval 40560 |
. . . . . . 7
⊢ (𝑁 ∈ 𝑉 → (𝐺 NeighbVtx 𝑁) = {𝑘 ∈ (𝑉 ∖ {𝑁}) ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑘} ⊆ 𝑒}) |
8 | 7 | eleq2d 2673 |
. . . . . 6
⊢ (𝑁 ∈ 𝑉 → (𝐾 ∈ (𝐺 NeighbVtx 𝑁) ↔ 𝐾 ∈ {𝑘 ∈ (𝑉 ∖ {𝑁}) ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑘} ⊆ 𝑒})) |
9 | | preq2 4213 |
. . . . . . . . . 10
⊢ (𝑘 = 𝐾 → {𝑁, 𝑘} = {𝑁, 𝐾}) |
10 | 9 | sseq1d 3595 |
. . . . . . . . 9
⊢ (𝑘 = 𝐾 → ({𝑁, 𝑘} ⊆ 𝑒 ↔ {𝑁, 𝐾} ⊆ 𝑒)) |
11 | 10 | rexbidv 3034 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 → (∃𝑒 ∈ 𝐸 {𝑁, 𝑘} ⊆ 𝑒 ↔ ∃𝑒 ∈ 𝐸 {𝑁, 𝐾} ⊆ 𝑒)) |
12 | 11 | elrab 3331 |
. . . . . . 7
⊢ (𝐾 ∈ {𝑘 ∈ (𝑉 ∖ {𝑁}) ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑘} ⊆ 𝑒} ↔ (𝐾 ∈ (𝑉 ∖ {𝑁}) ∧ ∃𝑒 ∈ 𝐸 {𝑁, 𝐾} ⊆ 𝑒)) |
13 | | eldifsn 4260 |
. . . . . . . 8
⊢ (𝐾 ∈ (𝑉 ∖ {𝑁}) ↔ (𝐾 ∈ 𝑉 ∧ 𝐾 ≠ 𝑁)) |
14 | 13 | anbi1i 727 |
. . . . . . 7
⊢ ((𝐾 ∈ (𝑉 ∖ {𝑁}) ∧ ∃𝑒 ∈ 𝐸 {𝑁, 𝐾} ⊆ 𝑒) ↔ ((𝐾 ∈ 𝑉 ∧ 𝐾 ≠ 𝑁) ∧ ∃𝑒 ∈ 𝐸 {𝑁, 𝐾} ⊆ 𝑒)) |
15 | | anass 679 |
. . . . . . 7
⊢ (((𝐾 ∈ 𝑉 ∧ 𝐾 ≠ 𝑁) ∧ ∃𝑒 ∈ 𝐸 {𝑁, 𝐾} ⊆ 𝑒) ↔ (𝐾 ∈ 𝑉 ∧ (𝐾 ≠ 𝑁 ∧ ∃𝑒 ∈ 𝐸 {𝑁, 𝐾} ⊆ 𝑒))) |
16 | 12, 14, 15 | 3bitri 285 |
. . . . . 6
⊢ (𝐾 ∈ {𝑘 ∈ (𝑉 ∖ {𝑁}) ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑘} ⊆ 𝑒} ↔ (𝐾 ∈ 𝑉 ∧ (𝐾 ≠ 𝑁 ∧ ∃𝑒 ∈ 𝐸 {𝑁, 𝐾} ⊆ 𝑒))) |
17 | 8, 16 | syl6bb 275 |
. . . . 5
⊢ (𝑁 ∈ 𝑉 → (𝐾 ∈ (𝐺 NeighbVtx 𝑁) ↔ (𝐾 ∈ 𝑉 ∧ (𝐾 ≠ 𝑁 ∧ ∃𝑒 ∈ 𝐸 {𝑁, 𝐾} ⊆ 𝑒)))) |
18 | 17 | adantl 481 |
. . . 4
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑁 ∈ 𝑉) → (𝐾 ∈ (𝐺 NeighbVtx 𝑁) ↔ (𝐾 ∈ 𝑉 ∧ (𝐾 ≠ 𝑁 ∧ ∃𝑒 ∈ 𝐸 {𝑁, 𝐾} ⊆ 𝑒)))) |
19 | 18 | pm5.32da 671 |
. . 3
⊢ (𝐺 ∈ 𝑊 → ((𝑁 ∈ 𝑉 ∧ 𝐾 ∈ (𝐺 NeighbVtx 𝑁)) ↔ (𝑁 ∈ 𝑉 ∧ (𝐾 ∈ 𝑉 ∧ (𝐾 ≠ 𝑁 ∧ ∃𝑒 ∈ 𝐸 {𝑁, 𝐾} ⊆ 𝑒))))) |
20 | | 3anass 1035 |
. . . 4
⊢ (((𝐾 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ≠ 𝑁 ∧ ∃𝑒 ∈ 𝐸 {𝑁, 𝐾} ⊆ 𝑒) ↔ ((𝐾 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ (𝐾 ≠ 𝑁 ∧ ∃𝑒 ∈ 𝐸 {𝑁, 𝐾} ⊆ 𝑒))) |
21 | | ancom 465 |
. . . . 5
⊢ ((𝐾 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ↔ (𝑁 ∈ 𝑉 ∧ 𝐾 ∈ 𝑉)) |
22 | 21 | anbi1i 727 |
. . . 4
⊢ (((𝐾 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ (𝐾 ≠ 𝑁 ∧ ∃𝑒 ∈ 𝐸 {𝑁, 𝐾} ⊆ 𝑒)) ↔ ((𝑁 ∈ 𝑉 ∧ 𝐾 ∈ 𝑉) ∧ (𝐾 ≠ 𝑁 ∧ ∃𝑒 ∈ 𝐸 {𝑁, 𝐾} ⊆ 𝑒))) |
23 | | anass 679 |
. . . 4
⊢ (((𝑁 ∈ 𝑉 ∧ 𝐾 ∈ 𝑉) ∧ (𝐾 ≠ 𝑁 ∧ ∃𝑒 ∈ 𝐸 {𝑁, 𝐾} ⊆ 𝑒)) ↔ (𝑁 ∈ 𝑉 ∧ (𝐾 ∈ 𝑉 ∧ (𝐾 ≠ 𝑁 ∧ ∃𝑒 ∈ 𝐸 {𝑁, 𝐾} ⊆ 𝑒)))) |
24 | 20, 22, 23 | 3bitrri 286 |
. . 3
⊢ ((𝑁 ∈ 𝑉 ∧ (𝐾 ∈ 𝑉 ∧ (𝐾 ≠ 𝑁 ∧ ∃𝑒 ∈ 𝐸 {𝑁, 𝐾} ⊆ 𝑒))) ↔ ((𝐾 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ≠ 𝑁 ∧ ∃𝑒 ∈ 𝐸 {𝑁, 𝐾} ⊆ 𝑒)) |
25 | 19, 24 | syl6bb 275 |
. 2
⊢ (𝐺 ∈ 𝑊 → ((𝑁 ∈ 𝑉 ∧ 𝐾 ∈ (𝐺 NeighbVtx 𝑁)) ↔ ((𝐾 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ≠ 𝑁 ∧ ∃𝑒 ∈ 𝐸 {𝑁, 𝐾} ⊆ 𝑒))) |
26 | 5, 25 | bitrd 267 |
1
⊢ (𝐺 ∈ 𝑊 → (𝐾 ∈ (𝐺 NeighbVtx 𝑁) ↔ ((𝐾 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ≠ 𝑁 ∧ ∃𝑒 ∈ 𝐸 {𝑁, 𝐾} ⊆ 𝑒))) |