Step |
Hyp |
Ref |
Expression |
1 |
|
alephon |
|- ( aleph ` suc A ) e. On |
2 |
1
|
oneli |
|- ( y e. ( aleph ` suc A ) -> y e. On ) |
3 |
|
alephcard |
|- ( card ` ( aleph ` suc A ) ) = ( aleph ` suc A ) |
4 |
|
iscard |
|- ( ( card ` ( aleph ` suc A ) ) = ( aleph ` suc A ) <-> ( ( aleph ` suc A ) e. On /\ A. y e. ( aleph ` suc A ) y ~< ( aleph ` suc A ) ) ) |
5 |
3 4
|
mpbi |
|- ( ( aleph ` suc A ) e. On /\ A. y e. ( aleph ` suc A ) y ~< ( aleph ` suc A ) ) |
6 |
5
|
simpri |
|- A. y e. ( aleph ` suc A ) y ~< ( aleph ` suc A ) |
7 |
6
|
rspec |
|- ( y e. ( aleph ` suc A ) -> y ~< ( aleph ` suc A ) ) |
8 |
2 7
|
jca |
|- ( y e. ( aleph ` suc A ) -> ( y e. On /\ y ~< ( aleph ` suc A ) ) ) |
9 |
|
sdomel |
|- ( ( y e. On /\ ( aleph ` suc A ) e. On ) -> ( y ~< ( aleph ` suc A ) -> y e. ( aleph ` suc A ) ) ) |
10 |
1 9
|
mpan2 |
|- ( y e. On -> ( y ~< ( aleph ` suc A ) -> y e. ( aleph ` suc A ) ) ) |
11 |
10
|
imp |
|- ( ( y e. On /\ y ~< ( aleph ` suc A ) ) -> y e. ( aleph ` suc A ) ) |
12 |
8 11
|
impbii |
|- ( y e. ( aleph ` suc A ) <-> ( y e. On /\ y ~< ( aleph ` suc A ) ) ) |
13 |
|
breq1 |
|- ( x = y -> ( x ~< ( aleph ` suc A ) <-> y ~< ( aleph ` suc A ) ) ) |
14 |
13
|
elrab |
|- ( y e. { x e. On | x ~< ( aleph ` suc A ) } <-> ( y e. On /\ y ~< ( aleph ` suc A ) ) ) |
15 |
12 14
|
bitr4i |
|- ( y e. ( aleph ` suc A ) <-> y e. { x e. On | x ~< ( aleph ` suc A ) } ) |
16 |
15
|
eqriv |
|- ( aleph ` suc A ) = { x e. On | x ~< ( aleph ` suc A ) } |
17 |
|
alephsucdom |
|- ( A e. On -> ( x ~<_ ( aleph ` A ) <-> x ~< ( aleph ` suc A ) ) ) |
18 |
17
|
rabbidv |
|- ( A e. On -> { x e. On | x ~<_ ( aleph ` A ) } = { x e. On | x ~< ( aleph ` suc A ) } ) |
19 |
16 18
|
eqtr4id |
|- ( A e. On -> ( aleph ` suc A ) = { x e. On | x ~<_ ( aleph ` A ) } ) |