I had a closer look at the theorems in sections "Miscellanea" and
"Functions" in Glauco`s Mathbox, and I think the following could be quite
useful and should be moved to the main part as soon as possible:
- "Miscellanea":
- neqned: ( ph -> -. A = B ) => ( ph -> A =/= B )
- iffalsed: ( ph -> -. ch ) => iffalsed $p |- ( ph -> if ( ch , A , B
) = B )
- iftrued:( ph -> ch ) =>( ph -> if ( ch , A , B ) = A )
- ifeq123d.: (ph -> ( ps <-> ch ) ) & ( ph -> A = B ) & ( ph -> C = D
) => ( ph -> if ( ps , A , C ) = if ( ch , B , D ) )
- rspan: ( ( A. x e. A ph /\ x e. A ) -> ph ) (maybe to be renamed!)
- "Functions":
- feq1dd: ( ph -> F = G ) &( ph -> F : A --> B ) => ( ph -> G : A
--> B ) (rename feq1d -> feq1bid; feq1dd -> feq1d)
- fssresd: ( ph -> F : A --> B ) & ( ph -> C C_ A ) => ( ph -> ( F |`
C ) : C --> B )
- fssd: ( ph -> F : A --> B ) & ( ph -> B C_ C ) =>( ph -> F : A -->
C )
- resmptd: ( ph -> B C_ A ) => ( ph -> ( ( x e. A |-> C ) |` B ) = (
x e. B |-> C ) )
- dmmptid: A = ( x e. B |-> C ) & ( ( ph /\ x e. B ) -> C e. V ) => (
ph -> dom A = B )
- resabs1d: ( ph -> B C_ C ) => ( ph -> ( ( A |` C ) |` B ) = ( A |`
B ) )
I have chosen these theorems especially because they are variants of
existing theorems, but in deduction form, so they support the "deduction
style" of set.mm. For the theorems in section "Miscellanea", I also took
the number of usages into account, see attachment.
If nobody objects, I can move these theorems before christmas :-).
On Monday, December 16, 2019 at 6:53:24 AM UTC+1, Alexander van der Vekens
wrote:
>
> Congratulations also from my side for proving another "Metamath 100"
> theorem!
>
> I also had a look at the "general theorems". I agree that a lot of them
> could be moved to the main part. As David (and also others) mentioned, this
> should be done in a structured way. At the moment, these theorems are all
> mixed up in section "Miscellanea", so maybe the first step would be to
> structure this section (using appropriate subsections, corresponding to the
> (sub)sections of the main part).
>
> As far as my latest "Metamath 100" theorem is concerned, I plan to move it
> (and all theorems which are used by its proof) to the main part, too. See
> issue #1314 at GitHub.
>
> Alexander
>
> On Monday, December 16, 2019 at 1:32:53 AM UTC+1, David A. Wheeler wrote:
>>
>> On Sun, 15 Dec 2019 13:02:33 -0800 (PST), Benoit <[email protected]>
>> wrote:
>> > Like FL, I think several lemmas deserve to be in the main part.
>>
>> I believe that all "Metamath 100" results (and thus all they depend on)
>> should eventually move into the main body. After all, all Metamath 100
>> results are
>> results that at least some others believe are important.
>>
>> We don't have to do that *instantly* of course.
>> In many cases I expect there will be discussion as the dependencies
>> are examined, possibly generalized, and then moved into the main body
>> in groups over time.
>>
>> I think it's important to keep working on getting more things moved from
>> mathboxes
>> into the main body. Tools like mmj2 only consider items in the main body
>> for
>> many automated steps, and in any case I think it's far more sensible to
>> readers if major results are properly organized in the main body.
>>
>> --- David A. Wheeler
>
>
--
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/777c207d-a1f2-4cb5-b0fb-f459f6bb7e10%40googlegroups.com.
Glauco's Mathbox - "Miscellanea":
adantlllr.1 $e |- ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ta ) $.
(3) adantlllr $p |- ( ( ( ( ( ph /\ et ) /\ ps ) /\ ch ) /\ th ) -> ta ) $=
3adantlr3.1 $e |- ( ( ( ph /\ ( ps /\ ch ) ) /\ th ) -> ta ) $.
(1) 3adantlr3 $p |- ( ( ( ph /\ ( ps /\ ch /\ et ) ) /\ th ) -> ta ) $=
3adantll2.1 $e |- ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ta ) $.
(1) 3adantll2 $p |- ( ( ( ( ph /\ et /\ ps ) /\ ch ) /\ th ) -> ta ) $=
3adantll3.1 $e |- ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ta ) $.
(2) 3adantll3 $p |- ( ( ( ( ph /\ ps /\ et ) /\ ch ) /\ th ) -> ta ) $=
adant423.1 $e |- ( ( ph /\ ps ) -> ch ) $.
(6) adant423 $p |- ( ( ( ( ph /\ th ) /\ ta ) /\ ps ) -> ch ) $=
simplrd.1 $e |- ( ph -> ( ( ps /\ ch ) /\ th ) ) $.
(5) simplrd $p |- ( ph -> ch ) $=
simprld.1 $e |- ( ph -> ( ps /\ ( ch /\ th ) ) ) $.
(4) simprld $p |- ( ph -> ch ) $=
simplld.1 $e |- ( ph -> ( ( ps /\ ch ) /\ th ) ) $.
(4) simplld $p |- ( ph -> ps ) $=
simprrd.1 $e |- ( ph -> ( ps /\ ( ch /\ th ) ) ) $.
(5) simprrd $p |- ( ph -> th ) $=
(-) 3expc.1 $e |- ( ( ( ph /\ ps ) /\ ch ) -> th ) $.
3expc $p |- ( ph -> ( ps -> ( ch -> th ) ) ) $=
jcn.1 $e |- ( ph -> ps ) $.
jcn.2 $e |- ( ph -> -. ch ) $.
(-) jcn $p |- ( ph -> -. ( ps -> ch ) ) $=
----
(2) elabrexg $p |- ( ( x e. A /\ B e. V ) -> B e. { y | E. x e. A y = B } ) $=
(1) rexnal2 $p |- ( E. x e. A E. y e. B -. ph <-> -. A. x e. A A. y e. B ph )
$=
(1) ralnex2 $p |- ( A. x e. A A. y e. B -. ph <-> -. E. x e. A E. y e. B ph )
$=
*(27) rspan $p |- ( ( A. x e. A ph /\ x e. A ) -> ph ) $=
rename: rspa (like ~ rspcva)
----
neqned.1 $e |- ( ph -> -. A = B ) $.
*(39) neqned $p |- ( ph -> A =/= B ) $=
(6) neneq $p |- ( A =/= B -> -. A = B ) $=
(34) neqne $p |- ( -. A = B -> A =/= B ) $=
ne0ii.1 $e |- A e. B $.
(3) ne0ii $p |- B =/= (/) $=
----
iffalsed.1 $e |- ( ph -> -. ch ) $.
* (17) iffalsed $p |- ( ph -> if ( ch , A , B ) = B ) $=
iftrued.1 $e |- ( ph -> ch ) $.
* (12) iftrued $p |- ( ph -> if ( ch , A , B ) = A ) $=
ifeq123d.1 $e |- ( ph -> ( ps <-> ch ) ) $.
ifeq123d.2 $e |- ( ph -> A = B ) $.
ifeq123d.3 $e |- ( ph -> C = D ) $.
* (23) ifeq123d $p |- ( ph -> if ( ps , A , C ) = if ( ch , B , D ) ) $=
----
(2) elunnel1 $p |- ( ( A e. ( B u. C ) /\ -. A e. B ) -> A e. C ) $=
(4) elunnel2 $p |- ( ( A e. ( B u. C ) /\ -. A e. C ) -> A e. B ) $=
(1) ssnel $p |- ( ( A C_ B /\ -. C e. B ) -> -. C e. A ) $=
(6) elinel2 $p |- ( A e. ( B i^i C ) -> A e. C ) $=
(6) elinel1 $p |- ( A e. ( B i^i C ) -> A e. B ) $=
----
(1) sncldre $p |- ( A e. RR -> { A } e. ( Clsd ` ( topGen ` ran (,) ) ) ) $=
nnxrd.1 $e |- ( ph -> A e. NN ) $.
(1) nnxrd $p |- ( ph -> A e. RR* ) $=
(12) unicntop $p |- CC = U. ( TopOpen ` CCfld ) $=
(1) cnopn $p |- CC e. ( TopOpen ` CCfld ) $=
