This is a fun thing. For more about the underlying system, see:
<a href="http://us.metamath.org/mpeuni/mmset.html" rel="nofollow">http://us.metamath.org/mpeuni/mmset.html</a>
Reminds me of an old Rudy Rucker story, 'A New Golden Age':<p><a href="http://www.rudyrucker.com/transrealbooks/completestories/#_Toc05" rel="nofollow">http://www.rudyrucker.com/transrealbooks/completestories/#_T...</a>
Listening to "axiom of choice equivalent" there is at some point a descending line and then a repetition of the main theme. Quite interesting.