Metamath Proof Explorer

Theorem iscplgr

Description: The property of being a complete graph. (Contributed by AV, 1-Nov-2020)

Ref Expression
Hypothesis cplgruvtxb.v ⊢ V = Vtx ⁡ G
Assertion iscplgr ⊢ G ∈ W → G ∈ ComplGraph ↔ ∀ v ∈ V v ∈ UnivVtx ⁡ G

Proof

Step Hyp Ref Expression
1 cplgruvtxb.v ⊢ V = Vtx ⁡ G
2 1 cplgruvtxb ⊢ G ∈ W → G ∈ ComplGraph ↔ UnivVtx ⁡ G = V
3 eqss ⊢ UnivVtx ⁡ G = V ↔ UnivVtx ⁡ G ⊆ V ∧ V ⊆ UnivVtx ⁡ G
4 1 uvtxssvtx ⊢ UnivVtx ⁡ G ⊆ V
5 dfss3 ⊢ V ⊆ UnivVtx ⁡ G ↔ ∀ v ∈ V v ∈ UnivVtx ⁡ G
6 5 anbi2i ⊢ UnivVtx ⁡ G ⊆ V ∧ V ⊆ UnivVtx ⁡ G ↔ UnivVtx ⁡ G ⊆ V ∧ ∀ v ∈ V v ∈ UnivVtx ⁡ G
7 4 6 mpbiran ⊢ UnivVtx ⁡ G ⊆ V ∧ V ⊆ UnivVtx ⁡ G ↔ ∀ v ∈ V v ∈ UnivVtx ⁡ G
8 3 7 bitri ⊢ UnivVtx ⁡ G = V ↔ ∀ v ∈ V v ∈ UnivVtx ⁡ G
9 2 8 bitrdi ⊢ G ∈ W → G ∈ ComplGraph ↔ ∀ v ∈ V v ∈ UnivVtx ⁡ G