I want to prove that for $f:A\times B\rightarrow \{ 0,1\}$ it holds that $\min(\min(f(a,b):b\in B):a\in A) = min(f(a,b):a\in A, b\in B)$
I am new to FO-Semantics and want to know how to read $\min(\min(f(a,b):b\in B):a\in A)$.
My question is if $ a $ on the left side of the equation is also known within the nested $\min()$ for function $f(a,b)$ or has it to be treated as a variable.
Is it allowed to write it as: If $f(a,b)= 0$ where $a=1$ and $b=0$, then $\min(\min(f(1,0))=\min(0)= 0 = \min(f(1,0))$
Thanks in advance.
It is not clear that your real question has anything to do with first-order logic.
Firstly, it is not really standard to write "$\min( \cdots : \cdots )$", though it could be treated as short-hand for "$\min( \{ \cdots : \cdots \})$", namely the minimum of some set under its natural/given ordering. If you want to be even more precise, you need to specify that ordered structure, such as "$\min_\mathbb{N}( \{ \cdots : \cdots \})$".
So to answer your question:
Yes, because the expression is to be treated as "$\min(\{\min(\{f(a,b):b \in B\}):a \in A\})$". As you can see, for each $a \in A$ we have the set $\{f(a,b):b \in B\}$ (which refers to exactly that $a$), and you take its minimum, and the expression is the minimum of all those minimums.