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 𝐵 ) → 𝐻 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑦 ) ⟩ ) )