Metamath Proof Explorer

Theorem cusgredgex2

Description: Any two distinct vertices in a complete simple graph are connected to each other by an edge. (Contributed by BTernaryTau, 4-Oct-2023)

Ref Expression
Hypotheses cusgredgex2.1 ⊢ V = Vtx ⁡ G
cusgredgex2.2 ⊢ E = Edg ⁡ G
Assertion cusgredgex2 ⊢ G ∈ ComplUSGraph → A ∈ V ∧ B ∈ V ∧ A ≠ B → A B ∈ E

Proof

Step Hyp Ref Expression
1 cusgredgex2.1 ⊢ V = Vtx ⁡ G
2 cusgredgex2.2 ⊢ E = Edg ⁡ G
3 eldifsn ⊢ B ∈ V ∖ A ↔ B ∈ V ∧ B ≠ A
4 necom ⊢ B ≠ A ↔ A ≠ B
5 4 anbi2i ⊢ B ∈ V ∧ B ≠ A ↔ B ∈ V ∧ A ≠ B
6 3 5 sylbbr ⊢ B ∈ V ∧ A ≠ B → B ∈ V ∖ A
7 6 anim2i ⊢ A ∈ V ∧ B ∈ V ∧ A ≠ B → A ∈ V ∧ B ∈ V ∖ A
8 7 3impb ⊢ A ∈ V ∧ B ∈ V ∧ A ≠ B → A ∈ V ∧ B ∈ V ∖ A
9 1 2 cusgredgex ⊢ G ∈ ComplUSGraph → A ∈ V ∧ B ∈ V ∖ A → A B ∈ E
10 8 9 syl5 ⊢ G ∈ ComplUSGraph → A ∈ V ∧ B ∈ V ∧ A ≠ B → A B ∈ E