Metamath Proof Explorer

Theorem cplgr2v

Description: An undirected hypergraph with two (different) vertices is complete iff there is an edge between these two vertices. (Contributed by AV, 3-Nov-2020)

Ref Expression
Hypotheses cplgr0v.v ⊢ V = Vtx ⁡ G
cplgr2v.e ⊢ E = Edg ⁡ G
Assertion cplgr2v ⊢ G ∈ UHGraph ∧ V = 2 → G ∈ ComplGraph ↔ V ∈ E

Proof

Step Hyp Ref Expression
1 cplgr0v.v ⊢ V = Vtx ⁡ G
2 cplgr2v.e ⊢ E = Edg ⁡ G
3 1 iscplgr ⊢ G ∈ UHGraph → G ∈ ComplGraph ↔ ∀ v ∈ V v ∈ UnivVtx ⁡ G
4 3 adantr ⊢ G ∈ UHGraph ∧ V = 2 → G ∈ ComplGraph ↔ ∀ v ∈ V v ∈ UnivVtx ⁡ G
5 1 2 uvtx2vtx1edgb ⊢ G ∈ UHGraph ∧ V = 2 → V ∈ E ↔ ∀ v ∈ V v ∈ UnivVtx ⁡ G
6 4 5 bitr4d ⊢ G ∈ UHGraph ∧ V = 2 → G ∈ ComplGraph ↔ V ∈ E