Theorem grutr

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

	Ref	Expression
Assertion	grutr	|- ( U e. Univ -> Tr U )

Proof

Step	Hyp	Ref	Expression
1		elgrug	|- ( U e. Univ -> ( U e. Univ <-> ( Tr U /\ A. x e. U ( ~P x e. U /\ A. y e. U { x , y } e. U /\ A. y e. ( U ^m x ) U. ran y e. U ) ) ) )
2	1	ibi	|- ( U e. Univ -> ( Tr U /\ A. x e. U ( ~P x e. U /\ A. y e. U { x , y } e. U /\ A. y e. ( U ^m x ) U. ran y e. U ) ) )
3	2	simpld	|- ( U e. Univ -> Tr U )