marypha2lem4

Description: Lemma for marypha2 . Properties of the used relation. (Contributed by Stefan O'Rear, 20-Feb-2015)

		Ref	Expression
	Hypothesis	marypha2lem.t	$⊢ T = ⋃_{x \in A} (\{x\} \times F (x))$
	Assertion	marypha2lem4	$⊢ (F Fn A \land X \subseteq A) \to T [X] = ⋃ F [X]$

Proof

Step	Hyp	Ref	Expression
1		marypha2lem.t	$⊢ T = ⋃_{x \in A} (\{x\} \times F (x))$
2	1	marypha2lem2	$⊢ T = \{⟨x, y⟩ \| (x \in A \land y \in F (x))\}$
3	2	imaeq1i	$⊢ T [X] = \{⟨x, y⟩ \| (x \in A \land y \in F (x))\} [X]$
4		df-ima	$⊢ \{⟨x, y⟩ \| (x \in A \land y \in F (x))\} [X] = ran ({\{⟨x, y⟩ \| (x \in A \land y \in F (x))\} ↾}_{X})$
5	3 4	eqtri	$⊢ T [X] = ran ({\{⟨x, y⟩ \| (x \in A \land y \in F (x))\} ↾}_{X})$
6		resopab2	$⊢ X \subseteq A \to {\{⟨x, y⟩ \| (x \in A \land y \in F (x))\} ↾}_{X} = \{⟨x, y⟩ \| (x \in X \land y \in F (x))\}$
7	6	adantl	$⊢ (F Fn A \land X \subseteq A) \to {\{⟨x, y⟩ \| (x \in A \land y \in F (x))\} ↾}_{X} = \{⟨x, y⟩ \| (x \in X \land y \in F (x))\}$
8	7	rneqd	$⊢ (F Fn A \land X \subseteq A) \to ran ({\{⟨x, y⟩ \| (x \in A \land y \in F (x))\} ↾}_{X}) = ran \{⟨x, y⟩ \| (x \in X \land y \in F (x))\}$
9		rnopab	$⊢ ran \{⟨x, y⟩ \| (x \in X \land y \in F (x))\} = \{y \| \exists x (x \in X \land y \in F (x))\}$
10		df-rex	$⊢ \exists x \in X y \in F (x) \leftrightarrow \exists x (x \in X \land y \in F (x))$
11	10	bicomi	$⊢ \exists x (x \in X \land y \in F (x)) \leftrightarrow \exists x \in X y \in F (x)$
12	11	abbii	$⊢ \{y \| \exists x (x \in X \land y \in F (x))\} = \{y \| \exists x \in X y \in F (x)\}$
13		df-iun	$⊢ ⋃_{x \in X} F (x) = \{y \| \exists x \in X y \in F (x)\}$
14	12 13	eqtr4i	$⊢ \{y \| \exists x (x \in X \land y \in F (x))\} = ⋃_{x \in X} F (x)$
15	14	a1i	$⊢ (F Fn A \land X \subseteq A) \to \{y \| \exists x (x \in X \land y \in F (x))\} = ⋃_{x \in X} F (x)$
16	9 15	syl5eq	$⊢ (F Fn A \land X \subseteq A) \to ran \{⟨x, y⟩ \| (x \in X \land y \in F (x))\} = ⋃_{x \in X} F (x)$
17	8 16	eqtrd	$⊢ (F Fn A \land X \subseteq A) \to ran ({\{⟨x, y⟩ \| (x \in A \land y \in F (x))\} ↾}_{X}) = ⋃_{x \in X} F (x)$
18	5 17	syl5eq	$⊢ (F Fn A \land X \subseteq A) \to T [X] = ⋃_{x \in X} F (x)$
19		fnfun	$⊢ F Fn A \to Fun F$
20	19	adantr	$⊢ (F Fn A \land X \subseteq A) \to Fun F$
21		funiunfv	$⊢ Fun F \to ⋃_{x \in X} F (x) = ⋃ F [X]$
22	20 21	syl	$⊢ (F Fn A \land X \subseteq A) \to ⋃_{x \in X} F (x) = ⋃ F [X]$
23	18 22	eqtrd	$⊢ (F Fn A \land X \subseteq A) \to T [X] = ⋃ F [X]$

Metamath Proof Explorer

Theorem marypha2lem4

Proof