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 e. On /\ A. x e. On ( A ~~ x -> A C_ x ) ) )

Proof

Step Hyp Ref Expression
1 cardon 
 |-  ( card ` A ) e. On
2 eleq1 
 |-  ( ( card ` A ) = A -> ( ( card ` A ) e. On <-> A e. On ) )
3 1 2 mpbii 
 |-  ( ( card ` A ) = A -> A e. On )
4 eqss 
 |-  ( ( card ` A ) = A <-> ( ( card ` A ) C_ A /\ A C_ ( card ` A ) ) )
5 cardonle 
 |-  ( A e. On -> ( card ` A ) C_ A )
6 5 biantrurd 
 |-  ( A e. On -> ( A C_ ( card ` A ) <-> ( ( card ` A ) C_ A /\ A C_ ( card ` A ) ) ) )
7 4 6 bitr4id 
 |-  ( A e. On -> ( ( card ` A ) = A <-> A C_ ( card ` A ) ) )
8 oncardval 
 |-  ( A e. On -> ( card ` A ) = |^| { y e. On | y ~~ A } )
9 8 sseq2d 
 |-  ( A e. On -> ( A C_ ( card ` A ) <-> A C_ |^| { y e. On | y ~~ A } ) )
10 7 9 bitrd 
 |-  ( A e. On -> ( ( card ` A ) = A <-> A C_ |^| { y e. On | y ~~ A } ) )
11 ssint 
 |-  ( A C_ |^| { y e. On | y ~~ A } <-> A. x e. { y e. On | y ~~ A } A C_ x )
12 breq1 
 |-  ( y = x -> ( y ~~ A <-> x ~~ A ) )
13 12 elrab 
 |-  ( x e. { y e. On | y ~~ A } <-> ( x e. On /\ x ~~ A ) )
14 ensymb 
 |-  ( x ~~ A <-> A ~~ x )
15 14 anbi2i 
 |-  ( ( x e. On /\ x ~~ A ) <-> ( x e. On /\ A ~~ x ) )
16 13 15 bitri 
 |-  ( x e. { y e. On | y ~~ A } <-> ( x e. On /\ A ~~ x ) )
17 16 imbi1i 
 |-  ( ( x e. { y e. On | y ~~ A } -> A C_ x ) <-> ( ( x e. On /\ A ~~ x ) -> A C_ x ) )
18 impexp 
 |-  ( ( ( x e. On /\ A ~~ x ) -> A C_ x ) <-> ( x e. On -> ( A ~~ x -> A C_ x ) ) )
19 17 18 bitri 
 |-  ( ( x e. { y e. On | y ~~ A } -> A C_ x ) <-> ( x e. On -> ( A ~~ x -> A C_ x ) ) )
20 19 ralbii2 
 |-  ( A. x e. { y e. On | y ~~ A } A C_ x <-> A. x e. On ( A ~~ x -> A C_ x ) )
21 11 20 bitri 
 |-  ( A C_ |^| { y e. On | y ~~ A } <-> A. x e. On ( A ~~ x -> A C_ x ) )
22 10 21 bitrdi 
 |-  ( A e. On -> ( ( card ` A ) = A <-> A. x e. On ( A ~~ x -> A C_ x ) ) )
23 3 22 biadanii 
 |-  ( ( card ` A ) = A <-> ( A e. On /\ A. x e. On ( A ~~ x -> A C_ x ) ) )