Theorem grutr

Description: A Grothendieck universe is transitive. (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Assertion	grutr	$$⊢U\in \mathrm{Univ}\to \mathrm{Tr}U$$

Proof

Step	Hyp	Ref	Expression
1		elgrug	$$⊢U\in \mathrm{Univ}\to \left(U\in \mathrm{Univ}\leftrightarrow \left(\mathrm{Tr}U\wedge \forall x\in U\left(𝒫x\in U\wedge \forall y\in U\left\{x,y\right\}\in U\wedge \forall y\in \left(U^x\right)\bigcup \mathrm{ran}y\in U\right)\right)\right)$$
2	1	ibi	$$⊢U\in \mathrm{Univ}\to \left(\mathrm{Tr}U\wedge \forall x\in U\left(𝒫x\in U\wedge \forall y\in U\left\{x,y\right\}\in U\wedge \forall y\in \left(U^x\right)\bigcup \mathrm{ran}y\in U\right)\right)$$
3	2	simpld	$$⊢U\in \mathrm{Univ}\to \mathrm{Tr}U$$