Proof of Theorem nbuhgr
Step | Hyp | Ref
| Expression |
1 | | nbgrel.v |
. . . 4
⊢ 𝑉 = (Vtx‘𝐺) |
2 | | nbgrel.e |
. . . 4
⊢ 𝐸 = (Edg‘𝐺) |
3 | 1, 2 | nbgrval 40560 |
. . 3
⊢ (𝑁 ∈ 𝑉 → (𝐺 NeighbVtx 𝑁) = {𝑛 ∈ (𝑉 ∖ {𝑁}) ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒}) |
4 | 3 | a1d 25 |
. 2
⊢ (𝑁 ∈ 𝑉 → ((𝐺 ∈ UHGraph ∧ 𝑁 ∈ 𝑋) → (𝐺 NeighbVtx 𝑁) = {𝑛 ∈ (𝑉 ∖ {𝑁}) ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒})) |
5 | | df-nel 2783 |
. . . . . 6
⊢ (𝑁 ∉ 𝑉 ↔ ¬ 𝑁 ∈ 𝑉) |
6 | 1 | nbgrnvtx0 40563 |
. . . . . 6
⊢ (𝑁 ∉ 𝑉 → (𝐺 NeighbVtx 𝑁) = ∅) |
7 | 5, 6 | sylbir 224 |
. . . . 5
⊢ (¬
𝑁 ∈ 𝑉 → (𝐺 NeighbVtx 𝑁) = ∅) |
8 | 7 | adantr 480 |
. . . 4
⊢ ((¬
𝑁 ∈ 𝑉 ∧ (𝐺 ∈ UHGraph ∧ 𝑁 ∈ 𝑋)) → (𝐺 NeighbVtx 𝑁) = ∅) |
9 | | simpl 472 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ UHGraph ∧ 𝑁 ∈ 𝑋) → 𝐺 ∈ UHGraph ) |
10 | 9 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ UHGraph ∧ 𝑁 ∈ 𝑋) ∧ 𝑛 ∈ (𝑉 ∖ {𝑁})) → 𝐺 ∈ UHGraph ) |
11 | 2 | eleq2i 2680 |
. . . . . . . . . . . 12
⊢ (𝑒 ∈ 𝐸 ↔ 𝑒 ∈ (Edg‘𝐺)) |
12 | 11 | biimpi 205 |
. . . . . . . . . . 11
⊢ (𝑒 ∈ 𝐸 → 𝑒 ∈ (Edg‘𝐺)) |
13 | | edguhgr 25803 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ UHGraph ∧ 𝑒 ∈ (Edg‘𝐺)) → 𝑒 ∈ 𝒫 (Vtx‘𝐺)) |
14 | 10, 12, 13 | syl2an 493 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ UHGraph ∧ 𝑁 ∈ 𝑋) ∧ 𝑛 ∈ (𝑉 ∖ {𝑁})) ∧ 𝑒 ∈ 𝐸) → 𝑒 ∈ 𝒫 (Vtx‘𝐺)) |
15 | | selpw 4115 |
. . . . . . . . . . . 12
⊢ (𝑒 ∈ 𝒫
(Vtx‘𝐺) ↔ 𝑒 ⊆ (Vtx‘𝐺)) |
16 | 1 | eqcomi 2619 |
. . . . . . . . . . . . 13
⊢
(Vtx‘𝐺) =
𝑉 |
17 | 16 | sseq2i 3593 |
. . . . . . . . . . . 12
⊢ (𝑒 ⊆ (Vtx‘𝐺) ↔ 𝑒 ⊆ 𝑉) |
18 | 15, 17 | bitri 263 |
. . . . . . . . . . 11
⊢ (𝑒 ∈ 𝒫
(Vtx‘𝐺) ↔ 𝑒 ⊆ 𝑉) |
19 | | sstr 3576 |
. . . . . . . . . . . . . . 15
⊢ (({𝑁, 𝑛} ⊆ 𝑒 ∧ 𝑒 ⊆ 𝑉) → {𝑁, 𝑛} ⊆ 𝑉) |
20 | | vex 3176 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑛 ∈ V |
21 | | prssg 4290 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ 𝑋 ∧ 𝑛 ∈ V) → ((𝑁 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉) ↔ {𝑁, 𝑛} ⊆ 𝑉)) |
22 | 21 | bicomd 212 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ 𝑋 ∧ 𝑛 ∈ V) → ({𝑁, 𝑛} ⊆ 𝑉 ↔ (𝑁 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉))) |
23 | 20, 22 | mpan2 703 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ 𝑋 → ({𝑁, 𝑛} ⊆ 𝑉 ↔ (𝑁 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉))) |
24 | | simpl 472 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉) → 𝑁 ∈ 𝑉) |
25 | 23, 24 | syl6bi 242 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ 𝑋 → ({𝑁, 𝑛} ⊆ 𝑉 → 𝑁 ∈ 𝑉)) |
26 | 19, 25 | syl5com 31 |
. . . . . . . . . . . . . 14
⊢ (({𝑁, 𝑛} ⊆ 𝑒 ∧ 𝑒 ⊆ 𝑉) → (𝑁 ∈ 𝑋 → 𝑁 ∈ 𝑉)) |
27 | 26 | ex 449 |
. . . . . . . . . . . . 13
⊢ ({𝑁, 𝑛} ⊆ 𝑒 → (𝑒 ⊆ 𝑉 → (𝑁 ∈ 𝑋 → 𝑁 ∈ 𝑉))) |
28 | 27 | com13 86 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ 𝑋 → (𝑒 ⊆ 𝑉 → ({𝑁, 𝑛} ⊆ 𝑒 → 𝑁 ∈ 𝑉))) |
29 | 28 | ad3antlr 763 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ UHGraph ∧ 𝑁 ∈ 𝑋) ∧ 𝑛 ∈ (𝑉 ∖ {𝑁})) ∧ 𝑒 ∈ 𝐸) → (𝑒 ⊆ 𝑉 → ({𝑁, 𝑛} ⊆ 𝑒 → 𝑁 ∈ 𝑉))) |
30 | 18, 29 | syl5bi 231 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ UHGraph ∧ 𝑁 ∈ 𝑋) ∧ 𝑛 ∈ (𝑉 ∖ {𝑁})) ∧ 𝑒 ∈ 𝐸) → (𝑒 ∈ 𝒫 (Vtx‘𝐺) → ({𝑁, 𝑛} ⊆ 𝑒 → 𝑁 ∈ 𝑉))) |
31 | 14, 30 | mpd 15 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ UHGraph ∧ 𝑁 ∈ 𝑋) ∧ 𝑛 ∈ (𝑉 ∖ {𝑁})) ∧ 𝑒 ∈ 𝐸) → ({𝑁, 𝑛} ⊆ 𝑒 → 𝑁 ∈ 𝑉)) |
32 | 31 | rexlimdva 3013 |
. . . . . . . 8
⊢ (((𝐺 ∈ UHGraph ∧ 𝑁 ∈ 𝑋) ∧ 𝑛 ∈ (𝑉 ∖ {𝑁})) → (∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒 → 𝑁 ∈ 𝑉)) |
33 | 32 | con3rr3 150 |
. . . . . . 7
⊢ (¬
𝑁 ∈ 𝑉 → (((𝐺 ∈ UHGraph ∧ 𝑁 ∈ 𝑋) ∧ 𝑛 ∈ (𝑉 ∖ {𝑁})) → ¬ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒)) |
34 | 33 | expdimp 452 |
. . . . . 6
⊢ ((¬
𝑁 ∈ 𝑉 ∧ (𝐺 ∈ UHGraph ∧ 𝑁 ∈ 𝑋)) → (𝑛 ∈ (𝑉 ∖ {𝑁}) → ¬ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒)) |
35 | 34 | ralrimiv 2948 |
. . . . 5
⊢ ((¬
𝑁 ∈ 𝑉 ∧ (𝐺 ∈ UHGraph ∧ 𝑁 ∈ 𝑋)) → ∀𝑛 ∈ (𝑉 ∖ {𝑁}) ¬ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒) |
36 | | rabeq0 3911 |
. . . . 5
⊢ ({𝑛 ∈ (𝑉 ∖ {𝑁}) ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒} = ∅ ↔ ∀𝑛 ∈ (𝑉 ∖ {𝑁}) ¬ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒) |
37 | 35, 36 | sylibr 223 |
. . . 4
⊢ ((¬
𝑁 ∈ 𝑉 ∧ (𝐺 ∈ UHGraph ∧ 𝑁 ∈ 𝑋)) → {𝑛 ∈ (𝑉 ∖ {𝑁}) ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒} = ∅) |
38 | 8, 37 | eqtr4d 2647 |
. . 3
⊢ ((¬
𝑁 ∈ 𝑉 ∧ (𝐺 ∈ UHGraph ∧ 𝑁 ∈ 𝑋)) → (𝐺 NeighbVtx 𝑁) = {𝑛 ∈ (𝑉 ∖ {𝑁}) ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒}) |
39 | 38 | ex 449 |
. 2
⊢ (¬
𝑁 ∈ 𝑉 → ((𝐺 ∈ UHGraph ∧ 𝑁 ∈ 𝑋) → (𝐺 NeighbVtx 𝑁) = {𝑛 ∈ (𝑉 ∖ {𝑁}) ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒})) |
40 | 4, 39 | pm2.61i 175 |
1
⊢ ((𝐺 ∈ UHGraph ∧ 𝑁 ∈ 𝑋) → (𝐺 NeighbVtx 𝑁) = {𝑛 ∈ (𝑉 ∖ {𝑁}) ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒}) |