Step |
Hyp |
Ref |
Expression |
1 |
|
cntzmhm.z |
|- Z = ( Cntz ` G ) |
2 |
|
cntzmhm.y |
|- Y = ( Cntz ` H ) |
3 |
1 2
|
cntzmhm |
|- ( ( F e. ( G MndHom H ) /\ x e. ( Z ` T ) ) -> ( F ` x ) e. ( Y ` ( F " T ) ) ) |
4 |
3
|
ralrimiva |
|- ( F e. ( G MndHom H ) -> A. x e. ( Z ` T ) ( F ` x ) e. ( Y ` ( F " T ) ) ) |
5 |
|
ssralv |
|- ( S C_ ( Z ` T ) -> ( A. x e. ( Z ` T ) ( F ` x ) e. ( Y ` ( F " T ) ) -> A. x e. S ( F ` x ) e. ( Y ` ( F " T ) ) ) ) |
6 |
4 5
|
mpan9 |
|- ( ( F e. ( G MndHom H ) /\ S C_ ( Z ` T ) ) -> A. x e. S ( F ` x ) e. ( Y ` ( F " T ) ) ) |
7 |
|
eqid |
|- ( Base ` G ) = ( Base ` G ) |
8 |
|
eqid |
|- ( Base ` H ) = ( Base ` H ) |
9 |
7 8
|
mhmf |
|- ( F e. ( G MndHom H ) -> F : ( Base ` G ) --> ( Base ` H ) ) |
10 |
9
|
adantr |
|- ( ( F e. ( G MndHom H ) /\ S C_ ( Z ` T ) ) -> F : ( Base ` G ) --> ( Base ` H ) ) |
11 |
10
|
ffund |
|- ( ( F e. ( G MndHom H ) /\ S C_ ( Z ` T ) ) -> Fun F ) |
12 |
|
simpr |
|- ( ( F e. ( G MndHom H ) /\ S C_ ( Z ` T ) ) -> S C_ ( Z ` T ) ) |
13 |
7 1
|
cntzssv |
|- ( Z ` T ) C_ ( Base ` G ) |
14 |
12 13
|
sstrdi |
|- ( ( F e. ( G MndHom H ) /\ S C_ ( Z ` T ) ) -> S C_ ( Base ` G ) ) |
15 |
10
|
fdmd |
|- ( ( F e. ( G MndHom H ) /\ S C_ ( Z ` T ) ) -> dom F = ( Base ` G ) ) |
16 |
14 15
|
sseqtrrd |
|- ( ( F e. ( G MndHom H ) /\ S C_ ( Z ` T ) ) -> S C_ dom F ) |
17 |
|
funimass4 |
|- ( ( Fun F /\ S C_ dom F ) -> ( ( F " S ) C_ ( Y ` ( F " T ) ) <-> A. x e. S ( F ` x ) e. ( Y ` ( F " T ) ) ) ) |
18 |
11 16 17
|
syl2anc |
|- ( ( F e. ( G MndHom H ) /\ S C_ ( Z ` T ) ) -> ( ( F " S ) C_ ( Y ` ( F " T ) ) <-> A. x e. S ( F ` x ) e. ( Y ` ( F " T ) ) ) ) |
19 |
6 18
|
mpbird |
|- ( ( F e. ( G MndHom H ) /\ S C_ ( Z ` T ) ) -> ( F " S ) C_ ( Y ` ( F " T ) ) ) |