Metamath Proof Explorer

Theorem cplgredgex

Description: Any two (distinct) vertices in a complete graph are connected to each other by at least one edge. (Contributed by BTernaryTau, 2-Oct-2023)

Ref Expression
Hypotheses cplgredgex.1 ⊢V=Vtx⁡G
cplgredgex.2 ⊢E=Edg⁡G
Assertion cplgredgex ⊢G∈ComplGraph→A∈V∧B∈V∖A→∃e∈EAB⊆e

Proof

Step Hyp Ref Expression
1 cplgredgex.1 ⊢V=Vtx⁡G
2 cplgredgex.2 ⊢E=Edg⁡G
3 simp2 ⊢G∈ComplGraph∧A∈V∧B∈V∖A→A∈V
4 simp3 ⊢G∈ComplGraph∧A∈V∧B∈V∖A→B∈V∖A
5 eleq1 ⊢a=A→a∈V↔A∈V
6 sneq ⊢a=A→a=A
7 6 difeq2d ⊢a=A→V∖a=V∖A
8 7 eleq2d ⊢a=A→b∈V∖a↔b∈V∖A
9 5 8 anbi12d ⊢a=A→a∈V∧b∈V∖a↔A∈V∧b∈V∖A
10 preq1 ⊢a=A→ab=Ab
11 10 sseq1d ⊢a=A→ab⊆e↔Ab⊆e
12 11 rexbidv ⊢a=A→∃e∈Eab⊆e↔∃e∈EAb⊆e
13 9 12 imbi12d ⊢a=A→a∈V∧b∈V∖a→∃e∈Eab⊆e↔A∈V∧b∈V∖A→∃e∈EAb⊆e
14 eleq1 ⊢b=B→b∈V∖A↔B∈V∖A
15 14 anbi2d ⊢b=B→A∈V∧b∈V∖A↔A∈V∧B∈V∖A
16 preq2 ⊢b=B→Ab=AB
17 16 sseq1d ⊢b=B→Ab⊆e↔AB⊆e
18 17 rexbidv ⊢b=B→∃e∈EAb⊆e↔∃e∈EAB⊆e
19 15 18 imbi12d ⊢b=B→A∈V∧b∈V∖A→∃e∈EAb⊆e↔A∈V∧B∈V∖A→∃e∈EAB⊆e
20 13 19 sylan9bb ⊢a=A∧b=B→a∈V∧b∈V∖a→∃e∈Eab⊆e↔A∈V∧B∈V∖A→∃e∈EAB⊆e
21 1 2 iscplgredg ⊢G∈ComplGraph→G∈ComplGraph↔∀a∈V∀b∈V∖a∃e∈Eab⊆e
22 21 ibi ⊢G∈ComplGraph→∀a∈V∀b∈V∖a∃e∈Eab⊆e
23 rsp2 ⊢∀a∈V∀b∈V∖a∃e∈Eab⊆e→a∈V∧b∈V∖a→∃e∈Eab⊆e
24 22 23 syl ⊢G∈ComplGraph→a∈V∧b∈V∖a→∃e∈Eab⊆e
25 24 3ad2ant1 ⊢G∈ComplGraph∧A∈V∧B∈V∖A→a∈V∧b∈V∖a→∃e∈Eab⊆e
26 3 4 20 25 vtocl2d ⊢G∈ComplGraph∧A∈V∧B∈V∖A→A∈V∧B∈V∖A→∃e∈EAB⊆e
27 3 4 26 mp2and ⊢G∈ComplGraph∧A∈V∧B∈V∖A→∃e∈EAB⊆e
28 27 3expib ⊢G∈ComplGraph→A∈V∧B∈V∖A→∃e∈EAB⊆e