Metamath Proof Explorer

Theorem vdiscusgrb

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

Ref Expression
Hypothesis hashnbusgrvd.v ⊢ V = Vtx ⁡ G
Assertion vdiscusgrb ⊢ G ∈ FinUSGraph → G ∈ ComplUSGraph ↔ ∀ v ∈ V VtxDeg ⁡ G ⁡ v = V − 1

Proof

Step Hyp Ref Expression
1 hashnbusgrvd.v ⊢ V = Vtx ⁡ G
2 fusgrusgr ⊢ G ∈ FinUSGraph → G ∈ USGraph
3 1 cusgruvtxb ⊢ G ∈ USGraph → G ∈ ComplUSGraph ↔ UnivVtx ⁡ G = V
4 1 uvtxssvtx ⊢ UnivVtx ⁡ G ⊆ V
5 eqcom ⊢ UnivVtx ⁡ G = V ↔ V = UnivVtx ⁡ G
6 sssseq ⊢ UnivVtx ⁡ G ⊆ V → V ⊆ UnivVtx ⁡ G ↔ V = UnivVtx ⁡ G
7 5 6 bitr4id ⊢ UnivVtx ⁡ G ⊆ V → UnivVtx ⁡ G = V ↔ V ⊆ UnivVtx ⁡ G
8 4 7 mp1i ⊢ G ∈ USGraph → UnivVtx ⁡ G = V ↔ V ⊆ UnivVtx ⁡ G
9 3 8 bitrd ⊢ G ∈ USGraph → G ∈ ComplUSGraph ↔ V ⊆ UnivVtx ⁡ G
10 dfss3 ⊢ V ⊆ UnivVtx ⁡ G ↔ ∀ v ∈ V v ∈ UnivVtx ⁡ G
11 9 10 bitrdi ⊢ G ∈ USGraph → G ∈ ComplUSGraph ↔ ∀ v ∈ V v ∈ UnivVtx ⁡ G
12 2 11 syl ⊢ G ∈ FinUSGraph → G ∈ ComplUSGraph ↔ ∀ v ∈ V v ∈ UnivVtx ⁡ G
13 1 usgruvtxvdb ⊢ G ∈ FinUSGraph ∧ v ∈ V → v ∈ UnivVtx ⁡ G ↔ VtxDeg ⁡ G ⁡ v = V − 1
14 13 ralbidva ⊢ G ∈ FinUSGraph → ∀ v ∈ V v ∈ UnivVtx ⁡ G ↔ ∀ v ∈ V VtxDeg ⁡ G ⁡ v = V − 1
15 12 14 bitrd ⊢ G ∈ FinUSGraph → G ∈ ComplUSGraph ↔ ∀ v ∈ V VtxDeg ⁡ G ⁡ v = V − 1