Metamath Proof Explorer


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 syl6bi ( ( ∈ V ∧ 𝑀 ∈ V ) → ( clLaw 𝑀 → ( ( 𝑋𝑀𝑌𝑀 ) → ( 𝑋 𝑌 ) ∈ 𝑀 ) ) )
7 2 6 mpcom ( clLaw 𝑀 → ( ( 𝑋𝑀𝑌𝑀 ) → ( 𝑋 𝑌 ) ∈ 𝑀 ) )
8 7 3impib ( ( clLaw 𝑀𝑋𝑀𝑌𝑀 ) → ( 𝑋 𝑌 ) ∈ 𝑀 )