Step |
Hyp |
Ref |
Expression |
1 |
|
eloni |
|- ( x e. On -> Ord x ) |
2 |
|
ordelsuc |
|- ( ( A e. On /\ Ord x ) -> ( A e. x <-> suc A C_ x ) ) |
3 |
1 2
|
sylan2 |
|- ( ( A e. On /\ x e. On ) -> ( A e. x <-> suc A C_ x ) ) |
4 |
3
|
rabbidva |
|- ( A e. On -> { x e. On | A e. x } = { x e. On | suc A C_ x } ) |
5 |
4
|
inteqd |
|- ( A e. On -> |^| { x e. On | A e. x } = |^| { x e. On | suc A C_ x } ) |
6 |
|
sucelon |
|- ( A e. On <-> suc A e. On ) |
7 |
|
intmin |
|- ( suc A e. On -> |^| { x e. On | suc A C_ x } = suc A ) |
8 |
6 7
|
sylbi |
|- ( A e. On -> |^| { x e. On | suc A C_ x } = suc A ) |
9 |
5 8
|
eqtr2d |
|- ( A e. On -> suc A = |^| { x e. On | A e. x } ) |