gruiin

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

		Ref	Expression
	Assertion	gruiin	$⊢ (U \in Univ \land \exists x \in A B \in U) \to ⋂_{x \in A} B \in U$

Step	Hyp	Ref	Expression
1		nfv	$⊢ Ⅎ x U \in Univ$
2		nfii1	$⊢ \underline{Ⅎ} x ⋂_{x \in A} B$
3	2	nfel1	$⊢ Ⅎ x ⋂_{x \in A} B \in U$
4		iinss2	$⊢ x \in A \to ⋂_{x \in A} B \subseteq B$
5		gruss	$⊢ (U \in Univ \land B \in U \land ⋂_{x \in A} B \subseteq B) \to ⋂_{x \in A} B \in U$
6	4 5	syl3an3	$⊢ (U \in Univ \land B \in U \land x \in A) \to ⋂_{x \in A} B \in U$
7	6	3exp	$⊢ U \in Univ \to (B \in U \to (x \in A \to ⋂_{x \in A} B \in U))$
8	7	com23	$⊢ U \in Univ \to (x \in A \to (B \in U \to ⋂_{x \in A} B \in U))$
9	1 3 8	rexlimd	$⊢ U \in Univ \to (\exists x \in A B \in U \to ⋂_{x \in A} B \in U)$
10	9	imp	$⊢ (U \in Univ \land \exists x \in A B \in U) \to ⋂_{x \in A} B \in U$

Metamath Proof Explorer