Metamath Proof Explorer

Theorem uvtxel1

Description: Characterization of a universal vertex. (Contributed by Alexander van der Vekens, 12-Oct-2017) (Revised by AV, 14-Feb-2022)

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

Proof

Step Hyp Ref Expression
1 uvtxel.v ⊢ V = Vtx ⁡ G
2 isuvtx.e ⊢ E = Edg ⁡ G
3 sneq ⊢ n = N → n = N
4 3 difeq2d ⊢ n = N → V ∖ n = V ∖ N
5 preq2 ⊢ n = N → k n = k N
6 5 sseq1d ⊢ n = N → k n ⊆ e ↔ k N ⊆ e
7 6 rexbidv ⊢ n = N → ∃ e ∈ E k n ⊆ e ↔ ∃ e ∈ E k N ⊆ e
8 4 7 raleqbidv ⊢ n = N → ∀ k ∈ V ∖ n ∃ e ∈ E k n ⊆ e ↔ ∀ k ∈ V ∖ N ∃ e ∈ E k N ⊆ e
9 1 2 isuvtx ⊢ UnivVtx ⁡ G = n ∈ V | ∀ k ∈ V ∖ n ∃ e ∈ E k n ⊆ e
10 8 9 elrab2 ⊢ N ∈ UnivVtx ⁡ G ↔ N ∈ V ∧ ∀ k ∈ V ∖ N ∃ e ∈ E k N ⊆ e