This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑝 ) ) ⟩ )