Mathbox global choice changes

[BTernaryTau]

Mathbox additions

• jaeqifi: Inference combining four equality antecedents into one equality of conditional operators antecedent.
• f1preimaex: If the image under a one-to-one function exists, then the corresponding preimage also exists.
• soinfdom: A strict order relation on an infinite set dominates that set.
• abweex: The class of well-orders of a set A and its subsets is a set.
• werankwe: Construct a well-order given a relation R ( x ) that well-orders elements of the same rank.
• weexenwe: If a well-ordering of an infinite set exists, then a well-ordering equinumerous to the set exists.
• infinfnum: Equivalence between two infiniteness criteria for numerable sets.
• rncardr1prc: The Axiom of Choice implies that the cardinalities of the layers of the cumulative hierarchy form a proper class.
• acwer1prclem: Lemma for ~ acwer1prc .
• acwer1prc: The class of all well-orderings of the stages of the cumulative hierarchy is a proper class.
• vonf1onprcf1ac: If F maps the universe one-to-one into the ordinals and A is a proper class, then I maps the ordinals one-to-one into A and the Axiom of Choice holds. This is the ZFC version of (6 -> 7) in ~ https://tinyurl.com/hamkins-gblac . Note that in NBG set theory the first hypothesis would be something like ph -> A. X E. F F : X -1-1-> On , but since we cannot quantify over classes, we instead consider only the case X = _V which is sufficient for this proof.
• onprcf1acwevdlem1: Lemma for ~ onprcf1acwevd .
• onprcf1acwevdlem2: Lemma for ~ onprcf1acwevd .
• onprcf1acwevd: If F maps the ordinals one-to-one into the proper class W and the Axiom of Choice holds, then R well-orders the universe. This is the ZFC version of (7 -> 3) in ~ https://tinyurl.com/hamkins-gblac . Note that in NBG set theory the first hypothesis would be something like ( ph -> A. X ( -. X e. _V -> E. F F : On -1-1-> X ) ) , but since we cannot quantify over classes, we instead consider only the case X = W which is sufficient for this proof.

Moves to main

• Moved fnwe2val, fnwe2, and lemmas to right after fnwe

[langgerard]

I have the following comments:
1: Constructible sets and global choice : Do you intend to prove that if V satistisfies ZF(C), then the proper class L of all constructible sets is an (the smallest) inner model of ZF + Global choice + GCH included in V ?

2: Classes Fin and Hf : Maybe it would be interesting to prove that if V satisfies ZF (including ax-inf), then Fin is a proper class, because every singleton of an ordinal is a finite set bijective with the ordinal 1 and On is a proper class, when Hf is a set, being the union on om of the sets R1(n). Specially the singleton of om is a finite set, but is not in the class Hf because its only member om is not in Hf.

[langgerard]

Addition to my previous message/
3: Classes Fin and Hf in the case that V = Fin, so that we negate ax-inf:
a/ In this case, we have On = om, so that with ax-reg we have Fin = V = R(On) = R(om) = Hf, that becomes a proper class.
b/ But, if we do not have ax-reg, it is possible to have finite sets x that are not well-founded, as proved by the theorem fineqvinfep (35694), so that it is possible that Hf is strictly included in Fin = V.
This is notably the case if we have some (Russel) sets are identical with their singleton, so are in the class Fin, but cannot be in Hf, because they are not well-founded. If they had a rank, we would have rank(x) = 1 + rank(x), that is impossible, so that it is possible that Hf can be a set that is strictly included in Fin

[BTernaryTau]

For 1, I'm not sure exactly how far I'll get, but I would like to at least prove that V = L gives us a global choice function. I don't currently have plans for 2 and 3.