search

metamath / set.mm

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

Avoid ax-12 in fveq1 and fveq2 #4022

Closed GinoGiotto closed 3 months ago

GinoGiotto commented 3 months ago

Revise proofs of fveq1 and fveq2 to reduce ax-12 usage. This happens to automatically remove ax-12 from the famous 2p2e4 as well.

All added DV conditions are with dummy variables.

This PR drops ax-12 from 189 theorems. Full axiom usage here: https://github.com/metamath/set.mm/commit/40b9626f767167ad29f6eb54e6cb839de811c8b7

GinoGiotto commented 3 months ago

Closed as per https://github.com/metamath/set.mm/pull/4022#discussion_r1617755156

wlammen commented 3 months ago

This is script for a Linux console that I use to locally fill a folder metamath/web with all theorems from a current set.mm:

cd /home/wolf/metamath/web rm -f cp /home/wolf/metamath/set.mm/set.mm . cp /home/wolf/metamath/bin/metamath . echo 'show statement /alt_html' > create echo 'submit create' > exec echo 'quit' >> exec ./metamath set.mm < exec

GinoGiotto commented 3 months ago

Interesting. I've never tried the /alt_html option. Only now I realise that it's the one that generates the pretty unicode symbols!