This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem uvtx2vtx1edgb

Description: If a hypergraph has two vertices, there is an edge between the vertices iff each vertex is universal. (Contributed by AV, 3-Nov-2020)

Ref Expression
Hypotheses uvtxel.v ⊢ V = Vtx ⁡ G
isuvtx.e ⊢ E = Edg ⁡ G
Assertion uvtx2vtx1edgb ⊢ G ∈ UHGraph ∧ V = 2 → V ∈ E ↔ ∀ v ∈ V v ∈ UnivVtx ⁡ G

Proof

Step Hyp Ref Expression
1 uvtxel.v ⊢ V = Vtx ⁡ G
2 isuvtx.e ⊢ E = Edg ⁡ G
3 1 2 nbuhgr2vtx1edgb ⊢ G ∈ UHGraph ∧ V = 2 → V ∈ E ↔ ∀ v ∈ V ∀ n ∈ V ∖ v n ∈ G NeighbVtx v
4 1 uvtxel ⊢ v ∈ UnivVtx ⁡ G ↔ v ∈ V ∧ ∀ n ∈ V ∖ v n ∈ G NeighbVtx v
5 4 a1i ⊢ G ∈ UHGraph ∧ V = 2 → v ∈ UnivVtx ⁡ G ↔ v ∈ V ∧ ∀ n ∈ V ∖ v n ∈ G NeighbVtx v
6 5 baibd ⊢ G ∈ UHGraph ∧ V = 2 ∧ v ∈ V → v ∈ UnivVtx ⁡ G ↔ ∀ n ∈ V ∖ v n ∈ G NeighbVtx v
7 6 bicomd ⊢ G ∈ UHGraph ∧ V = 2 ∧ v ∈ V → ∀ n ∈ V ∖ v n ∈ G NeighbVtx v ↔ v ∈ UnivVtx ⁡ G
8 7 ralbidva ⊢ G ∈ UHGraph ∧ V = 2 → ∀ v ∈ V ∀ n ∈ V ∖ v n ∈ G NeighbVtx v ↔ ∀ v ∈ V v ∈ UnivVtx ⁡ G
9 3 8 bitrd ⊢ G ∈ UHGraph ∧ V = 2 → V ∈ E ↔ ∀ v ∈ V v ∈ UnivVtx ⁡ G