Description: A graph G is complete iff each vertex is a universal vertex. (Contributed by Alexander van der Vekens, 14-Oct-2017) (Revised by AV, 15-Feb-2022)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | cplgruvtxb.v | ⊢ 𝑉 = ( Vtx ‘ 𝐺 ) | |
| Assertion | cplgruvtxb | ⊢ ( 𝐺 ∈ 𝑊 → ( 𝐺 ∈ ComplGraph ↔ ( UnivVtx ‘ 𝐺 ) = 𝑉 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cplgruvtxb.v | ⊢ 𝑉 = ( Vtx ‘ 𝐺 ) | |
| 2 | fveq2 | ⊢ ( 𝑔 = 𝐺 → ( UnivVtx ‘ 𝑔 ) = ( UnivVtx ‘ 𝐺 ) ) | |
| 3 | fveq2 | ⊢ ( 𝑔 = 𝐺 → ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) ) | |
| 4 | 3 1 | eqtr4di | ⊢ ( 𝑔 = 𝐺 → ( Vtx ‘ 𝑔 ) = 𝑉 ) |
| 5 | 2 4 | eqeq12d | ⊢ ( 𝑔 = 𝐺 → ( ( UnivVtx ‘ 𝑔 ) = ( Vtx ‘ 𝑔 ) ↔ ( UnivVtx ‘ 𝐺 ) = 𝑉 ) ) |
| 6 | df-cplgr | ⊢ ComplGraph = { 𝑔 ∣ ( UnivVtx ‘ 𝑔 ) = ( Vtx ‘ 𝑔 ) } | |
| 7 | 5 6 | elab2g | ⊢ ( 𝐺 ∈ 𝑊 → ( 𝐺 ∈ ComplGraph ↔ ( UnivVtx ‘ 𝐺 ) = 𝑉 ) ) |