Proof of Theorem nbupgrres
Step | Hyp | Ref
| Expression |
1 | | simp1l 1078 |
. . . . . 6
⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑀 ∈ (𝑉 ∖ {𝑁, 𝐾})) → 𝐺 ∈ UPGraph ) |
2 | | eldifi 3694 |
. . . . . . 7
⊢ (𝐾 ∈ (𝑉 ∖ {𝑁}) → 𝐾 ∈ 𝑉) |
3 | 2 | 3ad2ant2 1076 |
. . . . . 6
⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑀 ∈ (𝑉 ∖ {𝑁, 𝐾})) → 𝐾 ∈ 𝑉) |
4 | | eldifsn 4260 |
. . . . . . . . 9
⊢ (𝑀 ∈ ((𝑉 ∖ {𝑁}) ∖ {𝐾}) ↔ (𝑀 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑀 ≠ 𝐾)) |
5 | | eldifi 3694 |
. . . . . . . . . 10
⊢ (𝑀 ∈ (𝑉 ∖ {𝑁}) → 𝑀 ∈ 𝑉) |
6 | 5 | anim1i 590 |
. . . . . . . . 9
⊢ ((𝑀 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑀 ≠ 𝐾) → (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝐾)) |
7 | 4, 6 | sylbi 206 |
. . . . . . . 8
⊢ (𝑀 ∈ ((𝑉 ∖ {𝑁}) ∖ {𝐾}) → (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝐾)) |
8 | | difpr 4275 |
. . . . . . . 8
⊢ (𝑉 ∖ {𝑁, 𝐾}) = ((𝑉 ∖ {𝑁}) ∖ {𝐾}) |
9 | 7, 8 | eleq2s 2706 |
. . . . . . 7
⊢ (𝑀 ∈ (𝑉 ∖ {𝑁, 𝐾}) → (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝐾)) |
10 | 9 | 3ad2ant3 1077 |
. . . . . 6
⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑀 ∈ (𝑉 ∖ {𝑁, 𝐾})) → (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝐾)) |
11 | | nbupgrres.v |
. . . . . . 7
⊢ 𝑉 = (Vtx‘𝐺) |
12 | | nbupgrres.e |
. . . . . . 7
⊢ 𝐸 = (Edg‘𝐺) |
13 | 11, 12 | nbupgrel 40567 |
. . . . . 6
⊢ (((𝐺 ∈ UPGraph ∧ 𝐾 ∈ 𝑉) ∧ (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝐾)) → (𝑀 ∈ (𝐺 NeighbVtx 𝐾) ↔ {𝑀, 𝐾} ∈ 𝐸)) |
14 | 1, 3, 10, 13 | syl21anc 1317 |
. . . . 5
⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑀 ∈ (𝑉 ∖ {𝑁, 𝐾})) → (𝑀 ∈ (𝐺 NeighbVtx 𝐾) ↔ {𝑀, 𝐾} ∈ 𝐸)) |
15 | 14 | biimpa 500 |
. . . 4
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑀 ∈ (𝑉 ∖ {𝑁, 𝐾})) ∧ 𝑀 ∈ (𝐺 NeighbVtx 𝐾)) → {𝑀, 𝐾} ∈ 𝐸) |
16 | 8 | eleq2i 2680 |
. . . . . . . . . 10
⊢ (𝑀 ∈ (𝑉 ∖ {𝑁, 𝐾}) ↔ 𝑀 ∈ ((𝑉 ∖ {𝑁}) ∖ {𝐾})) |
17 | | eldifsn 4260 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ (𝑉 ∖ {𝑁}) ↔ (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑁)) |
18 | 17 | anbi1i 727 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑀 ≠ 𝐾) ↔ ((𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑁) ∧ 𝑀 ≠ 𝐾)) |
19 | 16, 4, 18 | 3bitri 285 |
. . . . . . . . 9
⊢ (𝑀 ∈ (𝑉 ∖ {𝑁, 𝐾}) ↔ ((𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑁) ∧ 𝑀 ≠ 𝐾)) |
20 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑁) → 𝑀 ≠ 𝑁) |
21 | 20 | necomd 2837 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑁) → 𝑁 ≠ 𝑀) |
22 | 21 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑁) ∧ 𝑀 ≠ 𝐾) → 𝑁 ≠ 𝑀) |
23 | 19, 22 | sylbi 206 |
. . . . . . . 8
⊢ (𝑀 ∈ (𝑉 ∖ {𝑁, 𝐾}) → 𝑁 ≠ 𝑀) |
24 | 23 | 3ad2ant3 1077 |
. . . . . . 7
⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑀 ∈ (𝑉 ∖ {𝑁, 𝐾})) → 𝑁 ≠ 𝑀) |
25 | | eldifsn 4260 |
. . . . . . . . 9
⊢ (𝐾 ∈ (𝑉 ∖ {𝑁}) ↔ (𝐾 ∈ 𝑉 ∧ 𝐾 ≠ 𝑁)) |
26 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ 𝑉 ∧ 𝐾 ≠ 𝑁) → 𝐾 ≠ 𝑁) |
27 | 26 | necomd 2837 |
. . . . . . . . 9
⊢ ((𝐾 ∈ 𝑉 ∧ 𝐾 ≠ 𝑁) → 𝑁 ≠ 𝐾) |
28 | 25, 27 | sylbi 206 |
. . . . . . . 8
⊢ (𝐾 ∈ (𝑉 ∖ {𝑁}) → 𝑁 ≠ 𝐾) |
29 | 28 | 3ad2ant2 1076 |
. . . . . . 7
⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑀 ∈ (𝑉 ∖ {𝑁, 𝐾})) → 𝑁 ≠ 𝐾) |
30 | 24, 29 | nelprd 4151 |
. . . . . 6
⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑀 ∈ (𝑉 ∖ {𝑁, 𝐾})) → ¬ 𝑁 ∈ {𝑀, 𝐾}) |
31 | | df-nel 2783 |
. . . . . 6
⊢ (𝑁 ∉ {𝑀, 𝐾} ↔ ¬ 𝑁 ∈ {𝑀, 𝐾}) |
32 | 30, 31 | sylibr 223 |
. . . . 5
⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑀 ∈ (𝑉 ∖ {𝑁, 𝐾})) → 𝑁 ∉ {𝑀, 𝐾}) |
33 | 32 | adantr 480 |
. . . 4
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑀 ∈ (𝑉 ∖ {𝑁, 𝐾})) ∧ 𝑀 ∈ (𝐺 NeighbVtx 𝐾)) → 𝑁 ∉ {𝑀, 𝐾}) |
34 | | neleq2 2889 |
. . . . 5
⊢ (𝑒 = {𝑀, 𝐾} → (𝑁 ∉ 𝑒 ↔ 𝑁 ∉ {𝑀, 𝐾})) |
35 | | nbupgrres.f |
. . . . 5
⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒} |
36 | 34, 35 | elrab2 3333 |
. . . 4
⊢ ({𝑀, 𝐾} ∈ 𝐹 ↔ ({𝑀, 𝐾} ∈ 𝐸 ∧ 𝑁 ∉ {𝑀, 𝐾})) |
37 | 15, 33, 36 | sylanbrc 695 |
. . 3
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑀 ∈ (𝑉 ∖ {𝑁, 𝐾})) ∧ 𝑀 ∈ (𝐺 NeighbVtx 𝐾)) → {𝑀, 𝐾} ∈ 𝐹) |
38 | | nbupgrres.s |
. . . . . . . 8
⊢ 𝑆 = 〈(𝑉 ∖ {𝑁}), ( I ↾ 𝐹)〉 |
39 | 11, 12, 35, 38 | upgrres1 40532 |
. . . . . . 7
⊢ ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) → 𝑆 ∈ UPGraph ) |
40 | 39 | 3ad2ant1 1075 |
. . . . . 6
⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑀 ∈ (𝑉 ∖ {𝑁, 𝐾})) → 𝑆 ∈ UPGraph ) |
41 | | simp2 1055 |
. . . . . 6
⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑀 ∈ (𝑉 ∖ {𝑁, 𝐾})) → 𝐾 ∈ (𝑉 ∖ {𝑁})) |
42 | 16, 4 | sylbb 208 |
. . . . . . 7
⊢ (𝑀 ∈ (𝑉 ∖ {𝑁, 𝐾}) → (𝑀 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑀 ≠ 𝐾)) |
43 | 42 | 3ad2ant3 1077 |
. . . . . 6
⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑀 ∈ (𝑉 ∖ {𝑁, 𝐾})) → (𝑀 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑀 ≠ 𝐾)) |
44 | 40, 41, 43 | jca31 555 |
. . . . 5
⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑀 ∈ (𝑉 ∖ {𝑁, 𝐾})) → ((𝑆 ∈ UPGraph ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})) ∧ (𝑀 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑀 ≠ 𝐾))) |
45 | 44 | adantr 480 |
. . . 4
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑀 ∈ (𝑉 ∖ {𝑁, 𝐾})) ∧ 𝑀 ∈ (𝐺 NeighbVtx 𝐾)) → ((𝑆 ∈ UPGraph ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})) ∧ (𝑀 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑀 ≠ 𝐾))) |
46 | 11, 12, 35, 38 | upgrres1lem2 40530 |
. . . . . 6
⊢
(Vtx‘𝑆) =
(𝑉 ∖ {𝑁}) |
47 | 46 | eqcomi 2619 |
. . . . 5
⊢ (𝑉 ∖ {𝑁}) = (Vtx‘𝑆) |
48 | | opex 4859 |
. . . . . . . 8
⊢
〈(𝑉 ∖
{𝑁}), ( I ↾ 𝐹)〉 ∈
V |
49 | 38, 48 | eqeltri 2684 |
. . . . . . 7
⊢ 𝑆 ∈ V |
50 | | edgaval 25794 |
. . . . . . 7
⊢ (𝑆 ∈ V →
(Edg‘𝑆) = ran
(iEdg‘𝑆)) |
51 | 49, 50 | ax-mp 5 |
. . . . . 6
⊢
(Edg‘𝑆) = ran
(iEdg‘𝑆) |
52 | 11, 12, 35, 38 | upgrres1lem3 40531 |
. . . . . . 7
⊢
(iEdg‘𝑆) = ( I
↾ 𝐹) |
53 | 52 | rneqi 5273 |
. . . . . 6
⊢ ran
(iEdg‘𝑆) = ran ( I
↾ 𝐹) |
54 | | rnresi 5398 |
. . . . . 6
⊢ ran ( I
↾ 𝐹) = 𝐹 |
55 | 51, 53, 54 | 3eqtrri 2637 |
. . . . 5
⊢ 𝐹 = (Edg‘𝑆) |
56 | 47, 55 | nbupgrel 40567 |
. . . 4
⊢ (((𝑆 ∈ UPGraph ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})) ∧ (𝑀 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑀 ≠ 𝐾)) → (𝑀 ∈ (𝑆 NeighbVtx 𝐾) ↔ {𝑀, 𝐾} ∈ 𝐹)) |
57 | 45, 56 | syl 17 |
. . 3
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑀 ∈ (𝑉 ∖ {𝑁, 𝐾})) ∧ 𝑀 ∈ (𝐺 NeighbVtx 𝐾)) → (𝑀 ∈ (𝑆 NeighbVtx 𝐾) ↔ {𝑀, 𝐾} ∈ 𝐹)) |
58 | 37, 57 | mpbird 246 |
. 2
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑀 ∈ (𝑉 ∖ {𝑁, 𝐾})) ∧ 𝑀 ∈ (𝐺 NeighbVtx 𝐾)) → 𝑀 ∈ (𝑆 NeighbVtx 𝐾)) |
59 | 58 | ex 449 |
1
⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑀 ∈ (𝑉 ∖ {𝑁, 𝐾})) → (𝑀 ∈ (𝐺 NeighbVtx 𝐾) → 𝑀 ∈ (𝑆 NeighbVtx 𝐾))) |