search

metamath / set.mm

Metamath source file for logic and set theory
Creative Commons Zero v1.0 Universal
238 stars 87 forks source link

Revise ficardun and related theorems #4072

Closed BTernaryTau closed 2 weeks ago

BTernaryTau commented 2 weeks ago

This change revises nnadju, ficardun, and ficardun2 so that they no longer depend on ax-rep. It also introduces ficardadju as a new theorem.

The disjoint union of finite sets is equinumerous to the ordinal sum of the cardinalities of those sets.

I kept the current nnadju proof around as nnadjuALT since it's much shorter and uses a different approach, though I'm not sure how strong the requirements are for justifying keeping an alternate proof.

The revision to ficardun in particular affects a lot of other theorems through hashun, including hashbc (Metamath 100 proof #​58).

jkingdon commented 2 weeks ago

I kept the current nnadju proof around as nnadjuALT since it's much shorter and uses a different approach, though I'm not sure how strong the requirements are for justifying keeping an alternate proof.

Shorter proof and different approach generally would be a reason to have an ALT proof.

If someone who has looked more closely at this case than I have has an opinion, feel free to speak up, but seems like a case where it seems like a good idea.