Metamath Proof Explorer


Theorem iscard2

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

Ref Expression
Assertion iscard2 card A = A A On x On A x A x

Proof

Step Hyp Ref Expression
1 cardon card A On
2 eleq1 card A = A card A On A On
3 1 2 mpbii card A = A A On
4 eqss card A = A card A A A card A
5 cardonle A On card A A
6 5 biantrurd A On A card A card A A A card A
7 4 6 bitr4id A On card A = A A card A
8 oncardval A On card A = y On | y A
9 8 sseq2d A On A card A A y On | y A
10 7 9 bitrd A On card A = A A y On | y A
11 ssint A y On | y A x y On | y A A x
12 breq1 y = x y A x A
13 12 elrab x y On | y A x On x A
14 ensymb x A A x
15 14 anbi2i x On x A x On A x
16 13 15 bitri x y On | y A x On A x
17 16 imbi1i x y On | y A A x x On A x A x
18 impexp x On A x A x x On A x A x
19 17 18 bitri x y On | y A A x x On A x A x
20 19 ralbii2 x y On | y A A x x On A x A x
21 11 20 bitri A y On | y A x On A x A x
22 10 21 bitrdi A On card A = A x On A x A x
23 3 22 biadanii card A = A A On x On A x A x