This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem harval2

Description: An alternate expression for the Hartogs number of a well-orderable set. (Contributed by Mario Carneiro, 15-May-2015)

Ref Expression
Assertion harval2 
|- ( A e. dom card -> ( har ` A ) = |^| { x e. On | A ~< x } )

Proof

Step Hyp Ref Expression
1 harval 
 |-  ( A e. dom card -> ( har ` A ) = { y e. On | y ~<_ A } )
2 1 adantr 
 |-  ( ( A e. dom card /\ ( x e. On /\ A ~< x ) ) -> ( har ` A ) = { y e. On | y ~<_ A } )
3 sdomel 
 |-  ( ( y e. On /\ x e. On ) -> ( y ~< x -> y e. x ) )
4 domsdomtr 
 |-  ( ( y ~<_ A /\ A ~< x ) -> y ~< x )
5 3 4 impel 
 |-  ( ( ( y e. On /\ x e. On ) /\ ( y ~<_ A /\ A ~< x ) ) -> y e. x )
6 5 an4s 
 |-  ( ( ( y e. On /\ y ~<_ A ) /\ ( x e. On /\ A ~< x ) ) -> y e. x )
7 6 ancoms 
 |-  ( ( ( x e. On /\ A ~< x ) /\ ( y e. On /\ y ~<_ A ) ) -> y e. x )
8 7 3impb 
 |-  ( ( ( x e. On /\ A ~< x ) /\ y e. On /\ y ~<_ A ) -> y e. x )
9 8 rabssdv 
 |-  ( ( x e. On /\ A ~< x ) -> { y e. On | y ~<_ A } C_ x )
10 9 adantl 
 |-  ( ( A e. dom card /\ ( x e. On /\ A ~< x ) ) -> { y e. On | y ~<_ A } C_ x )
11 2 10 eqsstrd 
 |-  ( ( A e. dom card /\ ( x e. On /\ A ~< x ) ) -> ( har ` A ) C_ x )
12 11 expr 
 |-  ( ( A e. dom card /\ x e. On ) -> ( A ~< x -> ( har ` A ) C_ x ) )
13 12 ralrimiva 
 |-  ( A e. dom card -> A. x e. On ( A ~< x -> ( har ` A ) C_ x ) )
14 ssintrab 
 |-  ( ( har ` A ) C_ |^| { x e. On | A ~< x } <-> A. x e. On ( A ~< x -> ( har ` A ) C_ x ) )
15 13 14 sylibr 
 |-  ( A e. dom card -> ( har ` A ) C_ |^| { x e. On | A ~< x } )
16 breq2 
 |-  ( x = ( har ` A ) -> ( A ~< x <-> A ~< ( har ` A ) ) )
17 harcl 
 |-  ( har ` A ) e. On
18 17 a1i 
 |-  ( A e. dom card -> ( har ` A ) e. On )
19 harsdom 
 |-  ( A e. dom card -> A ~< ( har ` A ) )
20 16 18 19 elrabd 
 |-  ( A e. dom card -> ( har ` A ) e. { x e. On | A ~< x } )
21 intss1 
 |-  ( ( har ` A ) e. { x e. On | A ~< x } -> |^| { x e. On | A ~< x } C_ ( har ` A ) )
22 20 21 syl 
 |-  ( A e. dom card -> |^| { x e. On | A ~< x } C_ ( har ` A ) )
23 15 22 eqssd 
 |-  ( A e. dom card -> ( har ` A ) = |^| { x e. On | A ~< x } )