Metamath Proof Explorer

Theorem iscplgredg

Description: A graph G is complete iff all vertices are connected with each other by (at least) one edge. (Contributed by AV, 10-Nov-2020)

Ref Expression
Hypotheses cplgruvtxb.v ⊢ V = Vtx ⁡ G
iscplgredg.v ⊢ E = Edg ⁡ G
Assertion iscplgredg ⊢ G ∈ W → G ∈ ComplGraph ↔ ∀ v ∈ V ∀ n ∈ V ∖ v ∃ e ∈ E v n ⊆ e

Proof

Step Hyp Ref Expression
1 cplgruvtxb.v ⊢ V = Vtx ⁡ G
2 iscplgredg.v ⊢ E = Edg ⁡ G
3 1 iscplgrnb ⊢ G ∈ W → G ∈ ComplGraph ↔ ∀ v ∈ V ∀ n ∈ V ∖ v n ∈ G NeighbVtx v
4 df-3an ⊢ n ∈ V ∧ v ∈ V ∧ n ≠ v ∧ ∃ e ∈ E v n ⊆ e ↔ n ∈ V ∧ v ∈ V ∧ n ≠ v ∧ ∃ e ∈ E v n ⊆ e
5 4 a1i ⊢ G ∈ W ∧ v ∈ V ∧ n ∈ V ∖ v → n ∈ V ∧ v ∈ V ∧ n ≠ v ∧ ∃ e ∈ E v n ⊆ e ↔ n ∈ V ∧ v ∈ V ∧ n ≠ v ∧ ∃ e ∈ E v n ⊆ e
6 1 2 nbgrel ⊢ n ∈ G NeighbVtx v ↔ n ∈ V ∧ v ∈ V ∧ n ≠ v ∧ ∃ e ∈ E v n ⊆ e
7 6 a1i ⊢ G ∈ W ∧ v ∈ V ∧ n ∈ V ∖ v → n ∈ G NeighbVtx v ↔ n ∈ V ∧ v ∈ V ∧ n ≠ v ∧ ∃ e ∈ E v n ⊆ e
8 eldifsn ⊢ n ∈ V ∖ v ↔ n ∈ V ∧ n ≠ v
9 simpr ⊢ G ∈ W ∧ v ∈ V → v ∈ V
10 simpl ⊢ n ∈ V ∧ n ≠ v → n ∈ V
11 9 10 anim12ci ⊢ G ∈ W ∧ v ∈ V ∧ n ∈ V ∧ n ≠ v → n ∈ V ∧ v ∈ V
12 simprr ⊢ G ∈ W ∧ v ∈ V ∧ n ∈ V ∧ n ≠ v → n ≠ v
13 11 12 jca ⊢ G ∈ W ∧ v ∈ V ∧ n ∈ V ∧ n ≠ v → n ∈ V ∧ v ∈ V ∧ n ≠ v
14 8 13 sylan2b ⊢ G ∈ W ∧ v ∈ V ∧ n ∈ V ∖ v → n ∈ V ∧ v ∈ V ∧ n ≠ v
15 14 biantrurd ⊢ G ∈ W ∧ v ∈ V ∧ n ∈ V ∖ v → ∃ e ∈ E v n ⊆ e ↔ n ∈ V ∧ v ∈ V ∧ n ≠ v ∧ ∃ e ∈ E v n ⊆ e
16 5 7 15 3bitr4d ⊢ G ∈ W ∧ v ∈ V ∧ n ∈ V ∖ v → n ∈ G NeighbVtx v ↔ ∃ e ∈ E v n ⊆ e
17 16 ralbidva ⊢ G ∈ W ∧ v ∈ V → ∀ n ∈ V ∖ v n ∈ G NeighbVtx v ↔ ∀ n ∈ V ∖ v ∃ e ∈ E v n ⊆ e
18 17 ralbidva ⊢ G ∈ W → ∀ v ∈ V ∀ n ∈ V ∖ v n ∈ G NeighbVtx v ↔ ∀ v ∈ V ∀ n ∈ V ∖ v ∃ e ∈ E v n ⊆ e
19 3 18 bitrd ⊢ G ∈ W → G ∈ ComplGraph ↔ ∀ v ∈ V ∀ n ∈ V ∖ v ∃ e ∈ E v n ⊆ e