Theorem clcllaw

Description: Closure of a closed operation. (Contributed by FL, 14-Sep-2010) (Revised by AV, 21-Jan-2020)

	Ref	Expression
Assertion	clcllaw	⊢ ( ( ⚬ clLaw 𝑀 ∧ 𝑋 ∈ 𝑀 ∧ 𝑌 ∈ 𝑀 ) → ( 𝑋 ⚬ 𝑌 ) ∈ 𝑀 )

Proof

Step	Hyp	Ref	Expression
1		df-cllaw	⊢ clLaw = { ⟨ 𝑜 , 𝑚 ⟩ ∣ ∀ 𝑥 ∈ 𝑚 ∀ 𝑦 ∈ 𝑚 ( 𝑥 𝑜 𝑦 ) ∈ 𝑚 }
2	1	bropaex12	⊢ ( ⚬ clLaw 𝑀 → ( ⚬ ∈ V ∧ 𝑀 ∈ V ) )
3		iscllaw	⊢ ( ( ⚬ ∈ V ∧ 𝑀 ∈ V ) → ( ⚬ clLaw 𝑀 ↔ ∀ 𝑥 ∈ 𝑀 ∀ 𝑦 ∈ 𝑀 ( 𝑥 ⚬ 𝑦 ) ∈ 𝑀 ) )
4		ovrspc2v	⊢ ( ( ( 𝑋 ∈ 𝑀 ∧ 𝑌 ∈ 𝑀 ) ∧ ∀ 𝑥 ∈ 𝑀 ∀ 𝑦 ∈ 𝑀 ( 𝑥 ⚬ 𝑦 ) ∈ 𝑀 ) → ( 𝑋 ⚬ 𝑌 ) ∈ 𝑀 )
5	4	expcom	⊢ ( ∀ 𝑥 ∈ 𝑀 ∀ 𝑦 ∈ 𝑀 ( 𝑥 ⚬ 𝑦 ) ∈ 𝑀 → ( ( 𝑋 ∈ 𝑀 ∧ 𝑌 ∈ 𝑀 ) → ( 𝑋 ⚬ 𝑌 ) ∈ 𝑀 ) )
6	3 5	biimtrdi	⊢ ( ( ⚬ ∈ V ∧ 𝑀 ∈ V ) → ( ⚬ clLaw 𝑀 → ( ( 𝑋 ∈ 𝑀 ∧ 𝑌 ∈ 𝑀 ) → ( 𝑋 ⚬ 𝑌 ) ∈ 𝑀 ) ) )
7	2 6	mpcom	⊢ ( ⚬ clLaw 𝑀 → ( ( 𝑋 ∈ 𝑀 ∧ 𝑌 ∈ 𝑀 ) → ( 𝑋 ⚬ 𝑌 ) ∈ 𝑀 ) )
8	7	3impib	⊢ ( ( ⚬ clLaw 𝑀 ∧ 𝑋 ∈ 𝑀 ∧ 𝑌 ∈ 𝑀 ) → ( 𝑋 ⚬ 𝑌 ) ∈ 𝑀 )