Metamath Proof Explorer

Theorem iscard4

Description: Two ways to express the property of being a cardinal number. (Contributed by RP, 8-Nov-2023)

Ref Expression
Assertion iscard4 
|- ( ( card ` A ) = A <-> A e. ran card )

Proof

Step Hyp Ref Expression
1 eqcom 
 |-  ( ( card ` A ) = A <-> A = ( card ` A ) )
2 mptrel 
 |-  Rel ( x e. _V |-> |^| { y e. On | y ~~ x } )
3 df-card 
 |-  card = ( x e. _V |-> |^| { y e. On | y ~~ x } )
4 3 releqi 
 |-  ( Rel card <-> Rel ( x e. _V |-> |^| { y e. On | y ~~ x } ) )
5 2 4 mpbir 
 |-  Rel card
6 relelrnb 
 |-  ( Rel card -> ( A e. ran card <-> E. x x card A ) )
7 5 6 ax-mp 
 |-  ( A e. ran card <-> E. x x card A )
8 3 funmpt2 
 |-  Fun card
9 funbrfv 
 |-  ( Fun card -> ( x card A -> ( card ` x ) = A ) )
10 8 9 ax-mp 
 |-  ( x card A -> ( card ` x ) = A )
11 10 eqcomd 
 |-  ( x card A -> A = ( card ` x ) )
12 11 eximi 
 |-  ( E. x x card A -> E. x A = ( card ` x ) )
13 cardidm 
 |-  ( card ` ( card ` x ) ) = ( card ` x )
14 fveq2 
 |-  ( A = ( card ` x ) -> ( card ` A ) = ( card ` ( card ` x ) ) )
15 id 
 |-  ( A = ( card ` x ) -> A = ( card ` x ) )
16 13 14 15 3eqtr4a 
 |-  ( A = ( card ` x ) -> ( card ` A ) = A )
17 16 exlimiv 
 |-  ( E. x A = ( card ` x ) -> ( card ` A ) = A )
18 1 biimpi 
 |-  ( ( card ` A ) = A -> A = ( card ` A ) )
19 cardon 
 |-  ( card ` A ) e. On
20 18 19 eqeltrdi 
 |-  ( ( card ` A ) = A -> A e. On )
21 onenon 
 |-  ( A e. On -> A e. dom card )
22 20 21 syl 
 |-  ( ( card ` A ) = A -> A e. dom card )
23 funfvbrb 
 |-  ( Fun card -> ( A e. dom card <-> A card ( card ` A ) ) )
24 23 biimpd 
 |-  ( Fun card -> ( A e. dom card -> A card ( card ` A ) ) )
25 8 22 24 mpsyl 
 |-  ( ( card ` A ) = A -> A card ( card ` A ) )
26 id 
 |-  ( ( card ` A ) = A -> ( card ` A ) = A )
27 25 26 breqtrd 
 |-  ( ( card ` A ) = A -> A card A )
28 id 
 |-  ( A = ( card ` A ) -> A = ( card ` A ) )
29 28 19 eqeltrdi 
 |-  ( A = ( card ` A ) -> A e. On )
30 29 eqcoms 
 |-  ( ( card ` A ) = A -> A e. On )
31 sbcbr1g 
 |-  ( A e. On -> ( [. A / x ]. x card A <-> [_ A / x ]_ x card A ) )
32 csbvarg 
 |-  ( A e. On -> [_ A / x ]_ x = A )
33 32 breq1d 
 |-  ( A e. On -> ( [_ A / x ]_ x card A <-> A card A ) )
34 31 33 bitrd 
 |-  ( A e. On -> ( [. A / x ]. x card A <-> A card A ) )
35 30 34 syl 
 |-  ( ( card ` A ) = A -> ( [. A / x ]. x card A <-> A card A ) )
36 27 35 mpbird 
 |-  ( ( card ` A ) = A -> [. A / x ]. x card A )
37 36 spesbcd 
 |-  ( ( card ` A ) = A -> E. x x card A )
38 17 37 syl 
 |-  ( E. x A = ( card ` x ) -> E. x x card A )
39 12 38 impbii 
 |-  ( E. x x card A <-> E. x A = ( card ` x ) )
40 oncard 
 |-  ( E. x A = ( card ` x ) <-> A = ( card ` A ) )
41 7 39 40 3bitrri 
 |-  ( A = ( card ` A ) <-> A e. ran card )
42 1 41 bitri 
 |-  ( ( card ` A ) = A <-> A e. ran card )