Description: Lemma 2 for funcringcsetcALTV . (Contributed by AV, 15-Feb-2020) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | funcringcsetcALTV.r | |- R = ( RingCatALTV ` U ) |
|
funcringcsetcALTV.s | |- S = ( SetCat ` U ) |
||
funcringcsetcALTV.b | |- B = ( Base ` R ) |
||
funcringcsetcALTV.c | |- C = ( Base ` S ) |
||
funcringcsetcALTV.u | |- ( ph -> U e. WUni ) |
||
funcringcsetcALTV.f | |- ( ph -> F = ( x e. B |-> ( Base ` x ) ) ) |
||
Assertion | funcringcsetclem2ALTV | |- ( ( ph /\ X e. B ) -> ( F ` X ) e. U ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | funcringcsetcALTV.r | |- R = ( RingCatALTV ` U ) |
|
2 | funcringcsetcALTV.s | |- S = ( SetCat ` U ) |
|
3 | funcringcsetcALTV.b | |- B = ( Base ` R ) |
|
4 | funcringcsetcALTV.c | |- C = ( Base ` S ) |
|
5 | funcringcsetcALTV.u | |- ( ph -> U e. WUni ) |
|
6 | funcringcsetcALTV.f | |- ( ph -> F = ( x e. B |-> ( Base ` x ) ) ) |
|
7 | 1 2 3 4 5 6 | funcringcsetclem1ALTV | |- ( ( ph /\ X e. B ) -> ( F ` X ) = ( Base ` X ) ) |
8 | 1 3 5 | ringcbasbasALTV | |- ( ( ph /\ X e. B ) -> ( Base ` X ) e. U ) |
9 | 7 8 | eqeltrd | |- ( ( ph /\ X e. B ) -> ( F ` X ) e. U ) |