Theorem gruwun

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

	Ref	Expression
Assertion	gruwun	|- ( ( U e. Univ /\ U =/= (/) ) -> U e. WUni )

Proof

Step	Hyp	Ref	Expression
1		grutr	|- ( U e. Univ -> Tr U )
2	1	adantr	|- ( ( U e. Univ /\ U =/= (/) ) -> Tr U )
3		simpr	|- ( ( U e. Univ /\ U =/= (/) ) -> U =/= (/) )
4		gruuni	|- ( ( U e. Univ /\ x e. U ) -> U. x e. U )
5	4	adantlr	|- ( ( ( U e. Univ /\ U =/= (/) ) /\ x e. U ) -> U. x e. U )
6		grupw	|- ( ( U e. Univ /\ x e. U ) -> ~P x e. U )
7	6	adantlr	|- ( ( ( U e. Univ /\ U =/= (/) ) /\ x e. U ) -> ~P x e. U )
8		grupr	|- ( ( U e. Univ /\ x e. U /\ y e. U ) -> { x , y } e. U )
9	8	ad4ant134	|- ( ( ( ( U e. Univ /\ U =/= (/) ) /\ x e. U ) /\ y e. U ) -> { x , y } e. U )
10	9	ralrimiva	|- ( ( ( U e. Univ /\ U =/= (/) ) /\ x e. U ) -> A. y e. U { x , y } e. U )
11	5 7 10	3jca	|- ( ( ( U e. Univ /\ U =/= (/) ) /\ x e. U ) -> ( U. x e. U /\ ~P x e. U /\ A. y e. U { x , y } e. U ) )
12	11	ralrimiva	|- ( ( U e. Univ /\ U =/= (/) ) -> A. x e. U ( U. x e. U /\ ~P x e. U /\ A. y e. U { x , y } e. U ) )
13		iswun	|- ( U e. Univ -> ( U e. WUni <-> ( Tr U /\ U =/= (/) /\ A. x e. U ( U. x e. U /\ ~P x e. U /\ A. y e. U { x , y } e. U ) ) ) )
14	13	adantr	|- ( ( U e. Univ /\ U =/= (/) ) -> ( U e. WUni <-> ( Tr U /\ U =/= (/) /\ A. x e. U ( U. x e. U /\ ~P x e. U /\ A. y e. U { x , y } e. U ) ) ) )
15	2 3 12 14	mpbir3and	|- ( ( U e. Univ /\ U =/= (/) ) -> U e. WUni )