Theorem ucnimalem

Description: Reformulate the G function as a mapping with one variable. (Contributed by Thierry Arnoux, 19-Nov-2017)

	Ref	Expression
Hypotheses	ucnprima.1	$$⊢\phi \to U\in \mathrm{UnifOn}\left(X\right)$$
	ucnprima.2	$$⊢\phi \to V\in \mathrm{UnifOn}\left(Y\right)$$
	ucnprima.3	$$⊢\phi \to F\in \left(U\mathrm{uCn}V\right)$$
	ucnprima.4	$$⊢\phi \to W\in V$$
	ucnprima.5	$$⊢G=\left(x\in X,y\in X⟼⟨F\left(x\right),F\left(y\right)⟩\right)$$
Assertion	ucnimalem	$$⊢G=\left(p\in \left(X\times X\right)⟼⟨F\left(1^{st}\left(p\right)\right),F\left(2^{nd}\left(p\right)\right)⟩\right)$$

Proof

Step	Hyp	Ref	Expression
1		ucnprima.1	$$⊢\phi \to U\in \mathrm{UnifOn}\left(X\right)$$
2		ucnprima.2	$$⊢\phi \to V\in \mathrm{UnifOn}\left(Y\right)$$
3		ucnprima.3	$$⊢\phi \to F\in \left(U\mathrm{uCn}V\right)$$
4		ucnprima.4	$$⊢\phi \to W\in V$$
5		ucnprima.5	$$⊢G=\left(x\in X,y\in X⟼⟨F\left(x\right),F\left(y\right)⟩\right)$$
6		vex	$$⊢x\in \mathrm{V}$$
7		vex	$$⊢y\in \mathrm{V}$$
8	6 7	op1std	$$⊢p=⟨x,y⟩\to 1^{st}\left(p\right)=x$$
9	8	fveq2d	$$⊢p=⟨x,y⟩\to F\left(1^{st}\left(p\right)\right)=F\left(x\right)$$
10	6 7	op2ndd	$$⊢p=⟨x,y⟩\to 2^{nd}\left(p\right)=y$$
11	10	fveq2d	$$⊢p=⟨x,y⟩\to F\left(2^{nd}\left(p\right)\right)=F\left(y\right)$$
12	9 11	opeq12d	$$⊢p=⟨x,y⟩\to ⟨F\left(1^{st}\left(p\right)\right),F\left(2^{nd}\left(p\right)\right)⟩=⟨F\left(x\right),F\left(y\right)⟩$$
13	12	mpompt	$$⊢\left(p\in \left(X\times X\right)⟼⟨F\left(1^{st}\left(p\right)\right),F\left(2^{nd}\left(p\right)\right)⟩\right)=\left(x\in X,y\in X⟼⟨F\left(x\right),F\left(y\right)⟩\right)$$
14	5 13	eqtr4i	$$⊢G=\left(p\in \left(X\times X\right)⟼⟨F\left(1^{st}\left(p\right)\right),F\left(2^{nd}\left(p\right)\right)⟩\right)$$