Potential proposition:
I am new to studying the measure-theoretic foundations of probability. I think I have come across this result when computing probabilities/expectations.
Let $X, Y$ be independent real-valued random variables on the same probability triple $(\Omega, \mathcal{F}, \mathbb{P})$. Let $F_Y(a) := \mathbb{P}[Y \le a] = \mathbb{P}[ Y^{-1}((-\infty,a]) ]$ denote the CDF of $Y$. Then it holds $\mathbb{E}[ 1_{\{Y \le X\}}\ |\ X] = F_Y \circ X$.
In the above, $1_{\{Y \le X\}}$ denotes the indicator function over the set where $Y \le X$ (I believe this is why $Y$ and $X$ have to be over the same probability triple).
I can understand why this would be true intuitively if we think of expectation as our "best guess" given what we know. To me, it is "clear" that our best guess of what $1_{\{Y \le X\}}$ should be is $F_Y(X)$, given we know what value $X$ is. Again, this is speaking loosely to gain intuition.
My question:
Can anyone please give hints on how to prove this result rigorously, if it is true? I believe the proof should be straight forward, but I cannot seem to figure it out.
I would be happy with a proof that uses any of the equivalent definitions of conditional expectation. However, I am most familiar with the Radon-Nikodym definition of where $\mathbb{E}[ 1_{\{Y \le X\}}\ |\ X]$ is defined to be the (a.s.) unique $\sigma(X)$-measurable random variable such that $$ \int_A \mathbb{E}[ 1_{\{Y \le X\}}\ |\ X]\ d\mathbb{P} = \int_A 1_{\{Y \le X\}}\ d\mathbb{P} \qquad \forall A \in \sigma(X). $$ So, a proof using this definition would be extra helpful, if possible.
Also, I should add that I am not sure if independence of $X$ or $Y$ is required or not.
My attempt so far:
Fix $B \subseteq \mathbb{R}$ Borel-measurable and let $A := X^{-1}(B)$. My goal is to show that $$ \int_A F_Y \circ X\ d\mathbb{P} = \int_A 1_{\{Y \le X\}}\ d\mathbb{P}. $$ I first observe that for any $a \in \Omega$, we have $$ F_Y \circ X(a) = \mathbb{P}\left[ Y^{-1}\left( (-\infty, X(a)] \right) \right] = \int_\Omega 1_{\{Y \le X(a)\}}(\omega)\ d\mathbb{P}(\omega). $$ In turn, we have $$ \int_A F_Y \circ X(a)\ d\mathbb{P}(a) = \int_A \int_\Omega 1_{\{Y \le X(a)\}}(\omega)\ d\mathbb{P}(\omega)\ d\mathbb{P}(a). $$ So, we would be done if we can show $$ \int_A \int_\Omega 1_{\{Y \le X(a)\}}(\omega)\ d\mathbb{P}(\omega)\ d\mathbb{P}(a) = \int_A 1_{\{Y \le X\}}(a)\ d\mathbb{P}(a). $$ However, I have been unsuccessful in establishing this equality. In particular, I have tried to use Fubini-Tonelli and I have also tried to show that $a \mapsto \int_\Omega 1_{\{Y \le X(a)\}}(\omega)\ d\mathbb{P}(\omega)$ equals (as a function) $a \mapsto 1_{\{Y \le X\}}(a)$.
I suspect maybe I should use independence at this point, but I am not sure. Thanks for any help!