cpcolld

Description: Property of the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023)

Step	Hyp	Ref	Expression
1		cpcolld.1	$⊢ φ \to x \in A$
2		cpcolld.2	$⊢ φ \to x F y$
3		vex	$⊢ y \in V$
4		breq2	$⊢ z = y \to (x F z \leftrightarrow x F y)$
5	3 4	elab	$⊢ y \in \{z \| x F z\} \leftrightarrow x F y$
6	2 5	sylibr	$⊢ φ \to y \in \{z \| x F z\}$
7	6	19.8ad	$⊢ φ \to \exists y y \in \{z \| x F z\}$
8	7	scotteld	$⊢ φ \to \exists y y \in Scott \{z \| x F z\}$
9		ssiun2	$⊢ x \in A \to Scott \{z \| x F z\} \subseteq ⋃_{x \in A} Scott \{z \| x F z\}$
10		dfcoll2	$⊢ (F Coll A) = ⋃_{x \in A} Scott \{z \| x F z\}$
11	9 10	sseqtrrdi	$⊢ x \in A \to Scott \{z \| x F z\} \subseteq (F Coll A)$
12	11	sselda	$⊢ (x \in A \land y \in Scott \{z \| x F z\}) \to y \in (F Coll A)$
13	4	elscottab	$⊢ y \in Scott \{z \| x F z\} \to x F y$
14	13	adantl	$⊢ (x \in A \land y \in Scott \{z \| x F z\}) \to x F y$
15	12 14	jca	$⊢ (x \in A \land y \in Scott \{z \| x F z\}) \to (y \in (F Coll A) \land x F y)$
16	15	ex	$⊢ x \in A \to (y \in Scott \{z \| x F z\} \to (y \in (F Coll A) \land x F y))$
17	16	eximdv	$⊢ x \in A \to (\exists y y \in Scott \{z \| x F z\} \to \exists y (y \in (F Coll A) \land x F y))$
18	1 8 17	sylc	$⊢ φ \to \exists y (y \in (F Coll A) \land x F y)$
19		df-rex	$⊢ \exists y \in (F Coll A) x F y \leftrightarrow \exists y (y \in (F Coll A) \land x F y)$
20	18 19	sylibr	$⊢ φ \to \exists y \in (F Coll A) x F y$

Metamath Proof Explorer