Metamath Proof Explorer


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 φ G Univ
grucollcld.2 φ F G × G
grucollcld.3 φ A G
Assertion grucollcld φ F Coll A G

Proof

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