Sorry, our emails crossed with Mario, so when I was mentionning the proof above (and the typo), I meant the previous one!
On Monday, November 1, 2021 at 4:56:11 PM UTC+1 Benoit wrote: > On Monday, November 1, 2021 at 4:34:10 PM UTC+1 Thierry Arnoux wrote: > >> In order to make that work, I had to introduce two new axioms. I wonder >> if anyone can eliminate any of them, or propose a cleverer approach. > > > Note that your ax-abidc is basically bj-eleq1w or Mario's ax-8c above (he > wrote ax-9c instead). The need to define not two but three predicates for > membership reflects the three step process in Levy's proof or Mario's proof > above. > > Benoît > -- 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/0771e456-62b6-4a34-a551-9e7bad9d11cfn%40googlegroups.com.
