Metamath Proof Explorer

Theorem harcard

Description: The class of ordinal numbers dominated by a set is a cardinal number. Theorem 59 of Suppes p. 228. (Contributed by Mario Carneiro, 20-Jan-2013) (Revised by Mario Carneiro, 15-May-2015)

Ref Expression
Assertion harcard 
|- ( card ` ( har ` A ) ) = ( har ` A )

Proof

Step Hyp Ref Expression
1 harcl 
 |-  ( har ` A ) e. On
2 harndom 
 |-  -. ( har ` A ) ~<_ A
3 simpll 
 |-  ( ( ( x e. On /\ ( har ` A ) ~~ x ) /\ y e. ( har ` A ) ) -> x e. On )
4 elharval 
 |-  ( y e. ( har ` A ) <-> ( y e. On /\ y ~<_ A ) )
5 4 bilani 
 |-  ( ( ( x e. On /\ ( har ` A ) ~~ x ) /\ y e. ( har ` A ) ) -> ( y e. On /\ y ~<_ A ) )
6 5 simpld 
 |-  ( ( ( x e. On /\ ( har ` A ) ~~ x ) /\ y e. ( har ` A ) ) -> y e. On )
7 ontri1 
 |-  ( ( x e. On /\ y e. On ) -> ( x C_ y <-> -. y e. x ) )
8 3 6 7 syl2anc 
 |-  ( ( ( x e. On /\ ( har ` A ) ~~ x ) /\ y e. ( har ` A ) ) -> ( x C_ y <-> -. y e. x ) )
9 simpllr 
 |-  ( ( ( ( x e. On /\ ( har ` A ) ~~ x ) /\ y e. ( har ` A ) ) /\ x C_ y ) -> ( har ` A ) ~~ x )
10 ssdomg 
 |-  ( y e. _V -> ( x C_ y -> x ~<_ y ) )
11 10 elv 
 |-  ( x C_ y -> x ~<_ y )
12 5 simprd 
 |-  ( ( ( x e. On /\ ( har ` A ) ~~ x ) /\ y e. ( har ` A ) ) -> y ~<_ A )
13 domtr 
 |-  ( ( x ~<_ y /\ y ~<_ A ) -> x ~<_ A )
14 11 12 13 syl2anr 
 |-  ( ( ( ( x e. On /\ ( har ` A ) ~~ x ) /\ y e. ( har ` A ) ) /\ x C_ y ) -> x ~<_ A )
15 endomtr 
 |-  ( ( ( har ` A ) ~~ x /\ x ~<_ A ) -> ( har ` A ) ~<_ A )
16 9 14 15 syl2anc 
 |-  ( ( ( ( x e. On /\ ( har ` A ) ~~ x ) /\ y e. ( har ` A ) ) /\ x C_ y ) -> ( har ` A ) ~<_ A )
17 16 ex 
 |-  ( ( ( x e. On /\ ( har ` A ) ~~ x ) /\ y e. ( har ` A ) ) -> ( x C_ y -> ( har ` A ) ~<_ A ) )
18 8 17 sylbird 
 |-  ( ( ( x e. On /\ ( har ` A ) ~~ x ) /\ y e. ( har ` A ) ) -> ( -. y e. x -> ( har ` A ) ~<_ A ) )
19 2 18 mt3i 
 |-  ( ( ( x e. On /\ ( har ` A ) ~~ x ) /\ y e. ( har ` A ) ) -> y e. x )
20 19 ex 
 |-  ( ( x e. On /\ ( har ` A ) ~~ x ) -> ( y e. ( har ` A ) -> y e. x ) )
21 20 ssrdv 
 |-  ( ( x e. On /\ ( har ` A ) ~~ x ) -> ( har ` A ) C_ x )
22 21 ex 
 |-  ( x e. On -> ( ( har ` A ) ~~ x -> ( har ` A ) C_ x ) )
23 22 rgen 
 |-  A. x e. On ( ( har ` A ) ~~ x -> ( har ` A ) C_ x )
24 iscard2 
 |-  ( ( card ` ( har ` A ) ) = ( har ` A ) <-> ( ( har ` A ) e. On /\ A. x e. On ( ( har ` A ) ~~ x -> ( har ` A ) C_ x ) ) )
25 1 23 24 mpbir2an 
 |-  ( card ` ( har ` A ) ) = ( har ` A )