Step | Hyp | Ref
| Expression |
1 | | nbgrel.v |
. . . 4
⊢ 𝑉 = (Vtx‘𝐺) |
2 | | nbgrel.e |
. . . 4
⊢ 𝐸 = (Edg‘𝐺) |
3 | 1, 2 | nbgrval 26234 |
. . 3
⊢ (𝑁 ∈ 𝑉 → (𝐺 NeighbVtx 𝑁) = {𝑣 ∈ (𝑉 ∖ {𝑁}) ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑣} ⊆ 𝑒}) |
4 | 3 | adantl 482 |
. 2
⊢ ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) → (𝐺 NeighbVtx 𝑁) = {𝑣 ∈ (𝑉 ∖ {𝑁}) ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑣} ⊆ 𝑒}) |
5 | | eldifi 3732 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝑉 ∖ {𝑁}) → 𝑥 ∈ 𝑉) |
6 | 5 | adantl 482 |
. . . . . . . . 9
⊢ (((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝑥 ∈ (𝑉 ∖ {𝑁})) → 𝑥 ∈ 𝑉) |
7 | 6 | adantr 481 |
. . . . . . . 8
⊢ ((((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝑥 ∈ (𝑉 ∖ {𝑁})) ∧ (𝑒 ∈ 𝐸 ∧ {𝑁, 𝑥} ⊆ 𝑒)) → 𝑥 ∈ 𝑉) |
8 | | umgrupgr 25998 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ UMGraph → 𝐺 ∈ UPGraph
) |
9 | 8 | ad4antr 768 |
. . . . . . . . . . . 12
⊢
(((((𝐺 ∈
UMGraph ∧ 𝑁 ∈
𝑉) ∧ 𝑥 ∈ (𝑉 ∖ {𝑁})) ∧ 𝑒 ∈ 𝐸) ∧ {𝑁, 𝑥} ⊆ 𝑒) → 𝐺 ∈ UPGraph ) |
10 | | simpr 477 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝑥 ∈ (𝑉 ∖ {𝑁})) ∧ 𝑒 ∈ 𝐸) → 𝑒 ∈ 𝐸) |
11 | 10 | adantr 481 |
. . . . . . . . . . . 12
⊢
(((((𝐺 ∈
UMGraph ∧ 𝑁 ∈
𝑉) ∧ 𝑥 ∈ (𝑉 ∖ {𝑁})) ∧ 𝑒 ∈ 𝐸) ∧ {𝑁, 𝑥} ⊆ 𝑒) → 𝑒 ∈ 𝐸) |
12 | | simpr 477 |
. . . . . . . . . . . 12
⊢
(((((𝐺 ∈
UMGraph ∧ 𝑁 ∈
𝑉) ∧ 𝑥 ∈ (𝑉 ∖ {𝑁})) ∧ 𝑒 ∈ 𝐸) ∧ {𝑁, 𝑥} ⊆ 𝑒) → {𝑁, 𝑥} ⊆ 𝑒) |
13 | | simpr 477 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) → 𝑁 ∈ 𝑉) |
14 | 13 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝑥 ∈ (𝑉 ∖ {𝑁})) → 𝑁 ∈ 𝑉) |
15 | | vex 3203 |
. . . . . . . . . . . . . . . 16
⊢ 𝑥 ∈ V |
16 | 15 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝑥 ∈ (𝑉 ∖ {𝑁})) → 𝑥 ∈ V) |
17 | | eldifsn 4317 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (𝑉 ∖ {𝑁}) ↔ (𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 𝑁)) |
18 | | simpr 477 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 𝑁) → 𝑥 ≠ 𝑁) |
19 | 18 | necomd 2849 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 𝑁) → 𝑁 ≠ 𝑥) |
20 | 17, 19 | sylbi 207 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (𝑉 ∖ {𝑁}) → 𝑁 ≠ 𝑥) |
21 | 20 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝑥 ∈ (𝑉 ∖ {𝑁})) → 𝑁 ≠ 𝑥) |
22 | 14, 16, 21 | 3jca 1242 |
. . . . . . . . . . . . . 14
⊢ (((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝑥 ∈ (𝑉 ∖ {𝑁})) → (𝑁 ∈ 𝑉 ∧ 𝑥 ∈ V ∧ 𝑁 ≠ 𝑥)) |
23 | 22 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝑥 ∈ (𝑉 ∖ {𝑁})) ∧ 𝑒 ∈ 𝐸) → (𝑁 ∈ 𝑉 ∧ 𝑥 ∈ V ∧ 𝑁 ≠ 𝑥)) |
24 | 23 | adantr 481 |
. . . . . . . . . . . 12
⊢
(((((𝐺 ∈
UMGraph ∧ 𝑁 ∈
𝑉) ∧ 𝑥 ∈ (𝑉 ∖ {𝑁})) ∧ 𝑒 ∈ 𝐸) ∧ {𝑁, 𝑥} ⊆ 𝑒) → (𝑁 ∈ 𝑉 ∧ 𝑥 ∈ V ∧ 𝑁 ≠ 𝑥)) |
25 | 1, 2 | upgredgpr 26037 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ UPGraph ∧ 𝑒 ∈ 𝐸 ∧ {𝑁, 𝑥} ⊆ 𝑒) ∧ (𝑁 ∈ 𝑉 ∧ 𝑥 ∈ V ∧ 𝑁 ≠ 𝑥)) → {𝑁, 𝑥} = 𝑒) |
26 | 9, 11, 12, 24, 25 | syl31anc 1329 |
. . . . . . . . . . 11
⊢
(((((𝐺 ∈
UMGraph ∧ 𝑁 ∈
𝑉) ∧ 𝑥 ∈ (𝑉 ∖ {𝑁})) ∧ 𝑒 ∈ 𝐸) ∧ {𝑁, 𝑥} ⊆ 𝑒) → {𝑁, 𝑥} = 𝑒) |
27 | 26 | ex 450 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝑥 ∈ (𝑉 ∖ {𝑁})) ∧ 𝑒 ∈ 𝐸) → ({𝑁, 𝑥} ⊆ 𝑒 → {𝑁, 𝑥} = 𝑒)) |
28 | | eleq1 2689 |
. . . . . . . . . . 11
⊢ ({𝑁, 𝑥} = 𝑒 → ({𝑁, 𝑥} ∈ 𝐸 ↔ 𝑒 ∈ 𝐸)) |
29 | 28 | biimprd 238 |
. . . . . . . . . 10
⊢ ({𝑁, 𝑥} = 𝑒 → (𝑒 ∈ 𝐸 → {𝑁, 𝑥} ∈ 𝐸)) |
30 | 27, 10, 29 | syl6ci 71 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝑥 ∈ (𝑉 ∖ {𝑁})) ∧ 𝑒 ∈ 𝐸) → ({𝑁, 𝑥} ⊆ 𝑒 → {𝑁, 𝑥} ∈ 𝐸)) |
31 | 30 | impr 649 |
. . . . . . . 8
⊢ ((((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝑥 ∈ (𝑉 ∖ {𝑁})) ∧ (𝑒 ∈ 𝐸 ∧ {𝑁, 𝑥} ⊆ 𝑒)) → {𝑁, 𝑥} ∈ 𝐸) |
32 | 7, 31 | jca 554 |
. . . . . . 7
⊢ ((((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝑥 ∈ (𝑉 ∖ {𝑁})) ∧ (𝑒 ∈ 𝐸 ∧ {𝑁, 𝑥} ⊆ 𝑒)) → (𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ 𝐸)) |
33 | 32 | rexlimdvaa 3032 |
. . . . . 6
⊢ (((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝑥 ∈ (𝑉 ∖ {𝑁})) → (∃𝑒 ∈ 𝐸 {𝑁, 𝑥} ⊆ 𝑒 → (𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ 𝐸))) |
34 | 33 | expimpd 629 |
. . . . 5
⊢ ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) → ((𝑥 ∈ (𝑉 ∖ {𝑁}) ∧ ∃𝑒 ∈ 𝐸 {𝑁, 𝑥} ⊆ 𝑒) → (𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ 𝐸))) |
35 | | simprl 794 |
. . . . . . . 8
⊢ (((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ 𝐸)) → 𝑥 ∈ 𝑉) |
36 | 2 | umgredgne 26040 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ UMGraph ∧ {𝑁, 𝑥} ∈ 𝐸) → 𝑁 ≠ 𝑥) |
37 | 36 | ad2ant2rl 785 |
. . . . . . . . 9
⊢ (((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ 𝐸)) → 𝑁 ≠ 𝑥) |
38 | 37 | necomd 2849 |
. . . . . . . 8
⊢ (((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ 𝐸)) → 𝑥 ≠ 𝑁) |
39 | 35, 38, 17 | sylanbrc 698 |
. . . . . . 7
⊢ (((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ 𝐸)) → 𝑥 ∈ (𝑉 ∖ {𝑁})) |
40 | | simpr 477 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ 𝐸) → {𝑁, 𝑥} ∈ 𝐸) |
41 | 40 | adantl 482 |
. . . . . . . 8
⊢ (((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ 𝐸)) → {𝑁, 𝑥} ∈ 𝐸) |
42 | | sseq2 3627 |
. . . . . . . . 9
⊢ (𝑒 = {𝑁, 𝑥} → ({𝑁, 𝑥} ⊆ 𝑒 ↔ {𝑁, 𝑥} ⊆ {𝑁, 𝑥})) |
43 | 42 | adantl 482 |
. . . . . . . 8
⊢ ((((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ 𝐸)) ∧ 𝑒 = {𝑁, 𝑥}) → ({𝑁, 𝑥} ⊆ 𝑒 ↔ {𝑁, 𝑥} ⊆ {𝑁, 𝑥})) |
44 | | ssid 3624 |
. . . . . . . . 9
⊢ {𝑁, 𝑥} ⊆ {𝑁, 𝑥} |
45 | 44 | a1i 11 |
. . . . . . . 8
⊢ (((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ 𝐸)) → {𝑁, 𝑥} ⊆ {𝑁, 𝑥}) |
46 | 41, 43, 45 | rspcedvd 3317 |
. . . . . . 7
⊢ (((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ 𝐸)) → ∃𝑒 ∈ 𝐸 {𝑁, 𝑥} ⊆ 𝑒) |
47 | 39, 46 | jca 554 |
. . . . . 6
⊢ (((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ 𝐸)) → (𝑥 ∈ (𝑉 ∖ {𝑁}) ∧ ∃𝑒 ∈ 𝐸 {𝑁, 𝑥} ⊆ 𝑒)) |
48 | 47 | ex 450 |
. . . . 5
⊢ ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) → ((𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ 𝐸) → (𝑥 ∈ (𝑉 ∖ {𝑁}) ∧ ∃𝑒 ∈ 𝐸 {𝑁, 𝑥} ⊆ 𝑒))) |
49 | 34, 48 | impbid 202 |
. . . 4
⊢ ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) → ((𝑥 ∈ (𝑉 ∖ {𝑁}) ∧ ∃𝑒 ∈ 𝐸 {𝑁, 𝑥} ⊆ 𝑒) ↔ (𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ 𝐸))) |
50 | | preq2 4269 |
. . . . . . 7
⊢ (𝑣 = 𝑥 → {𝑁, 𝑣} = {𝑁, 𝑥}) |
51 | 50 | sseq1d 3632 |
. . . . . 6
⊢ (𝑣 = 𝑥 → ({𝑁, 𝑣} ⊆ 𝑒 ↔ {𝑁, 𝑥} ⊆ 𝑒)) |
52 | 51 | rexbidv 3052 |
. . . . 5
⊢ (𝑣 = 𝑥 → (∃𝑒 ∈ 𝐸 {𝑁, 𝑣} ⊆ 𝑒 ↔ ∃𝑒 ∈ 𝐸 {𝑁, 𝑥} ⊆ 𝑒)) |
53 | 52 | elrab 3363 |
. . . 4
⊢ (𝑥 ∈ {𝑣 ∈ (𝑉 ∖ {𝑁}) ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑣} ⊆ 𝑒} ↔ (𝑥 ∈ (𝑉 ∖ {𝑁}) ∧ ∃𝑒 ∈ 𝐸 {𝑁, 𝑥} ⊆ 𝑒)) |
54 | | preq2 4269 |
. . . . . 6
⊢ (𝑛 = 𝑥 → {𝑁, 𝑛} = {𝑁, 𝑥}) |
55 | 54 | eleq1d 2686 |
. . . . 5
⊢ (𝑛 = 𝑥 → ({𝑁, 𝑛} ∈ 𝐸 ↔ {𝑁, 𝑥} ∈ 𝐸)) |
56 | 55 | elrab 3363 |
. . . 4
⊢ (𝑥 ∈ {𝑛 ∈ 𝑉 ∣ {𝑁, 𝑛} ∈ 𝐸} ↔ (𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ 𝐸)) |
57 | 49, 53, 56 | 3bitr4g 303 |
. . 3
⊢ ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) → (𝑥 ∈ {𝑣 ∈ (𝑉 ∖ {𝑁}) ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑣} ⊆ 𝑒} ↔ 𝑥 ∈ {𝑛 ∈ 𝑉 ∣ {𝑁, 𝑛} ∈ 𝐸})) |
58 | 57 | eqrdv 2620 |
. 2
⊢ ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) → {𝑣 ∈ (𝑉 ∖ {𝑁}) ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑣} ⊆ 𝑒} = {𝑛 ∈ 𝑉 ∣ {𝑁, 𝑛} ∈ 𝐸}) |
59 | 4, 58 | eqtrd 2656 |
1
⊢ ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) → (𝐺 NeighbVtx 𝑁) = {𝑛 ∈ 𝑉 ∣ {𝑁, 𝑛} ∈ 𝐸}) |