Metamath Proof Explorer

Theorem cusgredgex

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

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

Proof

Step Hyp Ref Expression
1 cusgredgex.1 ⊢V=Vtx⁡G
2 cusgredgex.2 ⊢E=Edg⁡G
3 cusgrcplgr ⊢G∈ComplUSGraph→G∈ComplGraph
4 1 2 cplgredgex ⊢G∈ComplGraph→A∈V∧B∈V∖A→∃e∈EAB⊆e
5 3 4 syl ⊢G∈ComplUSGraph→A∈V∧B∈V∖A→∃e∈EAB⊆e
6 5 imp ⊢G∈ComplUSGraph∧A∈V∧B∈V∖A→∃e∈EAB⊆e
7 df-rex ⊢∃e∈EAB⊆e↔∃ee∈E∧AB⊆e
8 6 7 sylib ⊢G∈ComplUSGraph∧A∈V∧B∈V∖A→∃ee∈E∧AB⊆e
9 eldifsni ⊢B∈V∖A→B≠A
10 9 necomd ⊢B∈V∖A→A≠B
11 10 adantl ⊢A∈V∧B∈V∖A→A≠B
12 hashprg ⊢A∈V∧B∈V∖A→A≠B↔AB=2
13 11 12 mpbid ⊢A∈V∧B∈V∖A→AB=2
14 13 adantl ⊢G∈ComplUSGraph∧e∈E∧A∈V∧B∈V∖A→AB=2
15 cusgrusgr ⊢G∈ComplUSGraph→G∈USGraph
16 2 usgredgppr ⊢G∈USGraph∧e∈E→e=2
17 15 16 sylan ⊢G∈ComplUSGraph∧e∈E→e=2
18 17 adantr ⊢G∈ComplUSGraph∧e∈E∧A∈V∧B∈V∖A→e=2
19 14 18 eqtr4d ⊢G∈ComplUSGraph∧e∈E∧A∈V∧B∈V∖A→AB=e
20 simpl ⊢G∈ComplUSGraph∧e∈E∧A∈V∧B∈V∖A→G∈ComplUSGraph∧e∈E
21 vex ⊢e∈V
22 2nn0 ⊢2∈ℕ0
23 hashvnfin ⊢e∈V∧2∈ℕ0→e=2→e∈Fin
24 21 22 23 mp2an ⊢e=2→e∈Fin
25 17 24 syl ⊢G∈ComplUSGraph∧e∈E→e∈Fin
26 fisshasheq ⊢e∈Fin∧AB⊆e∧AB=e→AB=e
27 25 26 syl3an1 ⊢G∈ComplUSGraph∧e∈E∧AB⊆e∧AB=e→AB=e
28 27 3comr ⊢AB=e∧G∈ComplUSGraph∧e∈E∧AB⊆e→AB=e
29 28 3exp ⊢AB=e→G∈ComplUSGraph∧e∈E→AB⊆e→AB=e
30 19 20 29 sylc ⊢G∈ComplUSGraph∧e∈E∧A∈V∧B∈V∖A→AB⊆e→AB=e
31 30 3impa ⊢G∈ComplUSGraph∧e∈E∧A∈V∧B∈V∖A→AB⊆e→AB=e
32 31 3com23 ⊢G∈ComplUSGraph∧A∈V∧B∈V∖A∧e∈E→AB⊆e→AB=e
33 32 3expia ⊢G∈ComplUSGraph∧A∈V∧B∈V∖A→e∈E→AB⊆e→AB=e
34 33 imdistand ⊢G∈ComplUSGraph∧A∈V∧B∈V∖A→e∈E∧AB⊆e→e∈E∧AB=e
35 34 eximdv ⊢G∈ComplUSGraph∧A∈V∧B∈V∖A→∃ee∈E∧AB⊆e→∃ee∈E∧AB=e
36 8 35 mpd ⊢G∈ComplUSGraph∧A∈V∧B∈V∖A→∃ee∈E∧AB=e
37 pm3.22 ⊢e∈E∧AB=e→AB=e∧e∈E
38 eqcom ⊢AB=e↔e=AB
39 38 anbi1i ⊢AB=e∧e∈E↔e=AB∧e∈E
40 37 39 sylib ⊢e∈E∧AB=e→e=AB∧e∈E
41 40 eximi ⊢∃ee∈E∧AB=e→∃ee=AB∧e∈E
42 36 41 syl ⊢G∈ComplUSGraph∧A∈V∧B∈V∖A→∃ee=AB∧e∈E
43 prex ⊢AB∈V
44 eleq1 ⊢e=AB→e∈E↔AB∈E
45 43 44 ceqsexv ⊢∃ee=AB∧e∈E↔AB∈E
46 42 45 sylib ⊢G∈ComplUSGraph∧A∈V∧B∈V∖A→AB∈E
47 46 ex ⊢G∈ComplUSGraph→A∈V∧B∈V∖A→AB∈E