Theorem clintop

Description: A closed (internal binary) operation for a set. (Contributed by AV, 20-Jan-2020)

	Ref	Expression
Assertion	clintop	⊢ ( ⚬ ∈ ( clIntOp ‘ 𝑀 ) → ⚬ : ( 𝑀 × 𝑀 ) ⟶ 𝑀 )

Proof

Step	Hyp	Ref	Expression
1		elfvex	⊢ ( ⚬ ∈ ( clIntOp ‘ 𝑀 ) → 𝑀 ∈ V )
2		isclintop	⊢ ( 𝑀 ∈ V → ( ⚬ ∈ ( clIntOp ‘ 𝑀 ) ↔ ⚬ : ( 𝑀 × 𝑀 ) ⟶ 𝑀 ) )
3	2	biimpd	⊢ ( 𝑀 ∈ V → ( ⚬ ∈ ( clIntOp ‘ 𝑀 ) → ⚬ : ( 𝑀 × 𝑀 ) ⟶ 𝑀 ) )
4	1 3	mpcom	⊢ ( ⚬ ∈ ( clIntOp ‘ 𝑀 ) → ⚬ : ( 𝑀 × 𝑀 ) ⟶ 𝑀 )