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 → A B ∈ 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 ∈ E A B ⊆ e
5 3 4 syl ⊢ G ∈ ComplUSGraph → A ∈ V ∧ B ∈ V ∖ A → ∃ e ∈ E A B ⊆ e
6 5 imp ⊢ G ∈ ComplUSGraph ∧ A ∈ V ∧ B ∈ V ∖ A → ∃ e ∈ E A B ⊆ e
7 df-rex ⊢ ∃ e ∈ E A B ⊆ e ↔ ∃ e e ∈ E ∧ A B ⊆ e
8 6 7 sylib ⊢ G ∈ ComplUSGraph ∧ A ∈ V ∧ B ∈ V ∖ A → ∃ e e ∈ E ∧ A B ⊆ 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 ↔ A B = 2
13 11 12 mpbid ⊢ A ∈ V ∧ B ∈ V ∖ A → A B = 2
14 13 adantl ⊢ G ∈ ComplUSGraph ∧ e ∈ E ∧ A ∈ V ∧ B ∈ V ∖ A → A B = 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 → A B = 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 ∧ A B ⊆ e ∧ A B = e → A B = e
27 25 26 syl3an1 ⊢ G ∈ ComplUSGraph ∧ e ∈ E ∧ A B ⊆ e ∧ A B = e → A B = e
28 27 3comr ⊢ A B = e ∧ G ∈ ComplUSGraph ∧ e ∈ E ∧ A B ⊆ e → A B = e
29 28 3exp ⊢ A B = e → G ∈ ComplUSGraph ∧ e ∈ E → A B ⊆ e → A B = e
30 19 20 29 sylc ⊢ G ∈ ComplUSGraph ∧ e ∈ E ∧ A ∈ V ∧ B ∈ V ∖ A → A B ⊆ e → A B = e
31 30 3impa ⊢ G ∈ ComplUSGraph ∧ e ∈ E ∧ A ∈ V ∧ B ∈ V ∖ A → A B ⊆ e → A B = e
32 31 3com23 ⊢ G ∈ ComplUSGraph ∧ A ∈ V ∧ B ∈ V ∖ A ∧ e ∈ E → A B ⊆ e → A B = e
33 32 3expia ⊢ G ∈ ComplUSGraph ∧ A ∈ V ∧ B ∈ V ∖ A → e ∈ E → A B ⊆ e → A B = e
34 33 imdistand ⊢ G ∈ ComplUSGraph ∧ A ∈ V ∧ B ∈ V ∖ A → e ∈ E ∧ A B ⊆ e → e ∈ E ∧ A B = e
35 34 eximdv ⊢ G ∈ ComplUSGraph ∧ A ∈ V ∧ B ∈ V ∖ A → ∃ e e ∈ E ∧ A B ⊆ e → ∃ e e ∈ E ∧ A B = e
36 8 35 mpd ⊢ G ∈ ComplUSGraph ∧ A ∈ V ∧ B ∈ V ∖ A → ∃ e e ∈ E ∧ A B = e
37 pm3.22 ⊢ e ∈ E ∧ A B = e → A B = e ∧ e ∈ E
38 eqcom ⊢ A B = e ↔ e = A B
39 38 anbi1i ⊢ A B = e ∧ e ∈ E ↔ e = A B ∧ e ∈ E
40 37 39 sylib ⊢ e ∈ E ∧ A B = e → e = A B ∧ e ∈ E
41 40 eximi ⊢ ∃ e e ∈ E ∧ A B = e → ∃ e e = A B ∧ e ∈ E
42 36 41 syl ⊢ G ∈ ComplUSGraph ∧ A ∈ V ∧ B ∈ V ∖ A → ∃ e e = A B ∧ e ∈ E
43 prex ⊢ A B ∈ V
44 eleq1 ⊢ e = A B → e ∈ E ↔ A B ∈ E
45 43 44 ceqsexv ⊢ ∃ e e = A B ∧ e ∈ E ↔ A B ∈ E
46 42 45 sylib ⊢ G ∈ ComplUSGraph ∧ A ∈ V ∧ B ∈ V ∖ A → A B ∈ E
47 46 ex ⊢ G ∈ ComplUSGraph → A ∈ V ∧ B ∈ V ∖ A → A B ∈ E