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	Could not format assertion : No typesetting found for |- ( .o. e. ( assIntOp ` M ) -> .o. clLaw M ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		elfvex	Could not format ( .o. e. ( assIntOp ` M ) -> M e. _V ) : No typesetting found for |- ( .o. e. ( assIntOp ` M ) -> M e. _V ) with typecode |-
2		assintopval	$$⊢M\in \mathrm{V}\to \mathrm{assIntOp}\left(M\right)=\left\{o\in \mathrm{clIntOp}\left(M\right)|o\mathrm{assLaw}M\right\}$$
3	2	eleq2d	Could not format ( M e. _V -> ( .o. e. ( assIntOp ` M ) <-> .o. e. { o e. ( clIntOp ` M ) | o assLaw M } ) ) : No typesetting found for |- ( M e. _V -> ( .o. e. ( assIntOp ` M ) <-> .o. e. { o e. ( clIntOp ` M ) | o assLaw M } ) ) with typecode |-
4		breq1	Could not format ( o = .o. -> ( o assLaw M <-> .o. assLaw M ) ) : No typesetting found for |- ( o = .o. -> ( o assLaw M <-> .o. assLaw M ) ) with typecode |-
5	4	elrab	Could not format ( .o. e. { o e. ( clIntOp ` M ) | o assLaw M } <-> ( .o. e. ( clIntOp ` M ) /\ .o. assLaw M ) ) : No typesetting found for |- ( .o. e. { o e. ( clIntOp ` M ) | o assLaw M } <-> ( .o. e. ( clIntOp ` M ) /\ .o. assLaw M ) ) with typecode |-
6	3 5	bitrdi	Could not format ( M e. _V -> ( .o. e. ( assIntOp ` M ) <-> ( .o. e. ( clIntOp ` M ) /\ .o. assLaw M ) ) ) : No typesetting found for |- ( M e. _V -> ( .o. e. ( assIntOp ` M ) <-> ( .o. e. ( clIntOp ` M ) /\ .o. assLaw M ) ) ) with typecode |-
7		clintopcllaw	Could not format ( .o. e. ( clIntOp ` M ) -> .o. clLaw M ) : No typesetting found for |- ( .o. e. ( clIntOp ` M ) -> .o. clLaw M ) with typecode |-
8	7	adantr	Could not format ( ( .o. e. ( clIntOp ` M ) /\ .o. assLaw M ) -> .o. clLaw M ) : No typesetting found for |- ( ( .o. e. ( clIntOp ` M ) /\ .o. assLaw M ) -> .o. clLaw M ) with typecode |-
9	6 8	biimtrdi	Could not format ( M e. _V -> ( .o. e. ( assIntOp ` M ) -> .o. clLaw M ) ) : No typesetting found for |- ( M e. _V -> ( .o. e. ( assIntOp ` M ) -> .o. clLaw M ) ) with typecode |-
10	1 9	mpcom	Could not format ( .o. e. ( assIntOp ` M ) -> .o. clLaw M ) : No typesetting found for |- ( .o. e. ( assIntOp ` M ) -> .o. clLaw M ) with typecode |-