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 ∈ E A B ⊆ 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 → a b = A b
11 10 sseq1d ⊢ a = A → a b ⊆ e ↔ A b ⊆ e
12 11 rexbidv ⊢ a = A → ∃ e ∈ E a b ⊆ e ↔ ∃ e ∈ E A b ⊆ e
13 9 12 imbi12d ⊢ a = A → a ∈ V ∧ b ∈ V ∖ a → ∃ e ∈ E a b ⊆ e ↔ A ∈ V ∧ b ∈ V ∖ A → ∃ e ∈ E A b ⊆ 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 → A b = A B
17 16 sseq1d ⊢ b = B → A b ⊆ e ↔ A B ⊆ e
18 17 rexbidv ⊢ b = B → ∃ e ∈ E A b ⊆ e ↔ ∃ e ∈ E A B ⊆ e
19 15 18 imbi12d ⊢ b = B → A ∈ V ∧ b ∈ V ∖ A → ∃ e ∈ E A b ⊆ e ↔ A ∈ V ∧ B ∈ V ∖ A → ∃ e ∈ E A B ⊆ e
20 13 19 sylan9bb ⊢ a = A ∧ b = B → a ∈ V ∧ b ∈ V ∖ a → ∃ e ∈ E a b ⊆ e ↔ A ∈ V ∧ B ∈ V ∖ A → ∃ e ∈ E A B ⊆ e
21 1 2 iscplgredg ⊢ G ∈ ComplGraph → G ∈ ComplGraph ↔ ∀ a ∈ V ∀ b ∈ V ∖ a ∃ e ∈ E a b ⊆ e
22 21 ibi ⊢ G ∈ ComplGraph → ∀ a ∈ V ∀ b ∈ V ∖ a ∃ e ∈ E a b ⊆ e
23 rsp2 ⊢ ∀ a ∈ V ∀ b ∈ V ∖ a ∃ e ∈ E a b ⊆ e → a ∈ V ∧ b ∈ V ∖ a → ∃ e ∈ E a b ⊆ e
24 22 23 syl ⊢ G ∈ ComplGraph → a ∈ V ∧ b ∈ V ∖ a → ∃ e ∈ E a b ⊆ e
25 24 3ad2ant1 ⊢ G ∈ ComplGraph ∧ A ∈ V ∧ B ∈ V ∖ A → a ∈ V ∧ b ∈ V ∖ a → ∃ e ∈ E a b ⊆ e
26 3 4 20 25 vtocl2d ⊢ G ∈ ComplGraph ∧ A ∈ V ∧ B ∈ V ∖ A → A ∈ V ∧ B ∈ V ∖ A → ∃ e ∈ E A B ⊆ e
27 3 4 26 mp2and ⊢ G ∈ ComplGraph ∧ A ∈ V ∧ B ∈ V ∖ A → ∃ e ∈ E A B ⊆ e
28 27 3expib ⊢ G ∈ ComplGraph → A ∈ V ∧ B ∈ V ∖ A → ∃ e ∈ E A B ⊆ e