Fun with metamath.

While reading Wikipedia on different subjects in proof calculus I found the link to Metamath. Metamath is similar to the site I was thinking of writing about here. The problem I have with Metamath is that even though it explains in good detail what are its axioms and what axioms are added when more subjects are taken in it really doesn't explain why. It references Tarski's axioms but it doesn't note that the major thing about these axioms is that they are tautologies. That simple thing already makes axioms much more understandable. Another example where lack of this example is annoying is when you try to open the definition of complex limit you end up this $Slot9$ which simple Wikipedia search I didn't find anything understandable. Maybe I could understand if I had studied more topology but should I need to or should Metamath have a better explanation ready? Anyhow, I really would like to find some bit more complex on Metamath and open it fully but I think I have to learn more on certain topics before I could do that.