Step |
Hyp |
Ref |
Expression |
1 |
|
vex |
|- y e. _V |
2 |
1
|
inex1 |
|- ( y i^i A ) e. _V |
3 |
|
ineq1 |
|- ( x = ( y i^i A ) -> ( x i^i B ) = ( ( y i^i A ) i^i B ) ) |
4 |
|
inass |
|- ( ( y i^i A ) i^i B ) = ( y i^i ( A i^i B ) ) |
5 |
3 4
|
eqtrdi |
|- ( x = ( y i^i A ) -> ( x i^i B ) = ( y i^i ( A i^i B ) ) ) |
6 |
2 5
|
abrexco |
|- { z | E. x e. { w | E. y e. J w = ( y i^i A ) } z = ( x i^i B ) } = { z | E. y e. J z = ( y i^i ( A i^i B ) ) } |
7 |
|
eqid |
|- ( y e. J |-> ( y i^i A ) ) = ( y e. J |-> ( y i^i A ) ) |
8 |
7
|
rnmpt |
|- ran ( y e. J |-> ( y i^i A ) ) = { w | E. y e. J w = ( y i^i A ) } |
9 |
8
|
mpteq1i |
|- ( x e. ran ( y e. J |-> ( y i^i A ) ) |-> ( x i^i B ) ) = ( x e. { w | E. y e. J w = ( y i^i A ) } |-> ( x i^i B ) ) |
10 |
9
|
rnmpt |
|- ran ( x e. ran ( y e. J |-> ( y i^i A ) ) |-> ( x i^i B ) ) = { z | E. x e. { w | E. y e. J w = ( y i^i A ) } z = ( x i^i B ) } |
11 |
|
eqid |
|- ( y e. J |-> ( y i^i ( A i^i B ) ) ) = ( y e. J |-> ( y i^i ( A i^i B ) ) ) |
12 |
11
|
rnmpt |
|- ran ( y e. J |-> ( y i^i ( A i^i B ) ) ) = { z | E. y e. J z = ( y i^i ( A i^i B ) ) } |
13 |
6 10 12
|
3eqtr4i |
|- ran ( x e. ran ( y e. J |-> ( y i^i A ) ) |-> ( x i^i B ) ) = ran ( y e. J |-> ( y i^i ( A i^i B ) ) ) |
14 |
|
restval |
|- ( ( J e. V /\ A e. W ) -> ( J |`t A ) = ran ( y e. J |-> ( y i^i A ) ) ) |
15 |
14
|
3adant3 |
|- ( ( J e. V /\ A e. W /\ B e. X ) -> ( J |`t A ) = ran ( y e. J |-> ( y i^i A ) ) ) |
16 |
15
|
oveq1d |
|- ( ( J e. V /\ A e. W /\ B e. X ) -> ( ( J |`t A ) |`t B ) = ( ran ( y e. J |-> ( y i^i A ) ) |`t B ) ) |
17 |
|
ovex |
|- ( J |`t A ) e. _V |
18 |
15 17
|
eqeltrrdi |
|- ( ( J e. V /\ A e. W /\ B e. X ) -> ran ( y e. J |-> ( y i^i A ) ) e. _V ) |
19 |
|
simp3 |
|- ( ( J e. V /\ A e. W /\ B e. X ) -> B e. X ) |
20 |
|
restval |
|- ( ( ran ( y e. J |-> ( y i^i A ) ) e. _V /\ B e. X ) -> ( ran ( y e. J |-> ( y i^i A ) ) |`t B ) = ran ( x e. ran ( y e. J |-> ( y i^i A ) ) |-> ( x i^i B ) ) ) |
21 |
18 19 20
|
syl2anc |
|- ( ( J e. V /\ A e. W /\ B e. X ) -> ( ran ( y e. J |-> ( y i^i A ) ) |`t B ) = ran ( x e. ran ( y e. J |-> ( y i^i A ) ) |-> ( x i^i B ) ) ) |
22 |
16 21
|
eqtrd |
|- ( ( J e. V /\ A e. W /\ B e. X ) -> ( ( J |`t A ) |`t B ) = ran ( x e. ran ( y e. J |-> ( y i^i A ) ) |-> ( x i^i B ) ) ) |
23 |
|
simp1 |
|- ( ( J e. V /\ A e. W /\ B e. X ) -> J e. V ) |
24 |
|
inex1g |
|- ( A e. W -> ( A i^i B ) e. _V ) |
25 |
24
|
3ad2ant2 |
|- ( ( J e. V /\ A e. W /\ B e. X ) -> ( A i^i B ) e. _V ) |
26 |
|
restval |
|- ( ( J e. V /\ ( A i^i B ) e. _V ) -> ( J |`t ( A i^i B ) ) = ran ( y e. J |-> ( y i^i ( A i^i B ) ) ) ) |
27 |
23 25 26
|
syl2anc |
|- ( ( J e. V /\ A e. W /\ B e. X ) -> ( J |`t ( A i^i B ) ) = ran ( y e. J |-> ( y i^i ( A i^i B ) ) ) ) |
28 |
13 22 27
|
3eqtr4a |
|- ( ( J e. V /\ A e. W /\ B e. X ) -> ( ( J |`t A ) |`t B ) = ( J |`t ( A i^i B ) ) ) |