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	⊢ ( 𝜑 → 𝐺 ∈ Univ )
	grucollcld.2	⊢ ( 𝜑 → 𝐹 ⊆ ( 𝐺 × 𝐺 ) )
	grucollcld.3	⊢ ( 𝜑 → 𝐴 ∈ 𝐺 )
Assertion	grucollcld	⊢ ( 𝜑 → ( 𝐹 Coll 𝐴 ) ∈ 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		grucollcld.1	⊢ ( 𝜑 → 𝐺 ∈ Univ )
2		grucollcld.2	⊢ ( 𝜑 → 𝐹 ⊆ ( 𝐺 × 𝐺 ) )
3		grucollcld.3	⊢ ( 𝜑 → 𝐴 ∈ 𝐺 )
4		dfcoll2	⊢ ( 𝐹 Coll 𝐴 ) = ∪ 𝑥 ∈ 𝐴 Scott { 𝑦 ∣ 𝑥 𝐹 𝑦 }
5		simpr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ Scott { 𝑦 ∣ 𝑥 𝐹 𝑦 } = ∅ ) → Scott { 𝑦 ∣ 𝑥 𝐹 𝑦 } = ∅ )
6	1	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ Scott { 𝑦 ∣ 𝑥 𝐹 𝑦 } = ∅ ) → 𝐺 ∈ Univ )
7	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ Scott { 𝑦 ∣ 𝑥 𝐹 𝑦 } = ∅ ) → 𝐴 ∈ 𝐺 )
8	6 7	gru0eld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ Scott { 𝑦 ∣ 𝑥 𝐹 𝑦 } = ∅ ) → ∅ ∈ 𝐺 )
9	5 8	eqeltrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ Scott { 𝑦 ∣ 𝑥 𝐹 𝑦 } = ∅ ) → Scott { 𝑦 ∣ 𝑥 𝐹 𝑦 } ∈ 𝐺 )
10		neq0	⊢ ( ¬ Scott { 𝑦 ∣ 𝑥 𝐹 𝑦 } = ∅ ↔ ∃ 𝑧 𝑧 ∈ Scott { 𝑦 ∣ 𝑥 𝐹 𝑦 } )
11	1	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ Scott { 𝑦 ∣ 𝑥 𝐹 𝑦 } ) → 𝐺 ∈ Univ )
12		breq2	⊢ ( 𝑦 = 𝑧 → ( 𝑥 𝐹 𝑦 ↔ 𝑥 𝐹 𝑧 ) )
13	12	elscottab	⊢ ( 𝑧 ∈ Scott { 𝑦 ∣ 𝑥 𝐹 𝑦 } → 𝑥 𝐹 𝑧 )
14	13	adantl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ Scott { 𝑦 ∣ 𝑥 𝐹 𝑦 } ) → 𝑥 𝐹 𝑧 )
15	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ Scott { 𝑦 ∣ 𝑥 𝐹 𝑦 } ) → 𝐹 ⊆ ( 𝐺 × 𝐺 ) )
16	15	ssbrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ Scott { 𝑦 ∣ 𝑥 𝐹 𝑦 } ) → ( 𝑥 𝐹 𝑧 → 𝑥 ( 𝐺 × 𝐺 ) 𝑧 ) )
17	14 16	mpd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ Scott { 𝑦 ∣ 𝑥 𝐹 𝑦 } ) → 𝑥 ( 𝐺 × 𝐺 ) 𝑧 )
18		brxp	⊢ ( 𝑥 ( 𝐺 × 𝐺 ) 𝑧 ↔ ( 𝑥 ∈ 𝐺 ∧ 𝑧 ∈ 𝐺 ) )
19	18	simprbi	⊢ ( 𝑥 ( 𝐺 × 𝐺 ) 𝑧 → 𝑧 ∈ 𝐺 )
20	17 19	syl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ Scott { 𝑦 ∣ 𝑥 𝐹 𝑦 } ) → 𝑧 ∈ 𝐺 )
21		simpr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ Scott { 𝑦 ∣ 𝑥 𝐹 𝑦 } ) → 𝑧 ∈ Scott { 𝑦 ∣ 𝑥 𝐹 𝑦 } )
22	11 20 21	gruscottcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ Scott { 𝑦 ∣ 𝑥 𝐹 𝑦 } ) → Scott { 𝑦 ∣ 𝑥 𝐹 𝑦 } ∈ 𝐺 )
23	22	expcom	⊢ ( 𝑧 ∈ Scott { 𝑦 ∣ 𝑥 𝐹 𝑦 } → ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → Scott { 𝑦 ∣ 𝑥 𝐹 𝑦 } ∈ 𝐺 ) )
24	23	exlimiv	⊢ ( ∃ 𝑧 𝑧 ∈ Scott { 𝑦 ∣ 𝑥 𝐹 𝑦 } → ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → Scott { 𝑦 ∣ 𝑥 𝐹 𝑦 } ∈ 𝐺 ) )
25	10 24	sylbi	⊢ ( ¬ Scott { 𝑦 ∣ 𝑥 𝐹 𝑦 } = ∅ → ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → Scott { 𝑦 ∣ 𝑥 𝐹 𝑦 } ∈ 𝐺 ) )
26	25	impcom	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ¬ Scott { 𝑦 ∣ 𝑥 𝐹 𝑦 } = ∅ ) → Scott { 𝑦 ∣ 𝑥 𝐹 𝑦 } ∈ 𝐺 )
27	9 26	pm2.61dan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → Scott { 𝑦 ∣ 𝑥 𝐹 𝑦 } ∈ 𝐺 )
28	27	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 Scott { 𝑦 ∣ 𝑥 𝐹 𝑦 } ∈ 𝐺 )
29		gruiun	⊢ ( ( 𝐺 ∈ Univ ∧ 𝐴 ∈ 𝐺 ∧ ∀ 𝑥 ∈ 𝐴 Scott { 𝑦 ∣ 𝑥 𝐹 𝑦 } ∈ 𝐺 ) → ∪ 𝑥 ∈ 𝐴 Scott { 𝑦 ∣ 𝑥 𝐹 𝑦 } ∈ 𝐺 )
30	1 3 28 29	syl3anc	⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 Scott { 𝑦 ∣ 𝑥 𝐹 𝑦 } ∈ 𝐺 )
31	4 30	eqeltrid	⊢ ( 𝜑 → ( 𝐹 Coll 𝐴 ) ∈ 𝐺 )