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 → ( ( 𝐴𝑉𝐵 ∈ ( 𝑉 ∖ { 𝐴 } ) ) → ∃ 𝑒𝐸 { 𝐴 , 𝐵 } ⊆ 𝑒 ) )