marypha2lem2

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	marypha2lem2	$⊢ T = \{⟨x, y⟩ \| (x \in A \land y \in F (x))\}$

Proof

Step	Hyp	Ref	Expression
1		marypha2lem.t	$⊢ T = ⋃_{x \in A} (\{x\} \times F (x))$
2		sneq	$⊢ x = z \to \{x\} = \{z\}$
3		fveq2	$⊢ x = z \to F (x) = F (z)$
4	2 3	xpeq12d	$⊢ x = z \to \{x\} \times F (x) = \{z\} \times F (z)$
5	4	cbviunv	$⊢ ⋃_{x \in A} (\{x\} \times F (x)) = ⋃_{z \in A} (\{z\} \times F (z))$
6		df-xp	$⊢ \{z\} \times F (z) = \{⟨x, y⟩ \| (x \in \{z\} \land y \in F (z))\}$
7	6	a1i	$⊢ z \in A \to \{z\} \times F (z) = \{⟨x, y⟩ \| (x \in \{z\} \land y \in F (z))\}$
8	7	iuneq2i	$⊢ ⋃_{z \in A} (\{z\} \times F (z)) = ⋃_{z \in A} \{⟨x, y⟩ \| (x \in \{z\} \land y \in F (z))\}$
9		iunopab	$⊢ ⋃_{z \in A} \{⟨x, y⟩ \| (x \in \{z\} \land y \in F (z))\} = \{⟨x, y⟩ \| \exists z \in A (x \in \{z\} \land y \in F (z))\}$
10		velsn	$⊢ x \in \{z\} \leftrightarrow x = z$
11		equcom	$⊢ x = z \leftrightarrow z = x$
12	10 11	bitri	$⊢ x \in \{z\} \leftrightarrow z = x$
13	12	anbi1i	$⊢ (x \in \{z\} \land y \in F (z)) \leftrightarrow (z = x \land y \in F (z))$
14	13	rexbii	$⊢ \exists z \in A (x \in \{z\} \land y \in F (z)) \leftrightarrow \exists z \in A (z = x \land y \in F (z))$
15		fveq2	$⊢ z = x \to F (z) = F (x)$
16	15	eleq2d	$⊢ z = x \to (y \in F (z) \leftrightarrow y \in F (x))$
17	16	ceqsrexbv	$⊢ \exists z \in A (z = x \land y \in F (z)) \leftrightarrow (x \in A \land y \in F (x))$
18	14 17	bitri	$⊢ \exists z \in A (x \in \{z\} \land y \in F (z)) \leftrightarrow (x \in A \land y \in F (x))$
19	18	opabbii	$⊢ \{⟨x, y⟩ \| \exists z \in A (x \in \{z\} \land y \in F (z))\} = \{⟨x, y⟩ \| (x \in A \land y \in F (x))\}$
20	8 9 19	3eqtri	$⊢ ⋃_{z \in A} (\{z\} \times F (z)) = \{⟨x, y⟩ \| (x \in A \land y \in F (x))\}$
21	1 5 20	3eqtri	$⊢ T = \{⟨x, y⟩ \| (x \in A \land y \in F (x))\}$

Metamath Proof Explorer

Theorem marypha2lem2

Proof