Theorem assintopcllaw

Description: The closure low holds for an associative (closed internal binary) operation for a set. (Contributed by FL, 2-Nov-2009) (Revised by AV, 20-Jan-2020)

	Ref	Expression
Assertion	assintopcllaw	|- ( .o. e. ( assIntOp ` M ) -> .o. clLaw M )

Proof

Step	Hyp	Ref	Expression
1		elfvex	|- ( .o. e. ( assIntOp ` M ) -> M e. _V )
2		assintopval	|- ( M e. _V -> ( assIntOp ` M ) = { o e. ( clIntOp ` M ) | o assLaw M } )
3	2	eleq2d	|- ( M e. _V -> ( .o. e. ( assIntOp ` M ) <-> .o. e. { o e. ( clIntOp ` M ) | o assLaw M } ) )
4		breq1	|- ( o = .o. -> ( o assLaw M <-> .o. assLaw M ) )
5	4	elrab	|- ( .o. e. { o e. ( clIntOp ` M ) | o assLaw M } <-> ( .o. e. ( clIntOp ` M ) /\ .o. assLaw M ) )
6	3 5	bitrdi	|- ( M e. _V -> ( .o. e. ( assIntOp ` M ) <-> ( .o. e. ( clIntOp ` M ) /\ .o. assLaw M ) ) )
7		clintopcllaw	|- ( .o. e. ( clIntOp ` M ) -> .o. clLaw M )
8	7	adantr	|- ( ( .o. e. ( clIntOp ` M ) /\ .o. assLaw M ) -> .o. clLaw M )
9	6 8	biimtrdi	|- ( M e. _V -> ( .o. e. ( assIntOp ` M ) -> .o. clLaw M ) )
10	1 9	mpcom	|- ( .o. e. ( assIntOp ` M ) -> .o. clLaw M )