Theorem grutsk

Description: Grothendieck universes are the same as transitive Tarski classes. (The proof in the forward direction requires Foundation.) (Contributed by Mario Carneiro, 24-Jun-2013)

	Ref	Expression
Assertion	grutsk	|- Univ = { x e. Tarski | Tr x }

Proof

Step	Hyp	Ref	Expression
1		0tsk	|- (/) e. Tarski
2		eleq1	|- ( y = (/) -> ( y e. Tarski <-> (/) e. Tarski ) )
3	1 2	mpbiri	|- ( y = (/) -> y e. Tarski )
4	3	a1i	|- ( y e. Univ -> ( y = (/) -> y e. Tarski ) )
5		vex	|- y e. _V
6		unir1	|- U. ( R1 " On ) = _V
7	5 6	eleqtrri	|- y e. U. ( R1 " On )
8		eqid	|- ( y i^i On ) = ( y i^i On )
9	8	grur1	|- ( ( y e. Univ /\ y e. U. ( R1 " On ) ) -> y = ( R1 ` ( y i^i On ) ) )
10	7 9	mpan2	|- ( y e. Univ -> y = ( R1 ` ( y i^i On ) ) )
11	10	adantr	|- ( ( y e. Univ /\ y =/= (/) ) -> y = ( R1 ` ( y i^i On ) ) )
12	8	gruina	|- ( ( y e. Univ /\ y =/= (/) ) -> ( y i^i On ) e. Inacc )
13		inatsk	|- ( ( y i^i On ) e. Inacc -> ( R1 ` ( y i^i On ) ) e. Tarski )
14	12 13	syl	|- ( ( y e. Univ /\ y =/= (/) ) -> ( R1 ` ( y i^i On ) ) e. Tarski )
15	11 14	eqeltrd	|- ( ( y e. Univ /\ y =/= (/) ) -> y e. Tarski )
16	15	ex	|- ( y e. Univ -> ( y =/= (/) -> y e. Tarski ) )
17	4 16	pm2.61dne	|- ( y e. Univ -> y e. Tarski )
18		grutr	|- ( y e. Univ -> Tr y )
19	17 18	jca	|- ( y e. Univ -> ( y e. Tarski /\ Tr y ) )
20		grutsk1	|- ( ( y e. Tarski /\ Tr y ) -> y e. Univ )
21	19 20	impbii	|- ( y e. Univ <-> ( y e. Tarski /\ Tr y ) )
22		treq	|- ( x = y -> ( Tr x <-> Tr y ) )
23	22	elrab	|- ( y e. { x e. Tarski | Tr x } <-> ( y e. Tarski /\ Tr y ) )
24	21 23	bitr4i	|- ( y e. Univ <-> y e. { x e. Tarski | Tr x } )
25	24	eqriv	|- Univ = { x e. Tarski | Tr x }