Is counting permutations really a use of the product property? Suppose you have a set $A=\{1,2,3,4\}$ and we want to count the number of permutations of these elements.  Of course the logic is that you may select one element to be in the first coordinate in four ways.  Having selected it, the next coordinate can be filled with any of the remaining three elements, and so on.  The number of permutations is $4!$.
However, often this is described as an application of the product property for finite sets, $|A\times B|=|A||B|$.  Naturally in this case we would be generalizing it to $$|A_1\times A_2\times A_3\times A_4| = |A_1||A_2||A_3||A_4|$$
But what exactly is set $A_1$ as it is applied here?  If we say that it is $\{1,2,3,4\}$ which I think is the most natural idea, then what is $A_2$?  The second choice is imagined to be made after the first choice has been made, so if we must actually fix $A_2$ before knowing which element is selected, then no particular choice of $A_2$ could be an actual description of what's happening.
I'm not bothered by this, I just want to confirm that my understanding is technically right: If you're being really technical, counting permutations isn't just the product property.  It's more like counting the leaves of the tree

Each set on the second level of the tree is different, representing that a different element had been chosen from the set.  Although the sets are all different, they still each have the same size.  This is why counting "as if" we were using the product property is valid, even though technically there is no one fixed choice of $A_2$.
Or maybe I'm totally wrong and there is a single fixed appropriate choice of $A_2$.  If this really is a direct application of the product property I'd love to be corrected about my understanding.
 A: The idea is not that the set of permutations on $\{1,2,3,4\}$ is a cartesian product of some sets. Instead, you first show that there is a bijection
$$
\{\pi \mid \text{$\pi$ is a permutation on $\{1,2,3,4\}$}\}\longleftrightarrow A_4\times A_3\times A_2\times A_1,
$$
where $A_i$ is a set of size $i$ for each $i\in \{1,2,3,4\}$. To be concrete, say $A_i=\{1,\dots,i\}$. This bijection implies the number of permutations is $|A_4\times A_3\times A_2\times A_1|$. We then apply the Product Property to $A_4\times A_3\times A_2\times A_1|$ to attain $|A_4|\times |A_3|\times |A_2|\times |A_1|$. Therefore, the reason is not just the product principle, but also the existence of this bijection.
What is this bijection? To choose a permutation of $\{1,2,3,4\}$, you need to make a four-way choice, then a three-way choice, then a two-way choice (say, by choosing the elements from left to right). At each point, the choice will be between several numbers in $\{1,2,3,4\}$. Given an element $(i_1,i_2,i_3,i_4)$ of $A_4\times A_3\times A_2\times A_1$, we will choose the $i_1^\text{st}$ smallest number for our first choice, the $i_2^\text{th}$ number for the second choice, and so on. This fully describes the permutation, completing the bijection.
In general, for all problems involving the product principle, you technically need to prove this bijection exists every time. However, this is always routinely the same, and uninteresting, so we never mention it in practice. The entire deduction is just called the Product Principle. This kind of reasoning is pervasive throughout combinatorics.
