Theorem grucollcld

Description: A Grothendieck universe contains the output of a collection operation whenever its left input is a relation on the universe, and its right input is in the universe. (Contributed by Rohan Ridenour, 11-Aug-2023)

	Ref	Expression
Hypotheses	grucollcld.1	|- ( ph -> G e. Univ )
	grucollcld.2	|- ( ph -> F C_ ( G X. G ) )
	grucollcld.3	|- ( ph -> A e. G )
Assertion	grucollcld	|- ( ph -> ( F Coll A ) e. G )

Proof

Step	Hyp	Ref	Expression
1		grucollcld.1	|- ( ph -> G e. Univ )
2		grucollcld.2	|- ( ph -> F C_ ( G X. G ) )
3		grucollcld.3	|- ( ph -> A e. G )
4		dfcoll2	|- ( F Coll A ) = U_ x e. A Scott { y | x F y }
5		simpr	|- ( ( ( ph /\ x e. A ) /\ Scott { y | x F y } = (/) ) -> Scott { y | x F y } = (/) )
6	1	ad2antrr	|- ( ( ( ph /\ x e. A ) /\ Scott { y | x F y } = (/) ) -> G e. Univ )
7	3	ad2antrr	|- ( ( ( ph /\ x e. A ) /\ Scott { y | x F y } = (/) ) -> A e. G )
8	6 7	gru0eld	|- ( ( ( ph /\ x e. A ) /\ Scott { y | x F y } = (/) ) -> (/) e. G )
9	5 8	eqeltrd	|- ( ( ( ph /\ x e. A ) /\ Scott { y | x F y } = (/) ) -> Scott { y | x F y } e. G )
10		neq0	|- ( -. Scott { y | x F y } = (/) <-> E. z z e. Scott { y | x F y } )
11	1	ad2antrr	|- ( ( ( ph /\ x e. A ) /\ z e. Scott { y | x F y } ) -> G e. Univ )
12		breq2	|- ( y = z -> ( x F y <-> x F z ) )
13	12	elscottab	|- ( z e. Scott { y | x F y } -> x F z )
14	13	adantl	|- ( ( ( ph /\ x e. A ) /\ z e. Scott { y | x F y } ) -> x F z )
15	2	ad2antrr	|- ( ( ( ph /\ x e. A ) /\ z e. Scott { y | x F y } ) -> F C_ ( G X. G ) )
16	15	ssbrd	|- ( ( ( ph /\ x e. A ) /\ z e. Scott { y | x F y } ) -> ( x F z -> x ( G X. G ) z ) )
17	14 16	mpd	|- ( ( ( ph /\ x e. A ) /\ z e. Scott { y | x F y } ) -> x ( G X. G ) z )
18		brxp	|- ( x ( G X. G ) z <-> ( x e. G /\ z e. G ) )
19	18	simprbi	|- ( x ( G X. G ) z -> z e. G )
20	17 19	syl	|- ( ( ( ph /\ x e. A ) /\ z e. Scott { y | x F y } ) -> z e. G )
21		simpr	|- ( ( ( ph /\ x e. A ) /\ z e. Scott { y | x F y } ) -> z e. Scott { y | x F y } )
22	11 20 21	gruscottcld	|- ( ( ( ph /\ x e. A ) /\ z e. Scott { y | x F y } ) -> Scott { y | x F y } e. G )
23	22	expcom	|- ( z e. Scott { y | x F y } -> ( ( ph /\ x e. A ) -> Scott { y | x F y } e. G ) )
24	23	exlimiv	|- ( E. z z e. Scott { y | x F y } -> ( ( ph /\ x e. A ) -> Scott { y | x F y } e. G ) )
25	10 24	sylbi	|- ( -. Scott { y | x F y } = (/) -> ( ( ph /\ x e. A ) -> Scott { y | x F y } e. G ) )
26	25	impcom	|- ( ( ( ph /\ x e. A ) /\ -. Scott { y | x F y } = (/) ) -> Scott { y | x F y } e. G )
27	9 26	pm2.61dan	|- ( ( ph /\ x e. A ) -> Scott { y | x F y } e. G )
28	27	ralrimiva	|- ( ph -> A. x e. A Scott { y | x F y } e. G )
29		gruiun	|- ( ( G e. Univ /\ A e. G /\ A. x e. A Scott { y | x F y } e. G ) -> U_ x e. A Scott { y | x F y } e. G )
30	1 3 28 29	syl3anc	|- ( ph -> U_ x e. A Scott { y | x F y } e. G )
31	4 30	eqeltrid	|- ( ph -> ( F Coll A ) e. G )