Metamath Proof Explorer

Theorem gruiin

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

Ref Expression
Assertion gruiin ⊢ U ∈ Univ ∧ ∃ x ∈ A B ∈ U → ⋂ x ∈ A B ∈ U

Proof

Step Hyp Ref Expression
1 nfv ⊢ Ⅎ x U ∈ Univ
2 nfii1 ⊢ Ⅎ _ x ⋂ x ∈ A B
3 2 nfel1 ⊢ Ⅎ x ⋂ x ∈ A B ∈ U
4 iinss2 ⊢ x ∈ A → ⋂ x ∈ A B ⊆ B
5 gruss ⊢ U ∈ Univ ∧ B ∈ U ∧ ⋂ x ∈ A B ⊆ B → ⋂ x ∈ A B ∈ U
6 4 5 syl3an3 ⊢ U ∈ Univ ∧ B ∈ U ∧ x ∈ A → ⋂ x ∈ A B ∈ U
7 6 3exp ⊢ U ∈ Univ → B ∈ U → x ∈ A → ⋂ x ∈ A B ∈ U
8 7 com23 ⊢ U ∈ Univ → x ∈ A → B ∈ U → ⋂ x ∈ A B ∈ U
9 1 3 8 rexlimd ⊢ U ∈ Univ → ∃ x ∈ A B ∈ U → ⋂ x ∈ A B ∈ U
10 9 imp ⊢ U ∈ Univ ∧ ∃ x ∈ A B ∈ U → ⋂ x ∈ A B ∈ U