Theorem gruiin

Description: A Grothendieck universe contains indexed intersections of its elements. (Contributed by Mario Carneiro, 9-Jun-2013)

	Ref	Expression
Assertion	gruiin	⊢ ( ( 𝑈 ∈ Univ ∧ ∃ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑈 ) → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		nfv	⊢ Ⅎ 𝑥 𝑈 ∈ Univ
2		nfii1	⊢ Ⅎ 𝑥 ∩ 𝑥 ∈ 𝐴 𝐵
3	2	nfel1	⊢ Ⅎ 𝑥 ∩ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑈
4		iinss2	⊢ ( 𝑥 ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐵 )
5		gruss	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐵 ∈ 𝑈 ∧ ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐵 ) → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑈 )
6	4 5	syl3an3	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐵 ∈ 𝑈 ∧ 𝑥 ∈ 𝐴 ) → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑈 )
7	6	3exp	⊢ ( 𝑈 ∈ Univ → ( 𝐵 ∈ 𝑈 → ( 𝑥 ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑈 ) ) )
8	7	com23	⊢ ( 𝑈 ∈ Univ → ( 𝑥 ∈ 𝐴 → ( 𝐵 ∈ 𝑈 → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑈 ) ) )
9	1 3 8	rexlimd	⊢ ( 𝑈 ∈ Univ → ( ∃ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑈 → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑈 ) )
10	9	imp	⊢ ( ( 𝑈 ∈ Univ ∧ ∃ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑈 ) → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑈 )