Metamath Proof Explorer

Theorem harval3

Description: ( harA ) is the least cardinal that is greater than A . (Contributed by RP, 4-Nov-2023)

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

Proof

Step Hyp Ref Expression
1 harval2 
 |-  ( A e. dom card -> ( har ` A ) = |^| { y e. On | A ~< y } )
2 vex 
 |-  x e. _V
3 2 a1i 
 |-  ( A e. dom card -> x e. _V )
4 elrncard 
 |-  ( x e. ran card <-> ( x e. On /\ A. y e. x -. y ~~ x ) )
5 4 simplbi 
 |-  ( x e. ran card -> x e. On )
6 5 anim1i 
 |-  ( ( x e. ran card /\ A ~< x ) -> ( x e. On /\ A ~< x ) )
7 eleq1 
 |-  ( y = x -> ( y e. On <-> x e. On ) )
8 breq2 
 |-  ( y = x -> ( A ~< y <-> A ~< x ) )
9 7 8 anbi12d 
 |-  ( y = x -> ( ( y e. On /\ A ~< y ) <-> ( x e. On /\ A ~< x ) ) )
10 6 9 imbitrrid 
 |-  ( y = x -> ( ( x e. ran card /\ A ~< x ) -> ( y e. On /\ A ~< y ) ) )
11 10 adantl 
 |-  ( ( A e. dom card /\ y = x ) -> ( ( x e. ran card /\ A ~< x ) -> ( y e. On /\ A ~< y ) ) )
12 ssidd 
 |-  ( A e. dom card -> x C_ x )
13 3 11 12 intabssd 
 |-  ( A e. dom card -> |^| { y | ( y e. On /\ A ~< y ) } C_ |^| { x | ( x e. ran card /\ A ~< x ) } )
14 vex 
 |-  y e. _V
15 14 inex1 
 |-  ( y i^i ( card ` y ) ) e. _V
16 15 a1i 
 |-  ( A e. dom card -> ( y i^i ( card ` y ) ) e. _V )
17 oncardid 
 |-  ( y e. On -> ( card ` y ) ~~ y )
18 17 ensymd 
 |-  ( y e. On -> y ~~ ( card ` y ) )
19 sdomentr 
 |-  ( ( A ~< y /\ y ~~ ( card ` y ) ) -> A ~< ( card ` y ) )
20 19 a1i 
 |-  ( y e. On -> ( ( A ~< y /\ y ~~ ( card ` y ) ) -> A ~< ( card ` y ) ) )
21 18 20 mpan2d 
 |-  ( y e. On -> ( A ~< y -> A ~< ( card ` y ) ) )
22 df-card 
 |-  card = ( x e. _V |-> |^| { y e. On | y ~~ x } )
23 22 funmpt2 
 |-  Fun card
24 onenon 
 |-  ( y e. On -> y e. dom card )
25 fvelrn 
 |-  ( ( Fun card /\ y e. dom card ) -> ( card ` y ) e. ran card )
26 23 24 25 sylancr 
 |-  ( y e. On -> ( card ` y ) e. ran card )
27 21 26 jctild 
 |-  ( y e. On -> ( A ~< y -> ( ( card ` y ) e. ran card /\ A ~< ( card ` y ) ) ) )
28 27 adantl 
 |-  ( ( x = ( y i^i ( card ` y ) ) /\ y e. On ) -> ( A ~< y -> ( ( card ` y ) e. ran card /\ A ~< ( card ` y ) ) ) )
29 simpl 
 |-  ( ( x = ( y i^i ( card ` y ) ) /\ y e. On ) -> x = ( y i^i ( card ` y ) ) )
30 cardonle 
 |-  ( y e. On -> ( card ` y ) C_ y )
31 30 adantl 
 |-  ( ( x = ( y i^i ( card ` y ) ) /\ y e. On ) -> ( card ` y ) C_ y )
32 sseqin2 
 |-  ( ( card ` y ) C_ y <-> ( y i^i ( card ` y ) ) = ( card ` y ) )
33 31 32 sylib 
 |-  ( ( x = ( y i^i ( card ` y ) ) /\ y e. On ) -> ( y i^i ( card ` y ) ) = ( card ` y ) )
34 29 33 eqtrd 
 |-  ( ( x = ( y i^i ( card ` y ) ) /\ y e. On ) -> x = ( card ` y ) )
35 eleq1 
 |-  ( x = ( card ` y ) -> ( x e. ran card <-> ( card ` y ) e. ran card ) )
36 breq2 
 |-  ( x = ( card ` y ) -> ( A ~< x <-> A ~< ( card ` y ) ) )
37 35 36 anbi12d 
 |-  ( x = ( card ` y ) -> ( ( x e. ran card /\ A ~< x ) <-> ( ( card ` y ) e. ran card /\ A ~< ( card ` y ) ) ) )
38 34 37 syl 
 |-  ( ( x = ( y i^i ( card ` y ) ) /\ y e. On ) -> ( ( x e. ran card /\ A ~< x ) <-> ( ( card ` y ) e. ran card /\ A ~< ( card ` y ) ) ) )
39 28 38 sylibrd 
 |-  ( ( x = ( y i^i ( card ` y ) ) /\ y e. On ) -> ( A ~< y -> ( x e. ran card /\ A ~< x ) ) )
40 39 expimpd 
 |-  ( x = ( y i^i ( card ` y ) ) -> ( ( y e. On /\ A ~< y ) -> ( x e. ran card /\ A ~< x ) ) )
41 40 adantl 
 |-  ( ( A e. dom card /\ x = ( y i^i ( card ` y ) ) ) -> ( ( y e. On /\ A ~< y ) -> ( x e. ran card /\ A ~< x ) ) )
42 inss1 
 |-  ( y i^i ( card ` y ) ) C_ y
43 42 a1i 
 |-  ( A e. dom card -> ( y i^i ( card ` y ) ) C_ y )
44 16 41 43 intabssd 
 |-  ( A e. dom card -> |^| { x | ( x e. ran card /\ A ~< x ) } C_ |^| { y | ( y e. On /\ A ~< y ) } )
45 13 44 eqssd 
 |-  ( A e. dom card -> |^| { y | ( y e. On /\ A ~< y ) } = |^| { x | ( x e. ran card /\ A ~< x ) } )
46 df-rab 
 |-  { y e. On | A ~< y } = { y | ( y e. On /\ A ~< y ) }
47 46 inteqi 
 |-  |^| { y e. On | A ~< y } = |^| { y | ( y e. On /\ A ~< y ) }
48 df-rab 
 |-  { x e. ran card | A ~< x } = { x | ( x e. ran card /\ A ~< x ) }
49 48 inteqi 
 |-  |^| { x e. ran card | A ~< x } = |^| { x | ( x e. ran card /\ A ~< x ) }
50 45 47 49 3eqtr4g 
 |-  ( A e. dom card -> |^| { y e. On | A ~< y } = |^| { x e. ran card | A ~< x } )
51 1 50 eqtrd 
 |-  ( A e. dom card -> ( har ` A ) = |^| { x e. ran card | A ~< x } )