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	$⊢ H = ({({1^{st} ↾}_{(V \times V)})}^{-1} \circ (F \circ ({1^{st} ↾}_{(V \times V)}))) \cap ({({2^{nd} ↾}_{(V \times V)})}^{-1} \circ (G \circ ({2^{nd} ↾}_{(V \times V)})))$
	Assertion	fpar	$⊢ (F Fn A \land G Fn B) \to H = (x \in A, y \in B ⟼ ⟨F (x), G (y)⟩)$

Proof

Step	Hyp	Ref	Expression
1		fpar.1	$⊢ H = ({({1^{st} ↾}_{(V \times V)})}^{-1} \circ (F \circ ({1^{st} ↾}_{(V \times V)}))) \cap ({({2^{nd} ↾}_{(V \times V)})}^{-1} \circ (G \circ ({2^{nd} ↾}_{(V \times V)})))$
2		fparlem3	$⊢ F Fn A \to {({1^{st} ↾}_{(V \times V)})}^{-1} \circ (F \circ ({1^{st} ↾}_{(V \times V)})) = ⋃_{x \in A} ((\{x\} \times V) \times (\{F (x)\} \times V))$
3		fparlem4	$⊢ G Fn B \to {({2^{nd} ↾}_{(V \times V)})}^{-1} \circ (G \circ ({2^{nd} ↾}_{(V \times V)})) = ⋃_{y \in B} ((V \times \{y\}) \times (V \times \{G (y)\}))$
4	2 3	ineqan12d	$⊢ (F Fn A \land G Fn B) \to ({({1^{st} ↾}_{(V \times V)})}^{-1} \circ (F \circ ({1^{st} ↾}_{(V \times V)}))) \cap ({({2^{nd} ↾}_{(V \times V)})}^{-1} \circ (G \circ ({2^{nd} ↾}_{(V \times V)}))) = ⋃_{x \in A} ((\{x\} \times V) \times (\{F (x)\} \times V)) \cap ⋃_{y \in B} ((V \times \{y\}) \times (V \times \{G (y)\}))$
5		opex	$⊢ ⟨F (x), G (y)⟩ \in V$
6	5	dfmpo	$⊢ (x \in A, y \in B ⟼ ⟨F (x), G (y)⟩) = ⋃_{x \in A} ⋃_{y \in B} \{⟨⟨x, y⟩, ⟨F (x), G (y)⟩⟩\}$
7		inxp	$⊢ ((\{x\} \times V) \times (\{F (x)\} \times V)) \cap ((V \times \{y\}) \times (V \times \{G (y)\})) = ((\{x\} \times V) \cap (V \times \{y\})) \times ((\{F (x)\} \times V) \cap (V \times \{G (y)\}))$
8		inxp	$⊢ (\{x\} \times V) \cap (V \times \{y\}) = (\{x\} \cap V) \times (V \cap \{y\})$
9		inv1	$⊢ \{x\} \cap V = \{x\}$
10		incom	$⊢ V \cap \{y\} = \{y\} \cap V$
11		inv1	$⊢ \{y\} \cap V = \{y\}$
12	10 11	eqtri	$⊢ V \cap \{y\} = \{y\}$
13	9 12	xpeq12i	$⊢ (\{x\} \cap V) \times (V \cap \{y\}) = \{x\} \times \{y\}$
14		vex	$⊢ x \in V$
15		vex	$⊢ y \in V$
16	14 15	xpsn	$⊢ \{x\} \times \{y\} = \{⟨x, y⟩\}$
17	8 13 16	3eqtri	$⊢ (\{x\} \times V) \cap (V \times \{y\}) = \{⟨x, y⟩\}$
18		inxp	$⊢ (\{F (x)\} \times V) \cap (V \times \{G (y)\}) = (\{F (x)\} \cap V) \times (V \cap \{G (y)\})$
19		inv1	$⊢ \{F (x)\} \cap V = \{F (x)\}$
20		incom	$⊢ V \cap \{G (y)\} = \{G (y)\} \cap V$
21		inv1	$⊢ \{G (y)\} \cap V = \{G (y)\}$
22	20 21	eqtri	$⊢ V \cap \{G (y)\} = \{G (y)\}$
23	19 22	xpeq12i	$⊢ (\{F (x)\} \cap V) \times (V \cap \{G (y)\}) = \{F (x)\} \times \{G (y)\}$
24		fvex	$⊢ F (x) \in V$
25		fvex	$⊢ G (y) \in V$
26	24 25	xpsn	$⊢ \{F (x)\} \times \{G (y)\} = \{⟨F (x), G (y)⟩\}$
27	18 23 26	3eqtri	$⊢ (\{F (x)\} \times V) \cap (V \times \{G (y)\}) = \{⟨F (x), G (y)⟩\}$
28	17 27	xpeq12i	$⊢ ((\{x\} \times V) \cap (V \times \{y\})) \times ((\{F (x)\} \times V) \cap (V \times \{G (y)\})) = \{⟨x, y⟩\} \times \{⟨F (x), G (y)⟩\}$
29		opex	$⊢ ⟨x, y⟩ \in V$
30	29 5	xpsn	$⊢ \{⟨x, y⟩\} \times \{⟨F (x), G (y)⟩\} = \{⟨⟨x, y⟩, ⟨F (x), G (y)⟩⟩\}$
31	7 28 30	3eqtri	$⊢ ((\{x\} \times V) \times (\{F (x)\} \times V)) \cap ((V \times \{y\}) \times (V \times \{G (y)\})) = \{⟨⟨x, y⟩, ⟨F (x), G (y)⟩⟩\}$
32	31	a1i	$⊢ y \in B \to ((\{x\} \times V) \times (\{F (x)\} \times V)) \cap ((V \times \{y\}) \times (V \times \{G (y)\})) = \{⟨⟨x, y⟩, ⟨F (x), G (y)⟩⟩\}$
33	32	iuneq2i	$⊢ ⋃_{y \in B} (((\{x\} \times V) \times (\{F (x)\} \times V)) \cap ((V \times \{y\}) \times (V \times \{G (y)\}))) = ⋃_{y \in B} \{⟨⟨x, y⟩, ⟨F (x), G (y)⟩⟩\}$
34	33	a1i	$⊢ x \in A \to ⋃_{y \in B} (((\{x\} \times V) \times (\{F (x)\} \times V)) \cap ((V \times \{y\}) \times (V \times \{G (y)\}))) = ⋃_{y \in B} \{⟨⟨x, y⟩, ⟨F (x), G (y)⟩⟩\}$
35	34	iuneq2i	$⊢ ⋃_{x \in A} ⋃_{y \in B} (((\{x\} \times V) \times (\{F (x)\} \times V)) \cap ((V \times \{y\}) \times (V \times \{G (y)\}))) = ⋃_{x \in A} ⋃_{y \in B} \{⟨⟨x, y⟩, ⟨F (x), G (y)⟩⟩\}$
36		2iunin	$⊢ ⋃_{x \in A} ⋃_{y \in B} (((\{x\} \times V) \times (\{F (x)\} \times V)) \cap ((V \times \{y\}) \times (V \times \{G (y)\}))) = ⋃_{x \in A} ((\{x\} \times V) \times (\{F (x)\} \times V)) \cap ⋃_{y \in B} ((V \times \{y\}) \times (V \times \{G (y)\}))$
37	6 35 36	3eqtr2i	$⊢ (x \in A, y \in B ⟼ ⟨F (x), G (y)⟩) = ⋃_{x \in A} ((\{x\} \times V) \times (\{F (x)\} \times V)) \cap ⋃_{y \in B} ((V \times \{y\}) \times (V \times \{G (y)\}))$
38	4 1 37	3eqtr4g	$⊢ (F Fn A \land G Fn B) \to H = (x \in A, y \in B ⟼ ⟨F (x), G (y)⟩)$

Metamath Proof Explorer

Theorem fpar

Proof