Theorem grutsk1

Description: Grothendieck universes are the same as transitive Tarski classes, part one: a transitive Tarski class is a universe. (The hard work is in tskuni .) (Contributed by Mario Carneiro, 17-Jun-2013)

	Ref	Expression
Assertion	grutsk1	|- ( ( T e. Tarski /\ Tr T ) -> T e. Univ )

Proof

Step	Hyp	Ref	Expression
1		simpr	|- ( ( T e. Tarski /\ Tr T ) -> Tr T )
2		tskpw	|- ( ( T e. Tarski /\ x e. T ) -> ~P x e. T )
3	2	adantlr	|- ( ( ( T e. Tarski /\ Tr T ) /\ x e. T ) -> ~P x e. T )
4		tskpr	|- ( ( T e. Tarski /\ x e. T /\ y e. T ) -> { x , y } e. T )
5	4	3expa	|- ( ( ( T e. Tarski /\ x e. T ) /\ y e. T ) -> { x , y } e. T )
6	5	ralrimiva	|- ( ( T e. Tarski /\ x e. T ) -> A. y e. T { x , y } e. T )
7	6	adantlr	|- ( ( ( T e. Tarski /\ Tr T ) /\ x e. T ) -> A. y e. T { x , y } e. T )
8		elmapg	|- ( ( T e. Tarski /\ x e. T ) -> ( y e. ( T ^m x ) <-> y : x --> T ) )
9	8	adantlr	|- ( ( ( T e. Tarski /\ Tr T ) /\ x e. T ) -> ( y e. ( T ^m x ) <-> y : x --> T ) )
10		tskurn	|- ( ( ( T e. Tarski /\ Tr T ) /\ x e. T /\ y : x --> T ) -> U. ran y e. T )
11	10	3expia	|- ( ( ( T e. Tarski /\ Tr T ) /\ x e. T ) -> ( y : x --> T -> U. ran y e. T ) )
12	9 11	sylbid	|- ( ( ( T e. Tarski /\ Tr T ) /\ x e. T ) -> ( y e. ( T ^m x ) -> U. ran y e. T ) )
13	12	ralrimiv	|- ( ( ( T e. Tarski /\ Tr T ) /\ x e. T ) -> A. y e. ( T ^m x ) U. ran y e. T )
14	3 7 13	3jca	|- ( ( ( T e. Tarski /\ Tr T ) /\ x e. T ) -> ( ~P x e. T /\ A. y e. T { x , y } e. T /\ A. y e. ( T ^m x ) U. ran y e. T ) )
15	14	ralrimiva	|- ( ( T e. Tarski /\ Tr T ) -> A. x e. T ( ~P x e. T /\ A. y e. T { x , y } e. T /\ A. y e. ( T ^m x ) U. ran y e. T ) )
16		elgrug	|- ( T e. Tarski -> ( T e. Univ <-> ( Tr T /\ A. x e. T ( ~P x e. T /\ A. y e. T { x , y } e. T /\ A. y e. ( T ^m x ) U. ran y e. T ) ) ) )
17	16	adantr	|- ( ( T e. Tarski /\ Tr T ) -> ( T e. Univ <-> ( Tr T /\ A. x e. T ( ~P x e. T /\ A. y e. T { x , y } e. T /\ A. y e. ( T ^m x ) U. ran y e. T ) ) ) )
18	1 15 17	mpbir2and	|- ( ( T e. Tarski /\ Tr T ) -> T e. Univ )