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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
cplgredgex.2 ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion cplgredgex ( 𝐺 ∈ ComplGraph → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝑉 ∖ { 𝐴 } ) ) → ∃ 𝑒 ∈ 𝐸 { 𝐴 , 𝐵 } ⊆ 𝑒 ) )

Proof

Step Hyp Ref Expression
1 cplgredgex.1 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 cplgredgex.2 ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 simp2 ⊢ ( ( 𝐺 ∈ ComplGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝑉 ∖ { 𝐴 } ) ) → 𝐴 ∈ 𝑉 )
4 simp3 ⊢ ( ( 𝐺 ∈ ComplGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝑉 ∖ { 𝐴 } ) ) → 𝐵 ∈ ( 𝑉 ∖ { 𝐴 } ) )
5 eleq1 ⊢ ( 𝑎 = 𝐴 → ( 𝑎 ∈ 𝑉 ↔ 𝐴 ∈ 𝑉 ) )
6 sneq ⊢ ( 𝑎 = 𝐴 → { 𝑎 } = { 𝐴 } )
7 6 difeq2d ⊢ ( 𝑎 = 𝐴 → ( 𝑉 ∖ { 𝑎 } ) = ( 𝑉 ∖ { 𝐴 } ) )
8 7 eleq2d ⊢ ( 𝑎 = 𝐴 → ( 𝑏 ∈ ( 𝑉 ∖ { 𝑎 } ) ↔ 𝑏 ∈ ( 𝑉 ∖ { 𝐴 } ) ) )
9 5 8 anbi12d ⊢ ( 𝑎 = 𝐴 → ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ ( 𝑉 ∖ { 𝑎 } ) ) ↔ ( 𝐴 ∈ 𝑉 ∧ 𝑏 ∈ ( 𝑉 ∖ { 𝐴 } ) ) ) )
10 preq1 ⊢ ( 𝑎 = 𝐴 → { 𝑎 , 𝑏 } = { 𝐴 , 𝑏 } )
11 10 sseq1d ⊢ ( 𝑎 = 𝐴 → ( { 𝑎 , 𝑏 } ⊆ 𝑒 ↔ { 𝐴 , 𝑏 } ⊆ 𝑒 ) )
12 11 rexbidv ⊢ ( 𝑎 = 𝐴 → ( ∃ 𝑒 ∈ 𝐸 { 𝑎 , 𝑏 } ⊆ 𝑒 ↔ ∃ 𝑒 ∈ 𝐸 { 𝐴 , 𝑏 } ⊆ 𝑒 ) )
13 9 12 imbi12d ⊢ ( 𝑎 = 𝐴 → ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ ( 𝑉 ∖ { 𝑎 } ) ) → ∃ 𝑒 ∈ 𝐸 { 𝑎 , 𝑏 } ⊆ 𝑒 ) ↔ ( ( 𝐴 ∈ 𝑉 ∧ 𝑏 ∈ ( 𝑉 ∖ { 𝐴 } ) ) → ∃ 𝑒 ∈ 𝐸 { 𝐴 , 𝑏 } ⊆ 𝑒 ) ) )
14 eleq1 ⊢ ( 𝑏 = 𝐵 → ( 𝑏 ∈ ( 𝑉 ∖ { 𝐴 } ) ↔ 𝐵 ∈ ( 𝑉 ∖ { 𝐴 } ) ) )
15 14 anbi2d ⊢ ( 𝑏 = 𝐵 → ( ( 𝐴 ∈ 𝑉 ∧ 𝑏 ∈ ( 𝑉 ∖ { 𝐴 } ) ) ↔ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝑉 ∖ { 𝐴 } ) ) ) )
16 preq2 ⊢ ( 𝑏 = 𝐵 → { 𝐴 , 𝑏 } = { 𝐴 , 𝐵 } )
17 16 sseq1d ⊢ ( 𝑏 = 𝐵 → ( { 𝐴 , 𝑏 } ⊆ 𝑒 ↔ { 𝐴 , 𝐵 } ⊆ 𝑒 ) )
18 17 rexbidv ⊢ ( 𝑏 = 𝐵 → ( ∃ 𝑒 ∈ 𝐸 { 𝐴 , 𝑏 } ⊆ 𝑒 ↔ ∃ 𝑒 ∈ 𝐸 { 𝐴 , 𝐵 } ⊆ 𝑒 ) )
19 15 18 imbi12d ⊢ ( 𝑏 = 𝐵 → ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑏 ∈ ( 𝑉 ∖ { 𝐴 } ) ) → ∃ 𝑒 ∈ 𝐸 { 𝐴 , 𝑏 } ⊆ 𝑒 ) ↔ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝑉 ∖ { 𝐴 } ) ) → ∃ 𝑒 ∈ 𝐸 { 𝐴 , 𝐵 } ⊆ 𝑒 ) ) )
20 13 19 sylan9bb ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ ( 𝑉 ∖ { 𝑎 } ) ) → ∃ 𝑒 ∈ 𝐸 { 𝑎 , 𝑏 } ⊆ 𝑒 ) ↔ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝑉 ∖ { 𝐴 } ) ) → ∃ 𝑒 ∈ 𝐸 { 𝐴 , 𝐵 } ⊆ 𝑒 ) ) )
21 1 2 iscplgredg ⊢ ( 𝐺 ∈ ComplGraph → ( 𝐺 ∈ ComplGraph ↔ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ ( 𝑉 ∖ { 𝑎 } ) ∃ 𝑒 ∈ 𝐸 { 𝑎 , 𝑏 } ⊆ 𝑒 ) )
22 21 ibi ⊢ ( 𝐺 ∈ ComplGraph → ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ ( 𝑉 ∖ { 𝑎 } ) ∃ 𝑒 ∈ 𝐸 { 𝑎 , 𝑏 } ⊆ 𝑒 )
23 rsp2 ⊢ ( ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ ( 𝑉 ∖ { 𝑎 } ) ∃ 𝑒 ∈ 𝐸 { 𝑎 , 𝑏 } ⊆ 𝑒 → ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ ( 𝑉 ∖ { 𝑎 } ) ) → ∃ 𝑒 ∈ 𝐸 { 𝑎 , 𝑏 } ⊆ 𝑒 ) )
24 22 23 syl ⊢ ( 𝐺 ∈ ComplGraph → ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ ( 𝑉 ∖ { 𝑎 } ) ) → ∃ 𝑒 ∈ 𝐸 { 𝑎 , 𝑏 } ⊆ 𝑒 ) )
25 24 3ad2ant1 ⊢ ( ( 𝐺 ∈ ComplGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝑉 ∖ { 𝐴 } ) ) → ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ ( 𝑉 ∖ { 𝑎 } ) ) → ∃ 𝑒 ∈ 𝐸 { 𝑎 , 𝑏 } ⊆ 𝑒 ) )
26 3 4 20 25 vtocl2d ⊢ ( ( 𝐺 ∈ ComplGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝑉 ∖ { 𝐴 } ) ) → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝑉 ∖ { 𝐴 } ) ) → ∃ 𝑒 ∈ 𝐸 { 𝐴 , 𝐵 } ⊆ 𝑒 ) )
27 3 4 26 mp2and ⊢ ( ( 𝐺 ∈ ComplGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝑉 ∖ { 𝐴 } ) ) → ∃ 𝑒 ∈ 𝐸 { 𝐴 , 𝐵 } ⊆ 𝑒 )
28 27 3expib ⊢ ( 𝐺 ∈ ComplGraph → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝑉 ∖ { 𝐴 } ) ) → ∃ 𝑒 ∈ 𝐸 { 𝐴 , 𝐵 } ⊆ 𝑒 ) )