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	⊢ ( 𝜑 → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
	ucnprima.2	⊢ ( 𝜑 → 𝑉 ∈ ( UnifOn ‘ 𝑌 ) )
	ucnprima.3	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑈 Cnu 𝑉 ) )
	ucnprima.4	⊢ ( 𝜑 → 𝑊 ∈ 𝑉 )
	ucnprima.5	⊢ 𝐺 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ )
Assertion	ucnimalem	⊢ 𝐺 = ( 𝑝 ∈ ( 𝑋 × 𝑋 ) ↦ ⟨ ( 𝐹 ‘ ( 1st ‘ 𝑝 ) ) , ( 𝐹 ‘ ( 2nd ‘ 𝑝 ) ) ⟩ )

Proof

Step	Hyp	Ref	Expression
1		ucnprima.1	⊢ ( 𝜑 → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
2		ucnprima.2	⊢ ( 𝜑 → 𝑉 ∈ ( UnifOn ‘ 𝑌 ) )
3		ucnprima.3	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑈 Cnu 𝑉 ) )
4		ucnprima.4	⊢ ( 𝜑 → 𝑊 ∈ 𝑉 )
5		ucnprima.5	⊢ 𝐺 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ )
6		vex	⊢ 𝑥 ∈ V
7		vex	⊢ 𝑦 ∈ V
8	6 7	op1std	⊢ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ( 1st ‘ 𝑝 ) = 𝑥 )
9	8	fveq2d	⊢ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐹 ‘ ( 1st ‘ 𝑝 ) ) = ( 𝐹 ‘ 𝑥 ) )
10	6 7	op2ndd	⊢ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ( 2nd ‘ 𝑝 ) = 𝑦 )
11	10	fveq2d	⊢ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐹 ‘ ( 2nd ‘ 𝑝 ) ) = ( 𝐹 ‘ 𝑦 ) )
12	9 11	opeq12d	⊢ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ⟨ ( 𝐹 ‘ ( 1st ‘ 𝑝 ) ) , ( 𝐹 ‘ ( 2nd ‘ 𝑝 ) ) ⟩ = ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ )
13	12	mpompt	⊢ ( 𝑝 ∈ ( 𝑋 × 𝑋 ) ↦ ⟨ ( 𝐹 ‘ ( 1st ‘ 𝑝 ) ) , ( 𝐹 ‘ ( 2nd ‘ 𝑝 ) ) ⟩ ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ )
14	5 13	eqtr4i	⊢ 𝐺 = ( 𝑝 ∈ ( 𝑋 × 𝑋 ) ↦ ⟨ ( 𝐹 ‘ ( 1st ‘ 𝑝 ) ) , ( 𝐹 ‘ ( 2nd ‘ 𝑝 ) ) ⟩ )