Metamath Proof Explorer

Theorem cplgr2vpr

Description: An undirected hypergraph with two (different) vertices is complete iff there is an edge between these two vertices. (Contributed by Alexander van der Vekens, 12-Oct-2017) (Proof shortened by Alexander van der Vekens, 16-Dec-2017) (Revised by AV, 3-Nov-2020)

Ref Expression
Hypotheses cplgr0v.v ⊢ V = Vtx ⁡ G
cplgr2v.e ⊢ E = Edg ⁡ G
Assertion cplgr2vpr ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ G ∈ UHGraph ∧ V = A B → G ∈ ComplGraph ↔ A B ∈ E

Proof

Step Hyp Ref Expression
1 cplgr0v.v ⊢ V = Vtx ⁡ G
2 cplgr2v.e ⊢ E = Edg ⁡ G
3 simpl ⊢ G ∈ UHGraph ∧ V = A B → G ∈ UHGraph
4 fveq2 ⊢ V = A B → V = A B
5 4 adantl ⊢ G ∈ UHGraph ∧ V = A B → V = A B
6 elex ⊢ A ∈ X → A ∈ V
7 elex ⊢ B ∈ Y → B ∈ V
8 id ⊢ A ≠ B → A ≠ B
9 hashprb ⊢ A ∈ V ∧ B ∈ V ∧ A ≠ B ↔ A B = 2
10 9 biimpi ⊢ A ∈ V ∧ B ∈ V ∧ A ≠ B → A B = 2
11 6 7 8 10 syl3an ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B → A B = 2
12 5 11 sylan9eqr ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ G ∈ UHGraph ∧ V = A B → V = 2
13 1 2 cplgr2v ⊢ G ∈ UHGraph ∧ V = 2 → G ∈ ComplGraph ↔ V ∈ E
14 3 12 13 syl2an2 ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ G ∈ UHGraph ∧ V = A B → G ∈ ComplGraph ↔ V ∈ E
15 simprr ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ G ∈ UHGraph ∧ V = A B → V = A B
16 15 eleq1d ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ G ∈ UHGraph ∧ V = A B → V ∈ E ↔ A B ∈ E
17 14 16 bitrd ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ G ∈ UHGraph ∧ V = A B → G ∈ ComplGraph ↔ A B ∈ E