Metamath Proof Explorer


Theorem elrncard

Description: Let us define a cardinal number to be an element A e. On such that A is not equipotent with any x e. A . (Contributed by RP, 1-Oct-2023)

Ref Expression
Assertion elrncard ArancardAOnxA¬xA

Proof

Step Hyp Ref Expression
1 iscard4 cardA=AArancard
2 iscard5 cardA=AAOnxA¬xA
3 1 2 bitr3i ArancardAOnxA¬xA