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

Metamath Proof Explorer

Theorem fpar

Description: Merge two functions in parallel. Use as the second argument of a composition with a binary operation to build compound functions such as ( x e. ( 0 [,) +oo ) , y e. RR |-> ( ( sqrtx ) + ( siny ) ) ) , see also ex-fpar . (Contributed by NM, 17-Sep-2007) (Proof shortened by Mario Carneiro, 28-Apr-2015)

Ref Expression
Hypothesis fpar.1 ⊢ 𝐻 = ( ( ◡ ( 1st ↾ ( V × V ) ) ∘ ( 𝐹 ∘ ( 1st ↾ ( V × V ) ) ) ) ∩ ( ◡ ( 2nd ↾ ( V × V ) ) ∘ ( 𝐺 ∘ ( 2nd ↾ ( V × V ) ) ) ) )
Assertion fpar ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) → 𝐻 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑦 ) ⟩ ) )

Proof

Step Hyp Ref Expression
1 fpar.1 ⊢ 𝐻 = ( ( ◡ ( 1st ↾ ( V × V ) ) ∘ ( 𝐹 ∘ ( 1st ↾ ( V × V ) ) ) ) ∩ ( ◡ ( 2nd ↾ ( V × V ) ) ∘ ( 𝐺 ∘ ( 2nd ↾ ( V × V ) ) ) ) )
2 fparlem3 ⊢ ( 𝐹 Fn 𝐴 → ( ◡ ( 1st ↾ ( V × V ) ) ∘ ( 𝐹 ∘ ( 1st ↾ ( V × V ) ) ) ) = ∪ 𝑥 ∈ 𝐴 ( ( { 𝑥 } × V ) × ( { ( 𝐹 ‘ 𝑥 ) } × V ) ) )
3 fparlem4 ⊢ ( 𝐺 Fn 𝐵 → ( ◡ ( 2nd ↾ ( V × V ) ) ∘ ( 𝐺 ∘ ( 2nd ↾ ( V × V ) ) ) ) = ∪ 𝑦 ∈ 𝐵 ( ( V × { 𝑦 } ) × ( V × { ( 𝐺 ‘ 𝑦 ) } ) ) )
4 2 3 ineqan12d ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) → ( ( ◡ ( 1st ↾ ( V × V ) ) ∘ ( 𝐹 ∘ ( 1st ↾ ( V × V ) ) ) ) ∩ ( ◡ ( 2nd ↾ ( V × V ) ) ∘ ( 𝐺 ∘ ( 2nd ↾ ( V × V ) ) ) ) ) = ( ∪ 𝑥 ∈ 𝐴 ( ( { 𝑥 } × V ) × ( { ( 𝐹 ‘ 𝑥 ) } × V ) ) ∩ ∪ 𝑦 ∈ 𝐵 ( ( V × { 𝑦 } ) × ( V × { ( 𝐺 ‘ 𝑦 ) } ) ) ) )
5 opex ⊢ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑦 ) ⟩ ∈ V
6 5 dfmpo ⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑦 ) ⟩ ) = ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑦 ) ⟩ ⟩ }
7 inxp ⊢ ( ( ( { 𝑥 } × V ) × ( { ( 𝐹 ‘ 𝑥 ) } × V ) ) ∩ ( ( V × { 𝑦 } ) × ( V × { ( 𝐺 ‘ 𝑦 ) } ) ) ) = ( ( ( { 𝑥 } × V ) ∩ ( V × { 𝑦 } ) ) × ( ( { ( 𝐹 ‘ 𝑥 ) } × V ) ∩ ( V × { ( 𝐺 ‘ 𝑦 ) } ) ) )
8 inxp ⊢ ( ( { 𝑥 } × V ) ∩ ( V × { 𝑦 } ) ) = ( ( { 𝑥 } ∩ V ) × ( V ∩ { 𝑦 } ) )
9 inv1 ⊢ ( { 𝑥 } ∩ V ) = { 𝑥 }
10 incom ⊢ ( V ∩ { 𝑦 } ) = ( { 𝑦 } ∩ V )
11 inv1 ⊢ ( { 𝑦 } ∩ V ) = { 𝑦 }
12 10 11 eqtri ⊢ ( V ∩ { 𝑦 } ) = { 𝑦 }
13 9 12 xpeq12i ⊢ ( ( { 𝑥 } ∩ V ) × ( V ∩ { 𝑦 } ) ) = ( { 𝑥 } × { 𝑦 } )
14 vex ⊢ 𝑥 ∈ V
15 vex ⊢ 𝑦 ∈ V
16 14 15 xpsn ⊢ ( { 𝑥 } × { 𝑦 } ) = { ⟨ 𝑥 , 𝑦 ⟩ }
17 8 13 16 3eqtri ⊢ ( ( { 𝑥 } × V ) ∩ ( V × { 𝑦 } ) ) = { ⟨ 𝑥 , 𝑦 ⟩ }
18 inxp ⊢ ( ( { ( 𝐹 ‘ 𝑥 ) } × V ) ∩ ( V × { ( 𝐺 ‘ 𝑦 ) } ) ) = ( ( { ( 𝐹 ‘ 𝑥 ) } ∩ V ) × ( V ∩ { ( 𝐺 ‘ 𝑦 ) } ) )
19 inv1 ⊢ ( { ( 𝐹 ‘ 𝑥 ) } ∩ V ) = { ( 𝐹 ‘ 𝑥 ) }
20 incom ⊢ ( V ∩ { ( 𝐺 ‘ 𝑦 ) } ) = ( { ( 𝐺 ‘ 𝑦 ) } ∩ V )
21 inv1 ⊢ ( { ( 𝐺 ‘ 𝑦 ) } ∩ V ) = { ( 𝐺 ‘ 𝑦 ) }
22 20 21 eqtri ⊢ ( V ∩ { ( 𝐺 ‘ 𝑦 ) } ) = { ( 𝐺 ‘ 𝑦 ) }
23 19 22 xpeq12i ⊢ ( ( { ( 𝐹 ‘ 𝑥 ) } ∩ V ) × ( V ∩ { ( 𝐺 ‘ 𝑦 ) } ) ) = ( { ( 𝐹 ‘ 𝑥 ) } × { ( 𝐺 ‘ 𝑦 ) } )
24 fvex ⊢ ( 𝐹 ‘ 𝑥 ) ∈ V
25 fvex ⊢ ( 𝐺 ‘ 𝑦 ) ∈ V
26 24 25 xpsn ⊢ ( { ( 𝐹 ‘ 𝑥 ) } × { ( 𝐺 ‘ 𝑦 ) } ) = { ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑦 ) ⟩ }
27 18 23 26 3eqtri ⊢ ( ( { ( 𝐹 ‘ 𝑥 ) } × V ) ∩ ( V × { ( 𝐺 ‘ 𝑦 ) } ) ) = { ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑦 ) ⟩ }
28 17 27 xpeq12i ⊢ ( ( ( { 𝑥 } × V ) ∩ ( V × { 𝑦 } ) ) × ( ( { ( 𝐹 ‘ 𝑥 ) } × V ) ∩ ( V × { ( 𝐺 ‘ 𝑦 ) } ) ) ) = ( { ⟨ 𝑥 , 𝑦 ⟩ } × { ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑦 ) ⟩ } )
29 opex ⊢ ⟨ 𝑥 , 𝑦 ⟩ ∈ V
30 29 5 xpsn ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ } × { ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑦 ) ⟩ } ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑦 ) ⟩ ⟩ }
31 7 28 30 3eqtri ⊢ ( ( ( { 𝑥 } × V ) × ( { ( 𝐹 ‘ 𝑥 ) } × V ) ) ∩ ( ( V × { 𝑦 } ) × ( V × { ( 𝐺 ‘ 𝑦 ) } ) ) ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑦 ) ⟩ ⟩ }
32 31 a1i ⊢ ( 𝑦 ∈ 𝐵 → ( ( ( { 𝑥 } × V ) × ( { ( 𝐹 ‘ 𝑥 ) } × V ) ) ∩ ( ( V × { 𝑦 } ) × ( V × { ( 𝐺 ‘ 𝑦 ) } ) ) ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑦 ) ⟩ ⟩ } )
33 32 iuneq2i ⊢ ∪ 𝑦 ∈ 𝐵 ( ( ( { 𝑥 } × V ) × ( { ( 𝐹 ‘ 𝑥 ) } × V ) ) ∩ ( ( V × { 𝑦 } ) × ( V × { ( 𝐺 ‘ 𝑦 ) } ) ) ) = ∪ 𝑦 ∈ 𝐵 { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑦 ) ⟩ ⟩ }
34 33 a1i ⊢ ( 𝑥 ∈ 𝐴 → ∪ 𝑦 ∈ 𝐵 ( ( ( { 𝑥 } × V ) × ( { ( 𝐹 ‘ 𝑥 ) } × V ) ) ∩ ( ( V × { 𝑦 } ) × ( V × { ( 𝐺 ‘ 𝑦 ) } ) ) ) = ∪ 𝑦 ∈ 𝐵 { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑦 ) ⟩ ⟩ } )
35 34 iuneq2i ⊢ ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 ( ( ( { 𝑥 } × V ) × ( { ( 𝐹 ‘ 𝑥 ) } × V ) ) ∩ ( ( V × { 𝑦 } ) × ( V × { ( 𝐺 ‘ 𝑦 ) } ) ) ) = ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑦 ) ⟩ ⟩ }
36 2iunin ⊢ ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 ( ( ( { 𝑥 } × V ) × ( { ( 𝐹 ‘ 𝑥 ) } × V ) ) ∩ ( ( V × { 𝑦 } ) × ( V × { ( 𝐺 ‘ 𝑦 ) } ) ) ) = ( ∪ 𝑥 ∈ 𝐴 ( ( { 𝑥 } × V ) × ( { ( 𝐹 ‘ 𝑥 ) } × V ) ) ∩ ∪ 𝑦 ∈ 𝐵 ( ( V × { 𝑦 } ) × ( V × { ( 𝐺 ‘ 𝑦 ) } ) ) )
37 6 35 36 3eqtr2i ⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑦 ) ⟩ ) = ( ∪ 𝑥 ∈ 𝐴 ( ( { 𝑥 } × V ) × ( { ( 𝐹 ‘ 𝑥 ) } × V ) ) ∩ ∪ 𝑦 ∈ 𝐵 ( ( V × { 𝑦 } ) × ( V × { ( 𝐺 ‘ 𝑦 ) } ) ) )
38 4 1 37 3eqtr4g ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) → 𝐻 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑦 ) ⟩ ) )