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 = { 𝑥 ∈ Tarski ∣ Tr 𝑥 }

Proof

Step	Hyp	Ref	Expression
1		0tsk	⊢ ∅ ∈ Tarski
2		eleq1	⊢ ( 𝑦 = ∅ → ( 𝑦 ∈ Tarski ↔ ∅ ∈ Tarski ) )
3	1 2	mpbiri	⊢ ( 𝑦 = ∅ → 𝑦 ∈ Tarski )
4	3	a1i	⊢ ( 𝑦 ∈ Univ → ( 𝑦 = ∅ → 𝑦 ∈ Tarski ) )
5		vex	⊢ 𝑦 ∈ V
6		unir1	⊢ ∪ ( 𝑅1 “ On ) = V
7	5 6	eleqtrri	⊢ 𝑦 ∈ ∪ ( 𝑅1 “ On )
8		eqid	⊢ ( 𝑦 ∩ On ) = ( 𝑦 ∩ On )
9	8	grur1	⊢ ( ( 𝑦 ∈ Univ ∧ 𝑦 ∈ ∪ ( 𝑅1 “ On ) ) → 𝑦 = ( 𝑅1 ‘ ( 𝑦 ∩ On ) ) )
10	7 9	mpan2	⊢ ( 𝑦 ∈ Univ → 𝑦 = ( 𝑅1 ‘ ( 𝑦 ∩ On ) ) )
11	10	adantr	⊢ ( ( 𝑦 ∈ Univ ∧ 𝑦 ≠ ∅ ) → 𝑦 = ( 𝑅1 ‘ ( 𝑦 ∩ On ) ) )
12	8	gruina	⊢ ( ( 𝑦 ∈ Univ ∧ 𝑦 ≠ ∅ ) → ( 𝑦 ∩ On ) ∈ Inacc )
13		inatsk	⊢ ( ( 𝑦 ∩ On ) ∈ Inacc → ( 𝑅1 ‘ ( 𝑦 ∩ On ) ) ∈ Tarski )
14	12 13	syl	⊢ ( ( 𝑦 ∈ Univ ∧ 𝑦 ≠ ∅ ) → ( 𝑅1 ‘ ( 𝑦 ∩ On ) ) ∈ Tarski )
15	11 14	eqeltrd	⊢ ( ( 𝑦 ∈ Univ ∧ 𝑦 ≠ ∅ ) → 𝑦 ∈ Tarski )
16	15	ex	⊢ ( 𝑦 ∈ Univ → ( 𝑦 ≠ ∅ → 𝑦 ∈ Tarski ) )
17	4 16	pm2.61dne	⊢ ( 𝑦 ∈ Univ → 𝑦 ∈ Tarski )
18		grutr	⊢ ( 𝑦 ∈ Univ → Tr 𝑦 )
19	17 18	jca	⊢ ( 𝑦 ∈ Univ → ( 𝑦 ∈ Tarski ∧ Tr 𝑦 ) )
20		grutsk1	⊢ ( ( 𝑦 ∈ Tarski ∧ Tr 𝑦 ) → 𝑦 ∈ Univ )
21	19 20	impbii	⊢ ( 𝑦 ∈ Univ ↔ ( 𝑦 ∈ Tarski ∧ Tr 𝑦 ) )
22		treq	⊢ ( 𝑥 = 𝑦 → ( Tr 𝑥 ↔ Tr 𝑦 ) )
23	22	elrab	⊢ ( 𝑦 ∈ { 𝑥 ∈ Tarski ∣ Tr 𝑥 } ↔ ( 𝑦 ∈ Tarski ∧ Tr 𝑦 ) )
24	21 23	bitr4i	⊢ ( 𝑦 ∈ Univ ↔ 𝑦 ∈ { 𝑥 ∈ Tarski ∣ Tr 𝑥 } )
25	24	eqriv	⊢ Univ = { 𝑥 ∈ Tarski ∣ Tr 𝑥 }