Theorem iscplgr

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

	Ref	Expression
Hypothesis	cplgruvtxb.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion	iscplgr	⊢ ( 𝐺 ∈ 𝑊 → ( 𝐺 ∈ ComplGraph ↔ ∀ 𝑣 ∈ 𝑉 𝑣 ∈ ( UnivVtx ‘ 𝐺 ) ) )

Proof

Step	Hyp	Ref	Expression
1		cplgruvtxb.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2	1	cplgruvtxb	⊢ ( 𝐺 ∈ 𝑊 → ( 𝐺 ∈ ComplGraph ↔ ( UnivVtx ‘ 𝐺 ) = 𝑉 ) )
3		eqss	⊢ ( ( UnivVtx ‘ 𝐺 ) = 𝑉 ↔ ( ( UnivVtx ‘ 𝐺 ) ⊆ 𝑉 ∧ 𝑉 ⊆ ( UnivVtx ‘ 𝐺 ) ) )
4	1	uvtxssvtx	⊢ ( UnivVtx ‘ 𝐺 ) ⊆ 𝑉
5		dfss3	⊢ ( 𝑉 ⊆ ( UnivVtx ‘ 𝐺 ) ↔ ∀ 𝑣 ∈ 𝑉 𝑣 ∈ ( UnivVtx ‘ 𝐺 ) )
6	5	anbi2i	⊢ ( ( ( UnivVtx ‘ 𝐺 ) ⊆ 𝑉 ∧ 𝑉 ⊆ ( UnivVtx ‘ 𝐺 ) ) ↔ ( ( UnivVtx ‘ 𝐺 ) ⊆ 𝑉 ∧ ∀ 𝑣 ∈ 𝑉 𝑣 ∈ ( UnivVtx ‘ 𝐺 ) ) )
7	4 6	mpbiran	⊢ ( ( ( UnivVtx ‘ 𝐺 ) ⊆ 𝑉 ∧ 𝑉 ⊆ ( UnivVtx ‘ 𝐺 ) ) ↔ ∀ 𝑣 ∈ 𝑉 𝑣 ∈ ( UnivVtx ‘ 𝐺 ) )
8	3 7	bitri	⊢ ( ( UnivVtx ‘ 𝐺 ) = 𝑉 ↔ ∀ 𝑣 ∈ 𝑉 𝑣 ∈ ( UnivVtx ‘ 𝐺 ) )
9	2 8	bitrdi	⊢ ( 𝐺 ∈ 𝑊 → ( 𝐺 ∈ ComplGraph ↔ ∀ 𝑣 ∈ 𝑉 𝑣 ∈ ( UnivVtx ‘ 𝐺 ) ) )