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 ⊢ V = Vtx ⁡ G
Assertion vdiscusgr ⊢ G ∈ FinUSGraph → ∀ v ∈ V VtxDeg ⁡ G ⁡ v = V − 1 → G ∈ ComplUSGraph

Proof

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