Theorem elgrug

Description: Properties of a Grothendieck universe. (Contributed by Mario Carneiro, 9-Jun-2013)

	Ref	Expression
Assertion	elgrug	|- ( U e. V -> ( 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 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		treq	|- ( u = U -> ( Tr u <-> Tr U ) )
2		eleq2	|- ( u = U -> ( ~P x e. u <-> ~P x e. U ) )
3		eleq2	|- ( u = U -> ( { x , y } e. u <-> { x , y } e. U ) )
4	3	raleqbi1dv	|- ( u = U -> ( A. y e. u { x , y } e. u <-> A. y e. U { x , y } e. U ) )
5		oveq1	|- ( u = U -> ( u ^m x ) = ( U ^m x ) )
6		eleq2	|- ( u = U -> ( U. ran y e. u <-> U. ran y e. U ) )
7	5 6	raleqbidv	|- ( u = U -> ( A. y e. ( u ^m x ) U. ran y e. u <-> A. y e. ( U ^m x ) U. ran y e. U ) )
8	2 4 7	3anbi123d	|- ( u = U -> ( ( ~P x e. u /\ A. y e. u { x , y } e. u /\ A. y e. ( u ^m x ) U. ran y 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 ) ) )
9	8	raleqbi1dv	|- ( u = 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 ) <-> 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 ) ) )
10	1 9	anbi12d	|- ( u = U -> ( ( 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 ) ) <-> ( 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 ) ) ) )
11		df-gru	|- Univ = { u | ( 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 ) ) }
12	10 11	elab2g	|- ( U e. V -> ( 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 ) ) ) )