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 ⊢ 𝑉 = ( 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 ↔ ∀ 𝑣 ∈ 𝑉 ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) ∃ 𝑒 ∈ 𝐸 { 𝑣 , 𝑛 } ⊆ 𝑒 ) )