| Step |
Hyp |
Ref |
Expression |
| 1 |
|
wfax.1 |
|- W = U. ( R1 " On ) |
| 2 |
|
ssclaxsep |
|- ( A. z e. W ~P z C_ W -> A. z e. W E. y e. W A. x e. W ( x e. y <-> ( x e. z /\ ph ) ) ) |
| 3 |
|
pwwf |
|- ( z e. U. ( R1 " On ) <-> ~P z e. U. ( R1 " On ) ) |
| 4 |
|
r1elssi |
|- ( ~P z e. U. ( R1 " On ) -> ~P z C_ U. ( R1 " On ) ) |
| 5 |
3 4
|
sylbi |
|- ( z e. U. ( R1 " On ) -> ~P z C_ U. ( R1 " On ) ) |
| 6 |
1
|
eleq2i |
|- ( z e. W <-> z e. U. ( R1 " On ) ) |
| 7 |
1
|
sseq2i |
|- ( ~P z C_ W <-> ~P z C_ U. ( R1 " On ) ) |
| 8 |
5 6 7
|
3imtr4i |
|- ( z e. W -> ~P z C_ W ) |
| 9 |
2 8
|
mprg |
|- A. z e. W E. y e. W A. x e. W ( x e. y <-> ( x e. z /\ ph ) ) |