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 ⊢ φ → U ∈ UnifOn ⁡ X
ucnprima.2 ⊢ φ → V ∈ UnifOn ⁡ Y
ucnprima.3 ⊢ φ → F ∈ U uCn V
ucnprima.4 ⊢ φ → W ∈ V
ucnprima.5 ⊢ G = x ∈ X , y ∈ X ⟼ F ⁡ x F ⁡ y
Assertion ucnimalem ⊢ G = p ∈ X × X ⟼ F ⁡ 1 st ⁡ p F ⁡ 2 nd ⁡ p

Proof

Step Hyp Ref Expression
1 ucnprima.1 ⊢ φ → U ∈ UnifOn ⁡ X
2 ucnprima.2 ⊢ φ → V ∈ UnifOn ⁡ Y
3 ucnprima.3 ⊢ φ → F ∈ U uCn V
4 ucnprima.4 ⊢ φ → W ∈ V
5 ucnprima.5 ⊢ G = x ∈ X , y ∈ X ⟼ F ⁡ x F ⁡ y
6 vex ⊢ x ∈ V
7 vex ⊢ y ∈ V
8 6 7 op1std ⊢ p = x y → 1 st ⁡ p = x
9 8 fveq2d ⊢ p = x y → F ⁡ 1 st ⁡ p = F ⁡ x
10 6 7 op2ndd ⊢ p = x y → 2 nd ⁡ p = y
11 10 fveq2d ⊢ p = x y → F ⁡ 2 nd ⁡ p = F ⁡ y
12 9 11 opeq12d ⊢ p = x y → F ⁡ 1 st ⁡ p F ⁡ 2 nd ⁡ p = F ⁡ x F ⁡ y
13 12 mpompt ⊢ p ∈ X × X ⟼ F ⁡ 1 st ⁡ p F ⁡ 2 nd ⁡ p = x ∈ X , y ∈ X ⟼ F ⁡ x F ⁡ y
14 5 13 eqtr4i ⊢ G = p ∈ X × X ⟼ F ⁡ 1 st ⁡ p F ⁡ 2 nd ⁡ p