dfco2a

Description: Generalization of dfco2 , where C can have any value between dom A i^i ran B and _V . (Contributed by NM, 21-Dec-2008) (Proof shortened by Andrew Salmon, 27-Aug-2011)

		Ref	Expression
	Assertion	dfco2a	$⊢ dom A \cap ran B \subseteq C \to A \circ B = ⋃_{x \in C} (B^{-1} [\{x\}] \times A [\{x\}])$

Proof

Step	Hyp	Ref	Expression
1		dfco2	$⊢ A \circ B = ⋃_{x \in V} (B^{-1} [\{x\}] \times A [\{x\}])$
2		vex	$⊢ z \in V$
3	2	eliniseg	$⊢ x \in V \to (z \in B^{-1} [\{x\}] \leftrightarrow z B x)$
4	3	elv	$⊢ z \in B^{-1} [\{x\}] \leftrightarrow z B x$
5		vex	$⊢ x \in V$
6	2 5	brelrn	$⊢ z B x \to x \in ran B$
7	4 6	sylbi	$⊢ z \in B^{-1} [\{x\}] \to x \in ran B$
8		vex	$⊢ w \in V$
9	5 8	elimasn	$⊢ w \in A [\{x\}] \leftrightarrow ⟨x, w⟩ \in A$
10	5 8	opeldm	$⊢ ⟨x, w⟩ \in A \to x \in dom A$
11	9 10	sylbi	$⊢ w \in A [\{x\}] \to x \in dom A$
12	7 11	anim12ci	$⊢ (z \in B^{-1} [\{x\}] \land w \in A [\{x\}]) \to (x \in dom A \land x \in ran B)$
13	12	adantl	$⊢ (y = ⟨z, w⟩ \land (z \in B^{-1} [\{x\}] \land w \in A [\{x\}])) \to (x \in dom A \land x \in ran B)$
14	13	exlimivv	$⊢ \exists z \exists w (y = ⟨z, w⟩ \land (z \in B^{-1} [\{x\}] \land w \in A [\{x\}])) \to (x \in dom A \land x \in ran B)$
15		elxp	$⊢ y \in (B^{-1} [\{x\}] \times A [\{x\}]) \leftrightarrow \exists z \exists w (y = ⟨z, w⟩ \land (z \in B^{-1} [\{x\}] \land w \in A [\{x\}]))$
16		elin	$⊢ x \in (dom A \cap ran B) \leftrightarrow (x \in dom A \land x \in ran B)$
17	14 15 16	3imtr4i	$⊢ y \in (B^{-1} [\{x\}] \times A [\{x\}]) \to x \in (dom A \cap ran B)$
18		ssel	$⊢ dom A \cap ran B \subseteq C \to (x \in (dom A \cap ran B) \to x \in C)$
19	17 18	syl5	$⊢ dom A \cap ran B \subseteq C \to (y \in (B^{-1} [\{x\}] \times A [\{x\}]) \to x \in C)$
20	19	pm4.71rd	$⊢ dom A \cap ran B \subseteq C \to (y \in (B^{-1} [\{x\}] \times A [\{x\}]) \leftrightarrow (x \in C \land y \in (B^{-1} [\{x\}] \times A [\{x\}])))$
21	20	exbidv	$⊢ dom A \cap ran B \subseteq C \to (\exists x y \in (B^{-1} [\{x\}] \times A [\{x\}]) \leftrightarrow \exists x (x \in C \land y \in (B^{-1} [\{x\}] \times A [\{x\}])))$
22		rexv	$⊢ \exists x \in V y \in (B^{-1} [\{x\}] \times A [\{x\}]) \leftrightarrow \exists x y \in (B^{-1} [\{x\}] \times A [\{x\}])$
23		df-rex	$⊢ \exists x \in C y \in (B^{-1} [\{x\}] \times A [\{x\}]) \leftrightarrow \exists x (x \in C \land y \in (B^{-1} [\{x\}] \times A [\{x\}]))$
24	21 22 23	3bitr4g	$⊢ dom A \cap ran B \subseteq C \to (\exists x \in V y \in (B^{-1} [\{x\}] \times A [\{x\}]) \leftrightarrow \exists x \in C y \in (B^{-1} [\{x\}] \times A [\{x\}]))$
25		eliun	$⊢ y \in ⋃_{x \in V} (B^{-1} [\{x\}] \times A [\{x\}]) \leftrightarrow \exists x \in V y \in (B^{-1} [\{x\}] \times A [\{x\}])$
26		eliun	$⊢ y \in ⋃_{x \in C} (B^{-1} [\{x\}] \times A [\{x\}]) \leftrightarrow \exists x \in C y \in (B^{-1} [\{x\}] \times A [\{x\}])$
27	24 25 26	3bitr4g	$⊢ dom A \cap ran B \subseteq C \to (y \in ⋃_{x \in V} (B^{-1} [\{x\}] \times A [\{x\}]) \leftrightarrow y \in ⋃_{x \in C} (B^{-1} [\{x\}] \times A [\{x\}]))$
28	27	eqrdv	$⊢ dom A \cap ran B \subseteq C \to ⋃_{x \in V} (B^{-1} [\{x\}] \times A [\{x\}]) = ⋃_{x \in C} (B^{-1} [\{x\}] \times A [\{x\}])$
29	1 28	syl5eq	$⊢ dom A \cap ran B \subseteq C \to A \circ B = ⋃_{x \in C} (B^{-1} [\{x\}] \times A [\{x\}])$

Metamath Proof Explorer

Theorem dfco2a

Proof