| Step |
Hyp |
Ref |
Expression |
| 1 |
|
funcsetcestrc.s |
|- S = ( SetCat ` U ) |
| 2 |
|
funcsetcestrc.c |
|- C = ( Base ` S ) |
| 3 |
|
funcsetcestrc.f |
|- ( ph -> F = ( x e. C |-> { <. ( Base ` ndx ) , x >. } ) ) |
| 4 |
3
|
adantr |
|- ( ( ph /\ X e. C ) -> F = ( x e. C |-> { <. ( Base ` ndx ) , x >. } ) ) |
| 5 |
|
opeq2 |
|- ( x = X -> <. ( Base ` ndx ) , x >. = <. ( Base ` ndx ) , X >. ) |
| 6 |
5
|
sneqd |
|- ( x = X -> { <. ( Base ` ndx ) , x >. } = { <. ( Base ` ndx ) , X >. } ) |
| 7 |
6
|
adantl |
|- ( ( ( ph /\ X e. C ) /\ x = X ) -> { <. ( Base ` ndx ) , x >. } = { <. ( Base ` ndx ) , X >. } ) |
| 8 |
|
simpr |
|- ( ( ph /\ X e. C ) -> X e. C ) |
| 9 |
|
snex |
|- { <. ( Base ` ndx ) , X >. } e. _V |
| 10 |
9
|
a1i |
|- ( ( ph /\ X e. C ) -> { <. ( Base ` ndx ) , X >. } e. _V ) |
| 11 |
4 7 8 10
|
fvmptd |
|- ( ( ph /\ X e. C ) -> ( F ` X ) = { <. ( Base ` ndx ) , X >. } ) |