Proof of Theorem nbupgrres
| Step | Hyp | Ref
| Expression |
| 1 | | simp1l 1198 |
. . . . . 6
⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑀 ∈ (𝑉 ∖ {𝑁, 𝐾})) → 𝐺 ∈ UPGraph) |
| 2 | | eldifi 4131 |
. . . . . . 7
⊢ (𝐾 ∈ (𝑉 ∖ {𝑁}) → 𝐾 ∈ 𝑉) |
| 3 | 2 | 3ad2ant2 1135 |
. . . . . 6
⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑀 ∈ (𝑉 ∖ {𝑁, 𝐾})) → 𝐾 ∈ 𝑉) |
| 4 | | eldifsn 4786 |
. . . . . . . . 9
⊢ (𝑀 ∈ ((𝑉 ∖ {𝑁}) ∖ {𝐾}) ↔ (𝑀 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑀 ≠ 𝐾)) |
| 5 | | eldifi 4131 |
. . . . . . . . . 10
⊢ (𝑀 ∈ (𝑉 ∖ {𝑁}) → 𝑀 ∈ 𝑉) |
| 6 | 5 | anim1i 615 |
. . . . . . . . 9
⊢ ((𝑀 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑀 ≠ 𝐾) → (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝐾)) |
| 7 | 4, 6 | sylbi 217 |
. . . . . . . 8
⊢ (𝑀 ∈ ((𝑉 ∖ {𝑁}) ∖ {𝐾}) → (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝐾)) |
| 8 | | difpr 4803 |
. . . . . . . 8
⊢ (𝑉 ∖ {𝑁, 𝐾}) = ((𝑉 ∖ {𝑁}) ∖ {𝐾}) |
| 9 | 7, 8 | eleq2s 2859 |
. . . . . . 7
⊢ (𝑀 ∈ (𝑉 ∖ {𝑁, 𝐾}) → (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝐾)) |
| 10 | 9 | 3ad2ant3 1136 |
. . . . . 6
⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑀 ∈ (𝑉 ∖ {𝑁, 𝐾})) → (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝐾)) |
| 11 | | nbupgrres.v |
. . . . . . 7
⊢ 𝑉 = (Vtx‘𝐺) |
| 12 | | nbupgrres.e |
. . . . . . 7
⊢ 𝐸 = (Edg‘𝐺) |
| 13 | 11, 12 | nbupgrel 29362 |
. . . . . 6
⊢ (((𝐺 ∈ UPGraph ∧ 𝐾 ∈ 𝑉) ∧ (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝐾)) → (𝑀 ∈ (𝐺 NeighbVtx 𝐾) ↔ {𝑀, 𝐾} ∈ 𝐸)) |
| 14 | 1, 3, 10, 13 | syl21anc 838 |
. . . . 5
⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑀 ∈ (𝑉 ∖ {𝑁, 𝐾})) → (𝑀 ∈ (𝐺 NeighbVtx 𝐾) ↔ {𝑀, 𝐾} ∈ 𝐸)) |
| 15 | 14 | biimpa 476 |
. . . 4
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑀 ∈ (𝑉 ∖ {𝑁, 𝐾})) ∧ 𝑀 ∈ (𝐺 NeighbVtx 𝐾)) → {𝑀, 𝐾} ∈ 𝐸) |
| 16 | 8 | eleq2i 2833 |
. . . . . . . . . 10
⊢ (𝑀 ∈ (𝑉 ∖ {𝑁, 𝐾}) ↔ 𝑀 ∈ ((𝑉 ∖ {𝑁}) ∖ {𝐾})) |
| 17 | | eldifsn 4786 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ (𝑉 ∖ {𝑁}) ↔ (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑁)) |
| 18 | 17 | anbi1i 624 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑀 ≠ 𝐾) ↔ ((𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑁) ∧ 𝑀 ≠ 𝐾)) |
| 19 | 16, 4, 18 | 3bitri 297 |
. . . . . . . . 9
⊢ (𝑀 ∈ (𝑉 ∖ {𝑁, 𝐾}) ↔ ((𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑁) ∧ 𝑀 ≠ 𝐾)) |
| 20 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑁) → 𝑀 ≠ 𝑁) |
| 21 | 20 | necomd 2996 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑁) → 𝑁 ≠ 𝑀) |
| 22 | 21 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑁) ∧ 𝑀 ≠ 𝐾) → 𝑁 ≠ 𝑀) |
| 23 | 19, 22 | sylbi 217 |
. . . . . . . 8
⊢ (𝑀 ∈ (𝑉 ∖ {𝑁, 𝐾}) → 𝑁 ≠ 𝑀) |
| 24 | 23 | 3ad2ant3 1136 |
. . . . . . 7
⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑀 ∈ (𝑉 ∖ {𝑁, 𝐾})) → 𝑁 ≠ 𝑀) |
| 25 | | eldifsn 4786 |
. . . . . . . . 9
⊢ (𝐾 ∈ (𝑉 ∖ {𝑁}) ↔ (𝐾 ∈ 𝑉 ∧ 𝐾 ≠ 𝑁)) |
| 26 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ 𝑉 ∧ 𝐾 ≠ 𝑁) → 𝐾 ≠ 𝑁) |
| 27 | 26 | necomd 2996 |
. . . . . . . . 9
⊢ ((𝐾 ∈ 𝑉 ∧ 𝐾 ≠ 𝑁) → 𝑁 ≠ 𝐾) |
| 28 | 25, 27 | sylbi 217 |
. . . . . . . 8
⊢ (𝐾 ∈ (𝑉 ∖ {𝑁}) → 𝑁 ≠ 𝐾) |
| 29 | 28 | 3ad2ant2 1135 |
. . . . . . 7
⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑀 ∈ (𝑉 ∖ {𝑁, 𝐾})) → 𝑁 ≠ 𝐾) |
| 30 | 24, 29 | nelprd 4657 |
. . . . . 6
⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑀 ∈ (𝑉 ∖ {𝑁, 𝐾})) → ¬ 𝑁 ∈ {𝑀, 𝐾}) |
| 31 | | df-nel 3047 |
. . . . . 6
⊢ (𝑁 ∉ {𝑀, 𝐾} ↔ ¬ 𝑁 ∈ {𝑀, 𝐾}) |
| 32 | 30, 31 | sylibr 234 |
. . . . 5
⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑀 ∈ (𝑉 ∖ {𝑁, 𝐾})) → 𝑁 ∉ {𝑀, 𝐾}) |
| 33 | 32 | adantr 480 |
. . . 4
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑀 ∈ (𝑉 ∖ {𝑁, 𝐾})) ∧ 𝑀 ∈ (𝐺 NeighbVtx 𝐾)) → 𝑁 ∉ {𝑀, 𝐾}) |
| 34 | | neleq2 3053 |
. . . . 5
⊢ (𝑒 = {𝑀, 𝐾} → (𝑁 ∉ 𝑒 ↔ 𝑁 ∉ {𝑀, 𝐾})) |
| 35 | | nbupgrres.f |
. . . . 5
⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒} |
| 36 | 34, 35 | elrab2 3695 |
. . . 4
⊢ ({𝑀, 𝐾} ∈ 𝐹 ↔ ({𝑀, 𝐾} ∈ 𝐸 ∧ 𝑁 ∉ {𝑀, 𝐾})) |
| 37 | 15, 33, 36 | sylanbrc 583 |
. . 3
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑀 ∈ (𝑉 ∖ {𝑁, 𝐾})) ∧ 𝑀 ∈ (𝐺 NeighbVtx 𝐾)) → {𝑀, 𝐾} ∈ 𝐹) |
| 38 | | nbupgrres.s |
. . . . . . . 8
⊢ 𝑆 = 〈(𝑉 ∖ {𝑁}), ( I ↾ 𝐹)〉 |
| 39 | 11, 12, 35, 38 | upgrres1 29330 |
. . . . . . 7
⊢ ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) → 𝑆 ∈ UPGraph) |
| 40 | 39 | 3ad2ant1 1134 |
. . . . . 6
⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑀 ∈ (𝑉 ∖ {𝑁, 𝐾})) → 𝑆 ∈ UPGraph) |
| 41 | | simp2 1138 |
. . . . . 6
⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑀 ∈ (𝑉 ∖ {𝑁, 𝐾})) → 𝐾 ∈ (𝑉 ∖ {𝑁})) |
| 42 | 16, 4 | sylbb 219 |
. . . . . . 7
⊢ (𝑀 ∈ (𝑉 ∖ {𝑁, 𝐾}) → (𝑀 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑀 ≠ 𝐾)) |
| 43 | 42 | 3ad2ant3 1136 |
. . . . . 6
⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑀 ∈ (𝑉 ∖ {𝑁, 𝐾})) → (𝑀 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑀 ≠ 𝐾)) |
| 44 | 40, 41, 43 | jca31 514 |
. . . . 5
⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑀 ∈ (𝑉 ∖ {𝑁, 𝐾})) → ((𝑆 ∈ UPGraph ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})) ∧ (𝑀 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑀 ≠ 𝐾))) |
| 45 | 44 | adantr 480 |
. . . 4
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑀 ∈ (𝑉 ∖ {𝑁, 𝐾})) ∧ 𝑀 ∈ (𝐺 NeighbVtx 𝐾)) → ((𝑆 ∈ UPGraph ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})) ∧ (𝑀 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑀 ≠ 𝐾))) |
| 46 | 11, 12, 35, 38 | upgrres1lem2 29328 |
. . . . . 6
⊢
(Vtx‘𝑆) =
(𝑉 ∖ {𝑁}) |
| 47 | 46 | eqcomi 2746 |
. . . . 5
⊢ (𝑉 ∖ {𝑁}) = (Vtx‘𝑆) |
| 48 | | edgval 29066 |
. . . . . 6
⊢
(Edg‘𝑆) = ran
(iEdg‘𝑆) |
| 49 | 11, 12, 35, 38 | upgrres1lem3 29329 |
. . . . . . 7
⊢
(iEdg‘𝑆) = ( I
↾ 𝐹) |
| 50 | 49 | rneqi 5948 |
. . . . . 6
⊢ ran
(iEdg‘𝑆) = ran ( I
↾ 𝐹) |
| 51 | | rnresi 6093 |
. . . . . 6
⊢ ran ( I
↾ 𝐹) = 𝐹 |
| 52 | 48, 50, 51 | 3eqtrri 2770 |
. . . . 5
⊢ 𝐹 = (Edg‘𝑆) |
| 53 | 47, 52 | nbupgrel 29362 |
. . . 4
⊢ (((𝑆 ∈ UPGraph ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})) ∧ (𝑀 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑀 ≠ 𝐾)) → (𝑀 ∈ (𝑆 NeighbVtx 𝐾) ↔ {𝑀, 𝐾} ∈ 𝐹)) |
| 54 | 45, 53 | syl 17 |
. . 3
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑀 ∈ (𝑉 ∖ {𝑁, 𝐾})) ∧ 𝑀 ∈ (𝐺 NeighbVtx 𝐾)) → (𝑀 ∈ (𝑆 NeighbVtx 𝐾) ↔ {𝑀, 𝐾} ∈ 𝐹)) |
| 55 | 37, 54 | mpbird 257 |
. 2
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑀 ∈ (𝑉 ∖ {𝑁, 𝐾})) ∧ 𝑀 ∈ (𝐺 NeighbVtx 𝐾)) → 𝑀 ∈ (𝑆 NeighbVtx 𝐾)) |
| 56 | 55 | ex 412 |
1
⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑀 ∈ (𝑉 ∖ {𝑁, 𝐾})) → (𝑀 ∈ (𝐺 NeighbVtx 𝐾) → 𝑀 ∈ (𝑆 NeighbVtx 𝐾))) |