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/b3ef8009-5c18-445f-90d8-9171de354f93n%40googlegroups.com.
