Theorem iscplgredg

Description: A graph G is complete iff all vertices are connected with each other by (at least) one edge. (Contributed by AV, 10-Nov-2020)

	Ref	Expression
Hypotheses	cplgruvtxb.v	|- V = ( Vtx ` G )
	iscplgredg.v	|- E = ( Edg ` G )
Assertion	iscplgredg	|- ( G e. W -> ( G e. ComplGraph <-> A. v e. V A. n e. ( V \ { v } ) E. e e. E { v , n } C_ e ) )

Proof

Step	Hyp	Ref	Expression
1		cplgruvtxb.v	|- V = ( Vtx ` G )
2		iscplgredg.v	|- E = ( Edg ` G )
3	1	iscplgrnb	|- ( G e. W -> ( G e. ComplGraph <-> A. v e. V A. n e. ( V \ { v } ) n e. ( G NeighbVtx v ) ) )
4		df-3an	|- ( ( ( n e. V /\ v e. V ) /\ n =/= v /\ E. e e. E { v , n } C_ e ) <-> ( ( ( n e. V /\ v e. V ) /\ n =/= v ) /\ E. e e. E { v , n } C_ e ) )
5	4	a1i	|- ( ( ( G e. W /\ v e. V ) /\ n e. ( V \ { v } ) ) -> ( ( ( n e. V /\ v e. V ) /\ n =/= v /\ E. e e. E { v , n } C_ e ) <-> ( ( ( n e. V /\ v e. V ) /\ n =/= v ) /\ E. e e. E { v , n } C_ e ) ) )
6	1 2	nbgrel	|- ( n e. ( G NeighbVtx v ) <-> ( ( n e. V /\ v e. V ) /\ n =/= v /\ E. e e. E { v , n } C_ e ) )
7	6	a1i	|- ( ( ( G e. W /\ v e. V ) /\ n e. ( V \ { v } ) ) -> ( n e. ( G NeighbVtx v ) <-> ( ( n e. V /\ v e. V ) /\ n =/= v /\ E. e e. E { v , n } C_ e ) ) )
8		eldifsn	|- ( n e. ( V \ { v } ) <-> ( n e. V /\ n =/= v ) )
9		simpr	|- ( ( G e. W /\ v e. V ) -> v e. V )
10		simpl	|- ( ( n e. V /\ n =/= v ) -> n e. V )
11	9 10	anim12ci	|- ( ( ( G e. W /\ v e. V ) /\ ( n e. V /\ n =/= v ) ) -> ( n e. V /\ v e. V ) )
12		simprr	|- ( ( ( G e. W /\ v e. V ) /\ ( n e. V /\ n =/= v ) ) -> n =/= v )
13	11 12	jca	|- ( ( ( G e. W /\ v e. V ) /\ ( n e. V /\ n =/= v ) ) -> ( ( n e. V /\ v e. V ) /\ n =/= v ) )
14	8 13	sylan2b	|- ( ( ( G e. W /\ v e. V ) /\ n e. ( V \ { v } ) ) -> ( ( n e. V /\ v e. V ) /\ n =/= v ) )
15	14	biantrurd	|- ( ( ( G e. W /\ v e. V ) /\ n e. ( V \ { v } ) ) -> ( E. e e. E { v , n } C_ e <-> ( ( ( n e. V /\ v e. V ) /\ n =/= v ) /\ E. e e. E { v , n } C_ e ) ) )
16	5 7 15	3bitr4d	|- ( ( ( G e. W /\ v e. V ) /\ n e. ( V \ { v } ) ) -> ( n e. ( G NeighbVtx v ) <-> E. e e. E { v , n } C_ e ) )
17	16	ralbidva	|- ( ( G e. W /\ v e. V ) -> ( A. n e. ( V \ { v } ) n e. ( G NeighbVtx v ) <-> A. n e. ( V \ { v } ) E. e e. E { v , n } C_ e ) )
18	17	ralbidva	|- ( G e. W -> ( A. v e. V A. n e. ( V \ { v } ) n e. ( G NeighbVtx v ) <-> A. v e. V A. n e. ( V \ { v } ) E. e e. E { v , n } C_ e ) )
19	3 18	bitrd	|- ( G e. W -> ( G e. ComplGraph <-> A. v e. V A. n e. ( V \ { v } ) E. e e. E { v , n } C_ e ) )