Theorem clcllaw

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

	Ref	Expression
Assertion	clcllaw	Could not format assertion : No typesetting found for |- ( ( .o. clLaw M /\ X e. M /\ Y e. M ) -> ( X .o. Y ) e. M ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		df-cllaw	$$⊢\mathrm{clLaw}=\left\{⟨o,m⟩|\forall x\in m\forall y\in mxoy\in m\right\}$$
2	1	bropaex12	Could not format ( .o. clLaw M -> ( .o. e. _V /\ M e. _V ) ) : No typesetting found for |- ( .o. clLaw M -> ( .o. e. _V /\ M e. _V ) ) with typecode |-
3		iscllaw	Could not format ( ( .o. e. _V /\ M e. _V ) -> ( .o. clLaw M <-> A. x e. M A. y e. M ( x .o. y ) e. M ) ) : No typesetting found for |- ( ( .o. e. _V /\ M e. _V ) -> ( .o. clLaw M <-> A. x e. M A. y e. M ( x .o. y ) e. M ) ) with typecode |-
4		ovrspc2v	Could not format ( ( ( X e. M /\ Y e. M ) /\ A. x e. M A. y e. M ( x .o. y ) e. M ) -> ( X .o. Y ) e. M ) : No typesetting found for |- ( ( ( X e. M /\ Y e. M ) /\ A. x e. M A. y e. M ( x .o. y ) e. M ) -> ( X .o. Y ) e. M ) with typecode |-
5	4	expcom	Could not format ( A. x e. M A. y e. M ( x .o. y ) e. M -> ( ( X e. M /\ Y e. M ) -> ( X .o. Y ) e. M ) ) : No typesetting found for |- ( A. x e. M A. y e. M ( x .o. y ) e. M -> ( ( X e. M /\ Y e. M ) -> ( X .o. Y ) e. M ) ) with typecode |-
6	3 5	biimtrdi	Could not format ( ( .o. e. _V /\ M e. _V ) -> ( .o. clLaw M -> ( ( X e. M /\ Y e. M ) -> ( X .o. Y ) e. M ) ) ) : No typesetting found for |- ( ( .o. e. _V /\ M e. _V ) -> ( .o. clLaw M -> ( ( X e. M /\ Y e. M ) -> ( X .o. Y ) e. M ) ) ) with typecode |-
7	2 6	mpcom	Could not format ( .o. clLaw M -> ( ( X e. M /\ Y e. M ) -> ( X .o. Y ) e. M ) ) : No typesetting found for |- ( .o. clLaw M -> ( ( X e. M /\ Y e. M ) -> ( X .o. Y ) e. M ) ) with typecode |-
8	7	3impib	Could not format ( ( .o. clLaw M /\ X e. M /\ Y e. M ) -> ( X .o. Y ) e. M ) : No typesetting found for |- ( ( .o. clLaw M /\ X e. M /\ Y e. M ) -> ( X .o. Y ) e. M ) with typecode |-