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 e. ComplGraph -> ( ( A e. V /\ B e. ( V \ { A } ) ) -> E. e e. E { A , B } C_ e ) )

Proof

Step	Hyp	Ref	Expression
1		cplgredgex.1	|- V = ( Vtx ` G )
2		cplgredgex.2	|- E = ( Edg ` G )
3		simp2	|- ( ( G e. ComplGraph /\ A e. V /\ B e. ( V \ { A } ) ) -> A e. V )
4		simp3	|- ( ( G e. ComplGraph /\ A e. V /\ B e. ( V \ { A } ) ) -> B e. ( V \ { A } ) )
5		eleq1	|- ( a = A -> ( a e. V <-> A e. V ) )
6		sneq	|- ( a = A -> { a } = { A } )
7	6	difeq2d	|- ( a = A -> ( V \ { a } ) = ( V \ { A } ) )
8	7	eleq2d	|- ( a = A -> ( b e. ( V \ { a } ) <-> b e. ( V \ { A } ) ) )
9	5 8	anbi12d	|- ( a = A -> ( ( a e. V /\ b e. ( V \ { a } ) ) <-> ( A e. V /\ b e. ( V \ { A } ) ) ) )
10		preq1	|- ( a = A -> { a , b } = { A , b } )
11	10	sseq1d	|- ( a = A -> ( { a , b } C_ e <-> { A , b } C_ e ) )
12	11	rexbidv	|- ( a = A -> ( E. e e. E { a , b } C_ e <-> E. e e. E { A , b } C_ e ) )
13	9 12	imbi12d	|- ( a = A -> ( ( ( a e. V /\ b e. ( V \ { a } ) ) -> E. e e. E { a , b } C_ e ) <-> ( ( A e. V /\ b e. ( V \ { A } ) ) -> E. e e. E { A , b } C_ e ) ) )
14		eleq1	|- ( b = B -> ( b e. ( V \ { A } ) <-> B e. ( V \ { A } ) ) )
15	14	anbi2d	|- ( b = B -> ( ( A e. V /\ b e. ( V \ { A } ) ) <-> ( A e. V /\ B e. ( V \ { A } ) ) ) )
16		preq2	|- ( b = B -> { A , b } = { A , B } )
17	16	sseq1d	|- ( b = B -> ( { A , b } C_ e <-> { A , B } C_ e ) )
18	17	rexbidv	|- ( b = B -> ( E. e e. E { A , b } C_ e <-> E. e e. E { A , B } C_ e ) )
19	15 18	imbi12d	|- ( b = B -> ( ( ( A e. V /\ b e. ( V \ { A } ) ) -> E. e e. E { A , b } C_ e ) <-> ( ( A e. V /\ B e. ( V \ { A } ) ) -> E. e e. E { A , B } C_ e ) ) )
20	13 19	sylan9bb	|- ( ( a = A /\ b = B ) -> ( ( ( a e. V /\ b e. ( V \ { a } ) ) -> E. e e. E { a , b } C_ e ) <-> ( ( A e. V /\ B e. ( V \ { A } ) ) -> E. e e. E { A , B } C_ e ) ) )
21	1 2	iscplgredg	|- ( G e. ComplGraph -> ( G e. ComplGraph <-> A. a e. V A. b e. ( V \ { a } ) E. e e. E { a , b } C_ e ) )
22	21	ibi	|- ( G e. ComplGraph -> A. a e. V A. b e. ( V \ { a } ) E. e e. E { a , b } C_ e )
23		rsp2	|- ( A. a e. V A. b e. ( V \ { a } ) E. e e. E { a , b } C_ e -> ( ( a e. V /\ b e. ( V \ { a } ) ) -> E. e e. E { a , b } C_ e ) )
24	22 23	syl	|- ( G e. ComplGraph -> ( ( a e. V /\ b e. ( V \ { a } ) ) -> E. e e. E { a , b } C_ e ) )
25	24	3ad2ant1	|- ( ( G e. ComplGraph /\ A e. V /\ B e. ( V \ { A } ) ) -> ( ( a e. V /\ b e. ( V \ { a } ) ) -> E. e e. E { a , b } C_ e ) )
26	3 4 20 25	vtocl2d	|- ( ( G e. ComplGraph /\ A e. V /\ B e. ( V \ { A } ) ) -> ( ( A e. V /\ B e. ( V \ { A } ) ) -> E. e e. E { A , B } C_ e ) )
27	3 4 26	mp2and	|- ( ( G e. ComplGraph /\ A e. V /\ B e. ( V \ { A } ) ) -> E. e e. E { A , B } C_ e )
28	27	3expib	|- ( G e. ComplGraph -> ( ( A e. V /\ B e. ( V \ { A } ) ) -> E. e e. E { A , B } C_ e ) )