Step |
Hyp |
Ref |
Expression |
1 |
|
supmo.1 |
|- ( ph -> R Or A ) |
2 |
|
df-sup |
|- sup ( B , A , R ) = U. { x e. A | ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) } |
3 |
1
|
supmo |
|- ( ph -> E* x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) ) |
4 |
|
rmorabex |
|- ( E* x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) -> { x e. A | ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) } e. _V ) |
5 |
|
uniexg |
|- ( { x e. A | ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) } e. _V -> U. { x e. A | ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) } e. _V ) |
6 |
3 4 5
|
3syl |
|- ( ph -> U. { x e. A | ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) } e. _V ) |
7 |
2 6
|
eqeltrid |
|- ( ph -> sup ( B , A , R ) e. _V ) |