On Wed, Apr 19, 2023 at 1:49 PM LM <[email protected]> wrote:
> I am confused how to export proofs so I can include them in my sandbox.mm
> file (which includes $[ set.mm $] )
mmj2 loads your set.mm file: try to edit you local set.mm. When you
are ready with a proof in mmj2, you should format it similarly to what
you see in set.mm.
For example, this proof in mmj2
$( <MM> <PROOF_ASST> THEOREM=dfcnvasymrel4 LOC_AFTER=?
* Alternate definition of the converse asymmetric relation predicate.
(Contributed by Peter Mazsa, 25-Mar-2023.)
50::dfcnvasymrel2 |- ( CnvASymRel R <-> ( ( ( _V X. _V ) \ R ) C_ `'
R /\ Rel R ) )
51::relcnv |- Rel `' R
52::relvvdifss |- ( ( Rel R /\ Rel `' R ) -> ( ( ( _V X. _V ) \
R ) C_ `' R <-> ( R u. `' R ) = ( _V X. _V ) ) )
53:51,52:mpan2 |- ( Rel R -> ( ( ( _V X. _V ) \ R ) C_ `' R <->
( R u. `' R ) = ( _V X. _V ) ) )
54:53:pm5.32ri |- ( ( ( ( _V X. _V ) \ R ) C_ `' R /\ Rel R )
<-> ( ( R u. `' R ) = ( _V X. _V ) /\ Rel R ) )
qed:50,54:bitri |- ( CnvASymRel R <-> ( ( R u. `' R ) = ( _V X.
_V ) /\ Rel R ) )
$= ( wcnvasymrel cvv cxp cdif ccnv wss wrel wa wceq dfcnvasymrel2 wb
cun relcnv relvvdifss mpan2 pm5.32ri bitri ) ABCCDZAEAFZGZAHZIATM
SJZUBIAKUBUAUCUBTHUAUCLANATOPQR $.
$)
should be
$( Alternate definition of the converse asymmetric relation predicate.
(Contributed by Peter Mazsa, 25-Mar-2023.) $)
dfcnvasymrel4 $p |- ( CnvASymRel R <-> ( ( R u. `' R ) = ( _V X. _V
) /\ Rel R ) ) $=
( wcnvasymrel cvv cxp cdif ccnv wss wrel wa wceq dfcnvasymrel2 wb
cun relcnv relvvdifss mpan2 pm5.32ri bitri ) ABCCDZAEAFZGZAHZIATMSJ
ZUBIAKUBUAUCUBTHUAUCLANATOPQR $.
at the end of your local set.mm .
This must solve some of your problems.
P.
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/CAJJTU5rxOAuCVMU-fa%3D7_ResN8g7O-DSsh6W%2Bud9QeP%2BKJS_%2Bw%40mail.gmail.com.
