Reduce ax-un usage

[BTernaryTau]

This change revises 1onn and 2onn to no longer depend on ax-un. It also revises snnen2o to no longer depend on ax-un or ax-pow and moves it out of the Pigeonhole Principle section since it doesn't make use of php anymore. It also introduces several new theorems that avoid ax-un.

f1cdmsn

If a one-to-one function with a nonempty domain has a singleton as its codomain, its domain must also be a singleton.

nlim1

1 is not a limit ordinal.

nlim2

2 is not a limit ordinal.

ord1eln01

An ordinal that is not 0 or 1 contains 1.

ord2eln012

An ordinal that is not 0, 1, or 2 contains 2.

1ellim

A limit ordinal contains 1.

2ellim

A limit ordinal contains 2.

Changes in axiom usage: a3ca221

[icecream17]

Incidentally, metamath seems to use range more often than codomain. I only just seen that there was a difference:

Codomain: The set of all possible output values that a function could produce
Range: The subset of those values that the function actually does produce
https://math.stackexchange.com/questions/3317941/what-is-the-difference-between-codomain-and-range

This means ~ frn and such is somewhat of a misnomer?

[BTernaryTau]

This means ~ frn and such is somewhat of a misnomer?

frn is fine since it explicitly deals with the function's range. foelrni is a better example since the statement doesn't reference the function's range and its description refers to the codomain. However, since it's about onto functions, the range and codomain are equal, so I don't think this is a big deal. The problem case (in my opinion) is theorems like ffvelrn and frnssb that don't deal with the range, only the codomain.

[jkingdon]

The problem case (in my opinion) is theorems like ffvelrn and frnssb that don't deal with the range, only the codomain.

The good news is that the comments correctly refer to the codomain and don't contain the word "range", which doesn't apply here.

Whether we want to rename them to something not containing rn I guess I don't have a strong opinion about. Maybe they could just be called ffvel and ssf (or something else with an f in it). The name fragment f refers to F : X --> Y notation and thus means that the theorem will be specifying a codomain (in this example Y).

[avekens]

The problem case (in my opinion) is theorems like ffvelrn and frnssb that don't deal with the range, only the codomain.

The good news is that the comments correctly refer to the codomain and don't contain the word "range", which doesn't apply here.

Whether we want to rename them to something not containing rn I guess I don't have a strong opinion about. Maybe they could just be called ffvel and ssf (or something else with an f in it). The name fragment f refers to F : X --> Y notation and thus means that the theorem will be specifying a codomain (in this example Y).

Maybe we should replace "rn" by "cdm" in the label in such cases, like here done with ~f1cdmsn, or also other theorems in set.mm (e.g., ~focdmex).

This discussion about label names should not block this PR. Maybe an issue could be open for this.

[avekens]

Issue #4470 created for adjusting the label names, so that this PR can be merged and closed.