Proof of Theorem isuvtxa
Step | Hyp | Ref
| Expression |
1 | | uvtxael.v |
. . 3
⊢ 𝑉 = (Vtx‘𝐺) |
2 | 1 | uvtxaval 40613 |
. 2
⊢ (𝐺 ∈ 𝑊 → (UnivVtx‘𝐺) = {𝑣 ∈ 𝑉 ∣ ∀𝑘 ∈ (𝑉 ∖ {𝑣})𝑘 ∈ (𝐺 NeighbVtx 𝑣)}) |
3 | | isuvtxa.e |
. . . . . . 7
⊢ 𝐸 = (Edg‘𝐺) |
4 | 1, 3 | nbgrel 40564 |
. . . . . 6
⊢ (𝐺 ∈ 𝑊 → (𝑘 ∈ (𝐺 NeighbVtx 𝑣) ↔ ((𝑘 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉) ∧ 𝑘 ≠ 𝑣 ∧ ∃𝑒 ∈ 𝐸 {𝑣, 𝑘} ⊆ 𝑒))) |
5 | 4 | ad2antrr 758 |
. . . . 5
⊢ (((𝐺 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) ∧ 𝑘 ∈ (𝑉 ∖ {𝑣})) → (𝑘 ∈ (𝐺 NeighbVtx 𝑣) ↔ ((𝑘 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉) ∧ 𝑘 ≠ 𝑣 ∧ ∃𝑒 ∈ 𝐸 {𝑣, 𝑘} ⊆ 𝑒))) |
6 | | df-3an 1033 |
. . . . . 6
⊢ (((𝑘 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉) ∧ 𝑘 ≠ 𝑣 ∧ ∃𝑒 ∈ 𝐸 {𝑣, 𝑘} ⊆ 𝑒) ↔ (((𝑘 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉) ∧ 𝑘 ≠ 𝑣) ∧ ∃𝑒 ∈ 𝐸 {𝑣, 𝑘} ⊆ 𝑒)) |
7 | | prcom 4211 |
. . . . . . . . 9
⊢ {𝑘, 𝑣} = {𝑣, 𝑘} |
8 | 7 | sseq1i 3592 |
. . . . . . . 8
⊢ ({𝑘, 𝑣} ⊆ 𝑒 ↔ {𝑣, 𝑘} ⊆ 𝑒) |
9 | 8 | rexbii 3023 |
. . . . . . 7
⊢
(∃𝑒 ∈
𝐸 {𝑘, 𝑣} ⊆ 𝑒 ↔ ∃𝑒 ∈ 𝐸 {𝑣, 𝑘} ⊆ 𝑒) |
10 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) → 𝑣 ∈ 𝑉) |
11 | | eldifi 3694 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (𝑉 ∖ {𝑣}) → 𝑘 ∈ 𝑉) |
12 | 10, 11 | anim12ci 589 |
. . . . . . . . 9
⊢ (((𝐺 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) ∧ 𝑘 ∈ (𝑉 ∖ {𝑣})) → (𝑘 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉)) |
13 | | eldifsni 4261 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (𝑉 ∖ {𝑣}) → 𝑘 ≠ 𝑣) |
14 | 13 | adantl 481 |
. . . . . . . . 9
⊢ (((𝐺 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) ∧ 𝑘 ∈ (𝑉 ∖ {𝑣})) → 𝑘 ≠ 𝑣) |
15 | 12, 14 | jca 553 |
. . . . . . . 8
⊢ (((𝐺 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) ∧ 𝑘 ∈ (𝑉 ∖ {𝑣})) → ((𝑘 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉) ∧ 𝑘 ≠ 𝑣)) |
16 | 15 | biantrurd 528 |
. . . . . . 7
⊢ (((𝐺 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) ∧ 𝑘 ∈ (𝑉 ∖ {𝑣})) → (∃𝑒 ∈ 𝐸 {𝑣, 𝑘} ⊆ 𝑒 ↔ (((𝑘 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉) ∧ 𝑘 ≠ 𝑣) ∧ ∃𝑒 ∈ 𝐸 {𝑣, 𝑘} ⊆ 𝑒))) |
17 | 9, 16 | syl5rbb 272 |
. . . . . 6
⊢ (((𝐺 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) ∧ 𝑘 ∈ (𝑉 ∖ {𝑣})) → ((((𝑘 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉) ∧ 𝑘 ≠ 𝑣) ∧ ∃𝑒 ∈ 𝐸 {𝑣, 𝑘} ⊆ 𝑒) ↔ ∃𝑒 ∈ 𝐸 {𝑘, 𝑣} ⊆ 𝑒)) |
18 | 6, 17 | syl5bb 271 |
. . . . 5
⊢ (((𝐺 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) ∧ 𝑘 ∈ (𝑉 ∖ {𝑣})) → (((𝑘 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉) ∧ 𝑘 ≠ 𝑣 ∧ ∃𝑒 ∈ 𝐸 {𝑣, 𝑘} ⊆ 𝑒) ↔ ∃𝑒 ∈ 𝐸 {𝑘, 𝑣} ⊆ 𝑒)) |
19 | 5, 18 | bitrd 267 |
. . . 4
⊢ (((𝐺 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) ∧ 𝑘 ∈ (𝑉 ∖ {𝑣})) → (𝑘 ∈ (𝐺 NeighbVtx 𝑣) ↔ ∃𝑒 ∈ 𝐸 {𝑘, 𝑣} ⊆ 𝑒)) |
20 | 19 | ralbidva 2968 |
. . 3
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) → (∀𝑘 ∈ (𝑉 ∖ {𝑣})𝑘 ∈ (𝐺 NeighbVtx 𝑣) ↔ ∀𝑘 ∈ (𝑉 ∖ {𝑣})∃𝑒 ∈ 𝐸 {𝑘, 𝑣} ⊆ 𝑒)) |
21 | 20 | rabbidva 3163 |
. 2
⊢ (𝐺 ∈ 𝑊 → {𝑣 ∈ 𝑉 ∣ ∀𝑘 ∈ (𝑉 ∖ {𝑣})𝑘 ∈ (𝐺 NeighbVtx 𝑣)} = {𝑣 ∈ 𝑉 ∣ ∀𝑘 ∈ (𝑉 ∖ {𝑣})∃𝑒 ∈ 𝐸 {𝑘, 𝑣} ⊆ 𝑒}) |
22 | 2, 21 | eqtrd 2644 |
1
⊢ (𝐺 ∈ 𝑊 → (UnivVtx‘𝐺) = {𝑣 ∈ 𝑉 ∣ ∀𝑘 ∈ (𝑉 ∖ {𝑣})∃𝑒 ∈ 𝐸 {𝑘, 𝑣} ⊆ 𝑒}) |