Step |
Hyp |
Ref |
Expression |
1 |
|
setc1strwun.s |
|- S = ( SetCat ` U ) |
2 |
|
setc1strwun.c |
|- C = ( Base ` S ) |
3 |
|
setc1strwun.u |
|- ( ph -> U e. WUni ) |
4 |
|
setc1strwun.o |
|- ( ph -> _om e. U ) |
5 |
1 3
|
setcbas |
|- ( ph -> U = ( Base ` S ) ) |
6 |
2 5
|
eqtr4id |
|- ( ph -> C = U ) |
7 |
6
|
eleq2d |
|- ( ph -> ( X e. C <-> X e. U ) ) |
8 |
7
|
biimpa |
|- ( ( ph /\ X e. C ) -> X e. U ) |
9 |
|
eqid |
|- { <. ( Base ` ndx ) , X >. } = { <. ( Base ` ndx ) , X >. } |
10 |
9 3 4
|
1strwun |
|- ( ( ph /\ X e. U ) -> { <. ( Base ` ndx ) , X >. } e. U ) |
11 |
8 10
|
syldan |
|- ( ( ph /\ X e. C ) -> { <. ( Base ` ndx ) , X >. } e. U ) |