This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )