| Step |
Hyp |
Ref |
Expression |
| 1 |
|
utopustuq.1 |
|- N = ( p e. X |-> ran ( v e. U |-> ( v " { p } ) ) ) |
| 2 |
|
ustbasel |
|- ( U e. ( UnifOn ` X ) -> ( X X. X ) e. U ) |
| 3 |
|
snssi |
|- ( p e. X -> { p } C_ X ) |
| 4 |
|
dfss |
|- ( { p } C_ X <-> { p } = ( { p } i^i X ) ) |
| 5 |
3 4
|
sylib |
|- ( p e. X -> { p } = ( { p } i^i X ) ) |
| 6 |
|
incom |
|- ( { p } i^i X ) = ( X i^i { p } ) |
| 7 |
5 6
|
eqtr2di |
|- ( p e. X -> ( X i^i { p } ) = { p } ) |
| 8 |
|
snnzg |
|- ( p e. X -> { p } =/= (/) ) |
| 9 |
7 8
|
eqnetrd |
|- ( p e. X -> ( X i^i { p } ) =/= (/) ) |
| 10 |
9
|
adantl |
|- ( ( U e. ( UnifOn ` X ) /\ p e. X ) -> ( X i^i { p } ) =/= (/) ) |
| 11 |
|
xpima2 |
|- ( ( X i^i { p } ) =/= (/) -> ( ( X X. X ) " { p } ) = X ) |
| 12 |
10 11
|
syl |
|- ( ( U e. ( UnifOn ` X ) /\ p e. X ) -> ( ( X X. X ) " { p } ) = X ) |
| 13 |
12
|
eqcomd |
|- ( ( U e. ( UnifOn ` X ) /\ p e. X ) -> X = ( ( X X. X ) " { p } ) ) |
| 14 |
|
imaeq1 |
|- ( w = ( X X. X ) -> ( w " { p } ) = ( ( X X. X ) " { p } ) ) |
| 15 |
14
|
rspceeqv |
|- ( ( ( X X. X ) e. U /\ X = ( ( X X. X ) " { p } ) ) -> E. w e. U X = ( w " { p } ) ) |
| 16 |
2 13 15
|
syl2an2r |
|- ( ( U e. ( UnifOn ` X ) /\ p e. X ) -> E. w e. U X = ( w " { p } ) ) |
| 17 |
|
elfvex |
|- ( U e. ( UnifOn ` X ) -> X e. _V ) |
| 18 |
1
|
ustuqtoplem |
|- ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ X e. _V ) -> ( X e. ( N ` p ) <-> E. w e. U X = ( w " { p } ) ) ) |
| 19 |
17 18
|
mpidan |
|- ( ( U e. ( UnifOn ` X ) /\ p e. X ) -> ( X e. ( N ` p ) <-> E. w e. U X = ( w " { p } ) ) ) |
| 20 |
16 19
|
mpbird |
|- ( ( U e. ( UnifOn ` X ) /\ p e. X ) -> X e. ( N ` p ) ) |