Step |
Hyp |
Ref |
Expression |
1 |
|
id |
|- ( R Or A -> R Or A ) |
2 |
1
|
supval2 |
|- ( R Or A -> sup ( (/) , A , R ) = ( iota_ x e. A ( A. y e. (/) -. x R y /\ A. y e. A ( y R x -> E. z e. (/) y R z ) ) ) ) |
3 |
|
ral0 |
|- A. y e. (/) -. x R y |
4 |
3
|
biantrur |
|- ( A. y e. A ( y R x -> E. z e. (/) y R z ) <-> ( A. y e. (/) -. x R y /\ A. y e. A ( y R x -> E. z e. (/) y R z ) ) ) |
5 |
|
rex0 |
|- -. E. z e. (/) y R z |
6 |
|
imnot |
|- ( -. E. z e. (/) y R z -> ( ( y R x -> E. z e. (/) y R z ) <-> -. y R x ) ) |
7 |
5 6
|
ax-mp |
|- ( ( y R x -> E. z e. (/) y R z ) <-> -. y R x ) |
8 |
7
|
ralbii |
|- ( A. y e. A ( y R x -> E. z e. (/) y R z ) <-> A. y e. A -. y R x ) |
9 |
4 8
|
bitr3i |
|- ( ( A. y e. (/) -. x R y /\ A. y e. A ( y R x -> E. z e. (/) y R z ) ) <-> A. y e. A -. y R x ) |
10 |
9
|
a1i |
|- ( R Or A -> ( ( A. y e. (/) -. x R y /\ A. y e. A ( y R x -> E. z e. (/) y R z ) ) <-> A. y e. A -. y R x ) ) |
11 |
10
|
riotabidv |
|- ( R Or A -> ( iota_ x e. A ( A. y e. (/) -. x R y /\ A. y e. A ( y R x -> E. z e. (/) y R z ) ) ) = ( iota_ x e. A A. y e. A -. y R x ) ) |
12 |
2 11
|
eqtrd |
|- ( R Or A -> sup ( (/) , A , R ) = ( iota_ x e. A A. y e. A -. y R x ) ) |