Description: Lemma 2 for funcestrcsetc . (Contributed by AV, 22-Mar-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | funcestrcsetc.e | |- E = ( ExtStrCat ` U ) |
|
funcestrcsetc.s | |- S = ( SetCat ` U ) |
||
funcestrcsetc.b | |- B = ( Base ` E ) |
||
funcestrcsetc.c | |- C = ( Base ` S ) |
||
funcestrcsetc.u | |- ( ph -> U e. WUni ) |
||
funcestrcsetc.f | |- ( ph -> F = ( x e. B |-> ( Base ` x ) ) ) |
||
Assertion | funcestrcsetclem2 | |- ( ( ph /\ X e. B ) -> ( F ` X ) e. U ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | funcestrcsetc.e | |- E = ( ExtStrCat ` U ) |
|
2 | funcestrcsetc.s | |- S = ( SetCat ` U ) |
|
3 | funcestrcsetc.b | |- B = ( Base ` E ) |
|
4 | funcestrcsetc.c | |- C = ( Base ` S ) |
|
5 | funcestrcsetc.u | |- ( ph -> U e. WUni ) |
|
6 | funcestrcsetc.f | |- ( ph -> F = ( x e. B |-> ( Base ` x ) ) ) |
|
7 | 1 2 3 4 5 6 | funcestrcsetclem1 | |- ( ( ph /\ X e. B ) -> ( F ` X ) = ( Base ` X ) ) |
8 | 1 3 5 | estrcbasbas | |- ( ( ph /\ X e. B ) -> ( Base ` X ) e. U ) |
9 | 7 8 | eqeltrd | |- ( ( ph /\ X e. B ) -> ( F ` X ) e. U ) |