Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Prove tz7.48lem without ax-8 #3199

Closed
wants to merge 3 commits into from
Closed

Prove tz7.48lem without ax-8 #3199

Changes from 2 commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
b98720e
edited proof of tz7.48lem
GinoGiotto May 21, 2023
afa0c00
added credit
GinoGiotto May 21, 2023
494f7ac
removed 'revised by' comment
GinoGiotto Aug 12, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
47 changes: 24 additions & 23 deletions set.mm
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -75869,32 +75869,33 @@ currently used conventions for such cases (see ~ cbvmpt2x , ~ ovmpt2x and
${
$d x A $.
$( A way of showing an ordinal function is one-to-one. (Contributed by
NM, 9-Feb-1997.) $)
NM, 9-Feb-1997.) Avoid ~ ax-8 . (Revised by Gino Giotto,
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The way ax-8 is avoided is basically bj-ax8 so idk if this is an actual improvement

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can you tell where bj-ax8 is used? Metamath.exe doesn't show me:

Metamath - Version 0.198 7-Aug-2021           Type HELP for help, EXIT to exit.
MM> READ set.mm
Reading source file "set.mm"... 43199123 bytes
43199123 bytes were read into the source buffer.
The source has 205354 statements; 2738 are $a and 40892 are $p.
No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
if you want to check them.
MM> SHOW TRACE_BACK tz7.48lem /MATCH bj-ax8
The proof of statement "tz7.48lem" uses the following earlier statements:
  (None)
MM>

If true that would be odd since bj-ax8 is in a mathbox, and I didn't have /INCLUDE_MATHBOXES activated, so it would be a bug of the minimizer.

Also is it even possible to depend from a statement that appears after the main one? I'm new here, so there might be something that I'm missing.

Copy link
Contributor

@icecream17 icecream17 May 22, 2023 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I mean that eleq1w is more general than elequ1 but doesn't use ax-8, due to df-clel being "too powerful" in its current state
So the way ax-8 is "saved" here is equivalent to the way it is saved in bj-ax8.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That's interesting. If df-clel is too powerful, it seems dangerous to leave it like that, shouldn't it have a New usage is discouraged label on it?

However in this case df-clel was already used in fvres and ordtri3, so technically it wasn't introduced as a new dependency for tz7.48lem. The final outcome is still a clear loss.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I originally approved but I did not have @icecream17's sharp eye about axiom dependency!
I think this is pending @icecream17's answer and so I will continue to hold merging for now.

For reference, there were mailing list exchanges between Norm and @benjub about ax-8. I think ultimately, Norm preferred to keep the actual axioms as near to the literature as possible, and so Benoît's suggestions were kept in his mathbox.

@avekens @jkingdon @digama0 don't hesitate to step in if you have an opinion!

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It would be nice if we could have a bit more settled situation with respect to https://us.metamath.org/mpeuni/df-clel.html and https://us.metamath.org/mpeuni/df-cleq.html.

I was under the impression that the mailing group discussion settled the point: Norm said he preferred to keep the current axioms, and have the alternative solution in a mathbox, @benjub agreed to do so, and that's the situation we have until now.

Did I understand that correctly? I'm also not diving much into these discussions.

We could reopen that discussion, though.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

A problem with changing the definition now is that currently cleljust2 would add ax-10 ax-12 ax-13 which obscures their actual usages. These axioms would be removed by the new definition of substitution df-ssb.

So if wanting to introduce ax-8 to df-clel, then the choices are either wait until df-ssb is merged or add ax-8 to df-clel in some arbitrary fashion (like with dfcleq and ax-9)

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

In case someone isn't following the recent additions in the metamath-knife repo, a discussion about df-clel df-clab df-cleq was brought up in this PR which adds a definition checker.

Copy link
Contributor

@icecream17 icecream17 Jun 19, 2023 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Perhaps one could introduce dfclel which arbitrarily introduces ax-8. This would be a quick solution. I say this now because based on #3250 + #3262 it seems this would unintuitively affect $j statements.

Edit: Wait, elequ2 doesn't use ax-8. nvm

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The ideal of "arbitrarily" introducing ax-8 is, I guess, similar to what we did with ax-9 in https://us.metamath.org/mpeuni/dfcleq.html . But I suppose that sort of thing sidesteps the question of what
the real status (axiom or definition) of df-clel df-clab and df-cleq is.

22-May-2023.) $)
tz7.48lem $p |- ( ( A C_ On /\ A. x e. A A. y e. x
-. ( F ` x ) = ( F ` y ) ) -> Fun `' ( F |` A ) ) $=
( vw vz con0 cv cfv wceq wn wral wa weq wi wel wcel wal r2al cres simpl
ccnv wfun anim1i imim1i 2alimi sylbi sylibr elequ1 fveq2 eqeq2d imbi12d
notbid cbvralv ralbii elequ2 fveqeq2 ralbidv bitri 3bitri ralcom2 ancri
wss expd r19.26-2 syl wb fvres eqeqan12d ad2antrl ssel anim12d wo oridm
pm3.48 eqcom notbii orbi1i bitr3i syl6ibr con2d word eloni syl2an syl9r
ordtri3 biimprd syl6 imp32 exp32 a2d 2alimdv 3imtr4g syl5 imdistani wfn
sylbid fnssres mpan cvv wf dffn2 wf1 dff13 df-f1 simprbi sylanb sylan )
CHVDZAIZDJZBIZDJZKZLZBXKMACMZNXJXKDCUAZJZXMXRJZKZABOZPZBCMACMZNXRUCUDZX
JXQYDXQABQZXNXLKZLZPZBAQZXPPZNZBCMACMZXJYDXQYKBCMZACMZYMXQXKCRZXMCRZNZY
KPZBSASZYOXQYPYJNZXPPZBSASYTXPABCXKTUUBYSABUUBYRYJXPYRYJNUUAXPYRYPYJYPY
QUBUEUFVEUGUHYKABCCTUIYOYIBCMACMZYONYMYOUUCYOYIACMZBCMZUUCYOFAQZXLFIZDJ
ZKZLZPZFCMZACMFGQZGIZDJZUUHKZLZPZFCMZGCMZUUEYNUULACYKUUKBFCBFOZYJUUFXPU
UJBFAUJUVAXOUUIUVAXNUUHXLXMUUGDUKULUNUMUOUPUULUUSAGCAGOZUUKUURFCUVBUUFU
UMUUJUUQAGFUQUVBUUIUUPXKUUNUUHDURUNUMUSUOUUTAGQZUUOXLKZLZPZACMZGCMUUEUU
SUVGGCUURUVFFACFAOZUUMUVCUUQUVEFAGUJUVHUUPUVDUVHUUHXLUUOUUGXKDUKULUNUMU
OUPUVGUUDGBCGBOZUVFYIACUVIUVCYFUVEYHGBAUQUVIUVDYGUUNXMXLDURUNUMUSUOUTVA
YIBACVBUHVCYIYKABCCVFUIVGXJYRYLPZBSASYRYCPZBSASYMYDXJUVJUVKABXJYRYLYCXJ
YRYLYCXJYRYLNNYAXOYBYRYAXOVHXJYLYPYQXSXLXTXNXKCDVIXMCDVIVJVKXJYRYLXOYBP
ZXJYRXKHRZXMHRZNZYLUVLPXJYPUVMYQUVNCHXKVLCHXMVLVMYLXOYFYJVNZLZUVOYBYLUV
PXOYLUVPYHXPVNZXPYFYHYJXPVPXPXPXPVNUVRXPVOXPYHXPXOYGXLXNVQVRVSVTWAWBUVM
XKWCZXMWCZUVQYBPUVNXKWDXMWDUVSUVTNYBUVQXKXMWGWHWEWFWIWJWRWKWLWMYLABCCTY
CABCCTWNWOWPXJXRCWQZYDYEDHWQXJUWAEHCDWSWTUWACXAXRXBZYDYECXRXCUWBYDNZUWB
YEUWCCXAXRXDUWBYENABCXAXRXECXAXRXFVTXGXHXIVG $.
ccnv wfun anim1i imim1i expd 2alimi 3imtr4i eleq1w fveq2 eqeq2d imbi12d
notbid cbvralv ralbii elequ2 fveqeq2 ralbidv bitri 3bitri ralcom2 sylbi
wss ancri r19.26-2 sylibr syl wb eqeqan12d ad2antrl ssel anim12d pm3.48
fvres oridm eqcom notbii orbi1i bitr3i syl6ibr con2d word eloni ordtri3
wo biimprd syl2an syl9r syl6 imp32 sylbid a2d 2alimdv 3imtr4g imdistani
exp32 syl5 wfn fnssres mpan cvv wf dffn2 wf1 dff13 df-f1 simprbi sylanb
sylan ) CHVDZAIZDJZBIZDJZKZLZBXLMACMZNXKXLDCUAZJZXNXSJZKZABOZPZBCMACMZN
XSUCUDZXKXRYEXRABQZXOXMKZLZPZBAQZXQPZNZBCMACMZXKYEXRYLBCMZACMZYNXLCRZYK
NZXQPZBSASYQXNCRZNZYLPZBSASXRYPYSUUBABYSUUAYKXQUUAYKNYRXQUUAYQYKYQYTUBU
EUFUGUHXQABCXLTYLABCCTUIYPYJBCMACMZYPNYNYPUUCYPYJACMZBCMZUUCYPFAQZXMFIZ
DJZKZLZPZFCMZACMFGQZGIZDJZUUHKZLZPZFCMZGCMZUUEYOUULACYLUUKBFCBFOZYKUUFX
QUUJBFXLUJUVAXPUUIUVAXOUUHXMXNUUGDUKULUNUMUOUPUULUUSAGCAGOZUUKUURFCUVBU
UFUUMUUJUUQAGFUQUVBUUIUUPXLUUNUUHDURUNUMUSUOUUTAGQZUUOXMKZLZPZACMZGCMUU
EUUSUVGGCUURUVFFACFAOZUUMUVCUUQUVEFAUUNUJUVHUUPUVDUVHUUHXMUUOUUGXLDUKUL
UNUMUOUPUVGUUDGBCGBOZUVFYJACUVIUVCYGUVEYIGBAUQUVIUVDYHUUNXNXMDURUNUMUSU
OUTVAYJBACVBVCVEYJYLABCCVFVGVHXKUUAYMPZBSASUUAYDPZBSASYNYEXKUVJUVKABXKU
UAYMYDXKUUAYMYDXKUUAYMNNYBXPYCUUAYBXPVIXKYMYQYTXTXMYAXOXLCDVOXNCDVOVJVK
XKUUAYMXPYCPZXKUUAXLHRZXNHRZNZYMUVLPXKYQUVMYTUVNCHXLVLCHXNVLVMYMXPYGYKW
FZLZUVOYCYMUVPXPYMUVPYIXQWFZXQYGYIYKXQVNXQXQXQWFUVRXQVPXQYIXQXPYHXMXOVQ
VRVSVTWAWBUVMXLWCZXNWCZUVQYCPUVNXLWDXNWDUVSUVTNYCUVQXLXNWEWGWHWIWJWKWLW
QWMWNYMABCCTYDABCCTWOWRWPXKXSCWSZYEYFDHWSXKUWAEHCDWTXAUWACXBXSXCZYEYFCX
SXDUWBYENZUWBYFUWCCXBXSXEUWBYFNABCXBXSXFCXBXSXGVTXHXIXJVH $.
$}

$( Proposition 7.48(2) of [TakeutiZaring] p. 51. (Contributed by NM,
Expand Down