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

Metamath Proof Explorer

Theorem vdiscusgr

Description: In a finite complete simple graph with n vertices every vertex has degree n - 1 . (Contributed by Alexander van der Vekens, 14-Jul-2018) (Revised by AV, 17-Dec-2020)

Ref Expression
Hypothesis hashnbusgrvd.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion vdiscusgr ( 𝐺 ∈ FinUSGraph → ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ♯ ‘ 𝑉 ) − 1 ) → 𝐺 ∈ ComplUSGraph ) )

Proof

Step Hyp Ref Expression
1 hashnbusgrvd.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 1 uvtxisvtx ⊢ ( 𝑛 ∈ ( UnivVtx ‘ 𝐺 ) → 𝑛 ∈ 𝑉 )
3 fveqeq2 ⊢ ( 𝑣 = 𝑛 → ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ↔ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑛 ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ) )
4 3 rspccv ⊢ ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ♯ ‘ 𝑉 ) − 1 ) → ( 𝑛 ∈ 𝑉 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑛 ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ) )
5 4 adantl ⊢ ( ( 𝐺 ∈ FinUSGraph ∧ ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ) → ( 𝑛 ∈ 𝑉 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑛 ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ) )
6 5 imp ⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ) ∧ 𝑛 ∈ 𝑉 ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑛 ) = ( ( ♯ ‘ 𝑉 ) − 1 ) )
7 1 usgruvtxvdb ⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑛 ∈ 𝑉 ) → ( 𝑛 ∈ ( UnivVtx ‘ 𝐺 ) ↔ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑛 ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ) )
8 7 adantlr ⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ) ∧ 𝑛 ∈ 𝑉 ) → ( 𝑛 ∈ ( UnivVtx ‘ 𝐺 ) ↔ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑛 ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ) )
9 6 8 mpbird ⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ) ∧ 𝑛 ∈ 𝑉 ) → 𝑛 ∈ ( UnivVtx ‘ 𝐺 ) )
10 9 ex ⊢ ( ( 𝐺 ∈ FinUSGraph ∧ ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ) → ( 𝑛 ∈ 𝑉 → 𝑛 ∈ ( UnivVtx ‘ 𝐺 ) ) )
11 2 10 impbid2 ⊢ ( ( 𝐺 ∈ FinUSGraph ∧ ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ) → ( 𝑛 ∈ ( UnivVtx ‘ 𝐺 ) ↔ 𝑛 ∈ 𝑉 ) )
12 11 eqrdv ⊢ ( ( 𝐺 ∈ FinUSGraph ∧ ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ) → ( UnivVtx ‘ 𝐺 ) = 𝑉 )
13 fusgrusgr ⊢ ( 𝐺 ∈ FinUSGraph → 𝐺 ∈ USGraph )
14 1 cusgruvtxb ⊢ ( 𝐺 ∈ USGraph → ( 𝐺 ∈ ComplUSGraph ↔ ( UnivVtx ‘ 𝐺 ) = 𝑉 ) )
15 13 14 syl ⊢ ( 𝐺 ∈ FinUSGraph → ( 𝐺 ∈ ComplUSGraph ↔ ( UnivVtx ‘ 𝐺 ) = 𝑉 ) )
16 15 adantr ⊢ ( ( 𝐺 ∈ FinUSGraph ∧ ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ) → ( 𝐺 ∈ ComplUSGraph ↔ ( UnivVtx ‘ 𝐺 ) = 𝑉 ) )
17 12 16 mpbird ⊢ ( ( 𝐺 ∈ FinUSGraph ∧ ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ) → 𝐺 ∈ ComplUSGraph )
18 17 ex ⊢ ( 𝐺 ∈ FinUSGraph → ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ♯ ‘ 𝑉 ) − 1 ) → 𝐺 ∈ ComplUSGraph ) )