Step |
Hyp |
Ref |
Expression |
1 |
|
elfvex |
|- ( U e. ( UnifOn ` X ) -> X e. _V ) |
2 |
|
isust |
|- ( X e. _V -> ( U e. ( UnifOn ` X ) <-> ( U C_ ~P ( X X. X ) /\ ( X X. X ) e. U /\ A. v e. U ( A. w e. ~P ( X X. X ) ( v C_ w -> w e. U ) /\ A. w e. U ( v i^i w ) e. U /\ ( ( _I |` X ) C_ v /\ `' v e. U /\ E. w e. U ( w o. w ) C_ v ) ) ) ) ) |
3 |
1 2
|
syl |
|- ( U e. ( UnifOn ` X ) -> ( U e. ( UnifOn ` X ) <-> ( U C_ ~P ( X X. X ) /\ ( X X. X ) e. U /\ A. v e. U ( A. w e. ~P ( X X. X ) ( v C_ w -> w e. U ) /\ A. w e. U ( v i^i w ) e. U /\ ( ( _I |` X ) C_ v /\ `' v e. U /\ E. w e. U ( w o. w ) C_ v ) ) ) ) ) |
4 |
3
|
ibi |
|- ( U e. ( UnifOn ` X ) -> ( U C_ ~P ( X X. X ) /\ ( X X. X ) e. U /\ A. v e. U ( A. w e. ~P ( X X. X ) ( v C_ w -> w e. U ) /\ A. w e. U ( v i^i w ) e. U /\ ( ( _I |` X ) C_ v /\ `' v e. U /\ E. w e. U ( w o. w ) C_ v ) ) ) ) |
5 |
4
|
simp1d |
|- ( U e. ( UnifOn ` X ) -> U C_ ~P ( X X. X ) ) |
6 |
5
|
sselda |
|- ( ( U e. ( UnifOn ` X ) /\ V e. U ) -> V e. ~P ( X X. X ) ) |
7 |
6
|
elpwid |
|- ( ( U e. ( UnifOn ` X ) /\ V e. U ) -> V C_ ( X X. X ) ) |