Theorem cpcolld

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

	Ref	Expression
Hypotheses	cpcolld.1	|- ( ph -> x e. A )
	cpcolld.2	|- ( ph -> x F y )
Assertion	cpcolld	|- ( ph -> E. y e. ( F Coll A ) x F y )

Proof

Step	Hyp	Ref	Expression
1		cpcolld.1	|- ( ph -> x e. A )
2		cpcolld.2	|- ( ph -> x F y )
3		vex	|- y e. _V
4		breq2	|- ( z = y -> ( x F z <-> x F y ) )
5	3 4	elab	|- ( y e. { z | x F z } <-> x F y )
6	2 5	sylibr	|- ( ph -> y e. { z | x F z } )
7	6	19.8ad	|- ( ph -> E. y y e. { z | x F z } )
8	7	scotteld	|- ( ph -> E. y y e. Scott { z | x F z } )
9		ssiun2	|- ( x e. A -> Scott { z | x F z } C_ U_ x e. A Scott { z | x F z } )
10		dfcoll2	|- ( F Coll A ) = U_ x e. A Scott { z | x F z }
11	9 10	sseqtrrdi	|- ( x e. A -> Scott { z | x F z } C_ ( F Coll A ) )
12	11	sselda	|- ( ( x e. A /\ y e. Scott { z | x F z } ) -> y e. ( F Coll A ) )
13	4	elscottab	|- ( y e. Scott { z | x F z } -> x F y )
14	13	adantl	|- ( ( x e. A /\ y e. Scott { z | x F z } ) -> x F y )
15	12 14	jca	|- ( ( x e. A /\ y e. Scott { z | x F z } ) -> ( y e. ( F Coll A ) /\ x F y ) )
16	15	ex	|- ( x e. A -> ( y e. Scott { z | x F z } -> ( y e. ( F Coll A ) /\ x F y ) ) )
17	16	eximdv	|- ( x e. A -> ( E. y y e. Scott { z | x F z } -> E. y ( y e. ( F Coll A ) /\ x F y ) ) )
18	1 8 17	sylc	|- ( ph -> E. y ( y e. ( F Coll A ) /\ x F y ) )
19		df-rex	|- ( E. y e. ( F Coll A ) x F y <-> E. y ( y e. ( F Coll A ) /\ x F y ) )
20	18 19	sylibr	|- ( ph -> E. y e. ( F Coll A ) x F y )