search

metamath / set.mm

Metamath source file for logic and set theory
Other
243 stars 88 forks source link

ax10-12 dfss2 elprg, structure deductions #3991

Closed icecream17 closed 3 months ago

icecream17 commented 3 months ago

elabg2w basically obsoletes elabgw in usage use elabg2w in elprg

dfss2 without ax10-12 elin had to be moved up to a not ideal location

this should cause a lot of downstream ax10-12 saves, though I didnt check

deductions for structures

from experience I think these should exist, though they're in my mathbox for now (see #3990)

tirix commented 3 months ago

I'm sure the "deductions for structures" theorems are used a lot and will lead to shortening that will "pay for themselves".