Re: [mizar] [Thomas Forster] Re: [FOM] Historical Queries on AC

[Andrzej Trybulec <trybulec@math.uwb.edu.pl>]

Jesse Alama wrote:

> Judging from Forster's reaction and questions that I've received from
> subscribers to the FOM mailing list concerning my post on TG, it looks
> like there's some surprise that Choice is a theorem of TG.  The surprise
> is that the universe axiom implies AC.  That was my intuition as well;
> those two don't seem to be related to each other.  Can anyone provide an
> intuitive sketch of why that follows?
>
>  
I am so sorry. My previous message was an answer rather to Thomas 
Forster's question:

> You mean that if there is a proper class of strong inaccessibles then AC 
> follows..?   Surely you can't mean that!?!


Original proof of Tarski is formalised in WELLSET1. But the Grzegorz's proof (WELLORD2) is based on a quite simple idea. Let U be a universe (CLASSES2), consider
    On U 
the set of all ordinal numbers in U, it does not belong to U, so U and On U are equipotent.
But On U is well-ordred, so U is well-ordered, too.

U is transitive, every set that belongs to U is well-ordered as well.

Regards,
Andrzej


>