Metamath Proof Explorer


Theorem iscard

Description: Two ways to express the property of being a cardinal number. (Contributed by Mario Carneiro, 15-Jan-2013)

Ref Expression
Assertion iscard cardA=AAOnxAxA

Proof

Step Hyp Ref Expression
1 cardon cardAOn
2 eleq1 cardA=AcardAOnAOn
3 1 2 mpbii cardA=AAOn
4 cardonle AOncardAA
5 eqss cardA=AcardAAAcardA
6 5 baibr cardAAAcardAcardA=A
7 4 6 syl AOnAcardAcardA=A
8 dfss3 AcardAxAxcardA
9 onelon AOnxAxOn
10 onenon AOnAdomcard
11 10 adantr AOnxAAdomcard
12 cardsdomel xOnAdomcardxAxcardA
13 9 11 12 syl2anc AOnxAxAxcardA
14 13 ralbidva AOnxAxAxAxcardA
15 8 14 bitr4id AOnAcardAxAxA
16 7 15 bitr3d AOncardA=AxAxA
17 3 16 biadanii cardA=AAOnxAxA