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