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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	iscplgredg.v	⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion	iscplgredg	⊢ ( 𝐺 ∈ 𝑊 → ( 𝐺 ∈ ComplGraph ↔ ∀ 𝑣 ∈ 𝑉 ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) ∃ 𝑒 ∈ 𝐸 { 𝑣 , 𝑛 } ⊆ 𝑒 ) )

Proof

Step	Hyp	Ref	Expression
1		cplgruvtxb.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		iscplgredg.v	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3	1	iscplgrnb	⊢ ( 𝐺 ∈ 𝑊 → ( 𝐺 ∈ ComplGraph ↔ ∀ 𝑣 ∈ 𝑉 ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ) )
4		df-3an	⊢ ( ( ( 𝑛 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉 ) ∧ 𝑛 ≠ 𝑣 ∧ ∃ 𝑒 ∈ 𝐸 { 𝑣 , 𝑛 } ⊆ 𝑒 ) ↔ ( ( ( 𝑛 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉 ) ∧ 𝑛 ≠ 𝑣 ) ∧ ∃ 𝑒 ∈ 𝐸 { 𝑣 , 𝑛 } ⊆ 𝑒 ) )
5	4	a1i	⊢ ( ( ( 𝐺 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉 ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) ) → ( ( ( 𝑛 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉 ) ∧ 𝑛 ≠ 𝑣 ∧ ∃ 𝑒 ∈ 𝐸 { 𝑣 , 𝑛 } ⊆ 𝑒 ) ↔ ( ( ( 𝑛 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉 ) ∧ 𝑛 ≠ 𝑣 ) ∧ ∃ 𝑒 ∈ 𝐸 { 𝑣 , 𝑛 } ⊆ 𝑒 ) ) )
6	1 2	nbgrel	⊢ ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ↔ ( ( 𝑛 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉 ) ∧ 𝑛 ≠ 𝑣 ∧ ∃ 𝑒 ∈ 𝐸 { 𝑣 , 𝑛 } ⊆ 𝑒 ) )
7	6	a1i	⊢ ( ( ( 𝐺 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉 ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) ) → ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ↔ ( ( 𝑛 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉 ) ∧ 𝑛 ≠ 𝑣 ∧ ∃ 𝑒 ∈ 𝐸 { 𝑣 , 𝑛 } ⊆ 𝑒 ) ) )
8		eldifsn	⊢ ( 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) ↔ ( 𝑛 ∈ 𝑉 ∧ 𝑛 ≠ 𝑣 ) )
9		simpr	⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉 ) → 𝑣 ∈ 𝑉 )
10		simpl	⊢ ( ( 𝑛 ∈ 𝑉 ∧ 𝑛 ≠ 𝑣 ) → 𝑛 ∈ 𝑉 )
11	9 10	anim12ci	⊢ ( ( ( 𝐺 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉 ) ∧ ( 𝑛 ∈ 𝑉 ∧ 𝑛 ≠ 𝑣 ) ) → ( 𝑛 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉 ) )
12		simprr	⊢ ( ( ( 𝐺 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉 ) ∧ ( 𝑛 ∈ 𝑉 ∧ 𝑛 ≠ 𝑣 ) ) → 𝑛 ≠ 𝑣 )
13	11 12	jca	⊢ ( ( ( 𝐺 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉 ) ∧ ( 𝑛 ∈ 𝑉 ∧ 𝑛 ≠ 𝑣 ) ) → ( ( 𝑛 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉 ) ∧ 𝑛 ≠ 𝑣 ) )
14	8 13	sylan2b	⊢ ( ( ( 𝐺 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉 ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) ) → ( ( 𝑛 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉 ) ∧ 𝑛 ≠ 𝑣 ) )
15	14	biantrurd	⊢ ( ( ( 𝐺 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉 ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) ) → ( ∃ 𝑒 ∈ 𝐸 { 𝑣 , 𝑛 } ⊆ 𝑒 ↔ ( ( ( 𝑛 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉 ) ∧ 𝑛 ≠ 𝑣 ) ∧ ∃ 𝑒 ∈ 𝐸 { 𝑣 , 𝑛 } ⊆ 𝑒 ) ) )
16	5 7 15	3bitr4d	⊢ ( ( ( 𝐺 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉 ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) ) → ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ↔ ∃ 𝑒 ∈ 𝐸 { 𝑣 , 𝑛 } ⊆ 𝑒 ) )
17	16	ralbidva	⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉 ) → ( ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ↔ ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) ∃ 𝑒 ∈ 𝐸 { 𝑣 , 𝑛 } ⊆ 𝑒 ) )
18	17	ralbidva	⊢ ( 𝐺 ∈ 𝑊 → ( ∀ 𝑣 ∈ 𝑉 ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ↔ ∀ 𝑣 ∈ 𝑉 ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) ∃ 𝑒 ∈ 𝐸 { 𝑣 , 𝑛 } ⊆ 𝑒 ) )
19	3 18	bitrd	⊢ ( 𝐺 ∈ 𝑊 → ( 𝐺 ∈ ComplGraph ↔ ∀ 𝑣 ∈ 𝑉 ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) ∃ 𝑒 ∈ 𝐸 { 𝑣 , 𝑛 } ⊆ 𝑒 ) )