Metamath Proof Explorer

Theorem isuvtx

Description: The set of all universal vertices. (Contributed by Alexander van der Vekens, 12-Oct-2017) (Revised by AV, 30-Oct-2020) (Revised by AV, 14-Feb-2022)

Ref Expression
Hypotheses uvtxel.v ⊢ V = Vtx ⁡ G
isuvtx.e ⊢ E = Edg ⁡ G
Assertion isuvtx ⊢ UnivVtx ⁡ G = v ∈ V | ∀ k ∈ V ∖ v ∃ e ∈ E k v ⊆ e

Proof

Step Hyp Ref Expression
1 uvtxel.v ⊢ V = Vtx ⁡ G
2 isuvtx.e ⊢ E = Edg ⁡ G
3 1 uvtxval ⊢ UnivVtx ⁡ G = v ∈ V | ∀ k ∈ V ∖ v k ∈ G NeighbVtx v
4 1 2 nbgrel ⊢ k ∈ G NeighbVtx v ↔ k ∈ V ∧ v ∈ V ∧ k ≠ v ∧ ∃ e ∈ E v k ⊆ e
5 df-3an ⊢ k ∈ V ∧ v ∈ V ∧ k ≠ v ∧ ∃ e ∈ E v k ⊆ e ↔ k ∈ V ∧ v ∈ V ∧ k ≠ v ∧ ∃ e ∈ E v k ⊆ e
6 4 5 bitri ⊢ k ∈ G NeighbVtx v ↔ k ∈ V ∧ v ∈ V ∧ k ≠ v ∧ ∃ e ∈ E v k ⊆ e
7 prcom ⊢ k v = v k
8 7 sseq1i ⊢ k v ⊆ e ↔ v k ⊆ e
9 8 rexbii ⊢ ∃ e ∈ E k v ⊆ e ↔ ∃ e ∈ E v k ⊆ e
10 id ⊢ v ∈ V → v ∈ V
11 eldifi ⊢ k ∈ V ∖ v → k ∈ V
12 10 11 anim12ci ⊢ v ∈ V ∧ k ∈ V ∖ v → k ∈ V ∧ v ∈ V
13 eldifsni ⊢ k ∈ V ∖ v → k ≠ v
14 13 adantl ⊢ v ∈ V ∧ k ∈ V ∖ v → k ≠ v
15 12 14 jca ⊢ v ∈ V ∧ k ∈ V ∖ v → k ∈ V ∧ v ∈ V ∧ k ≠ v
16 15 biantrurd ⊢ v ∈ V ∧ k ∈ V ∖ v → ∃ e ∈ E v k ⊆ e ↔ k ∈ V ∧ v ∈ V ∧ k ≠ v ∧ ∃ e ∈ E v k ⊆ e
17 9 16 bitr2id ⊢ v ∈ V ∧ k ∈ V ∖ v → k ∈ V ∧ v ∈ V ∧ k ≠ v ∧ ∃ e ∈ E v k ⊆ e ↔ ∃ e ∈ E k v ⊆ e
18 6 17 syl5bb ⊢ v ∈ V ∧ k ∈ V ∖ v → k ∈ G NeighbVtx v ↔ ∃ e ∈ E k v ⊆ e
19 18 ralbidva ⊢ v ∈ V → ∀ k ∈ V ∖ v k ∈ G NeighbVtx v ↔ ∀ k ∈ V ∖ v ∃ e ∈ E k v ⊆ e
20 19 rabbiia ⊢ v ∈ V | ∀ k ∈ V ∖ v k ∈ G NeighbVtx v = v ∈ V | ∀ k ∈ V ∖ v ∃ e ∈ E k v ⊆ e
21 3 20 eqtri ⊢ UnivVtx ⁡ G = v ∈ V | ∀ k ∈ V ∖ v ∃ e ∈ E k v ⊆ e