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 \in Tarski \| Tr x\}$

Proof

Step	Hyp	Ref	Expression
1		0tsk	$⊢ \emptyset \in Tarski$
2		eleq1	$⊢ y = \emptyset \to (y \in Tarski \leftrightarrow \emptyset \in Tarski)$
3	1 2	mpbiri	$⊢ y = \emptyset \to y \in Tarski$
4	3	a1i	$⊢ y \in Univ \to (y = \emptyset \to y \in Tarski)$
5		vex	$⊢ y \in V$
6		unir1	$⊢ ⋃ R_{1} [On] = V$
7	5 6	eleqtrri	$⊢ y \in ⋃ R_{1} [On]$
8		eqid	$⊢ y \cap On = y \cap On$
9	8	grur1	$⊢ (y \in Univ \land y \in ⋃ R_{1} [On]) \to y = R_{1} (y \cap On)$
10	7 9	mpan2	$⊢ y \in Univ \to y = R_{1} (y \cap On)$
11	10	adantr	$⊢ (y \in Univ \land y \neq \emptyset) \to y = R_{1} (y \cap On)$
12	8	gruina	$⊢ (y \in Univ \land y \neq \emptyset) \to y \cap On \in Inacc$
13		inatsk	$⊢ y \cap On \in Inacc \to R_{1} (y \cap On) \in Tarski$
14	12 13	syl	$⊢ (y \in Univ \land y \neq \emptyset) \to R_{1} (y \cap On) \in Tarski$
15	11 14	eqeltrd	$⊢ (y \in Univ \land y \neq \emptyset) \to y \in Tarski$
16	15	ex	$⊢ y \in Univ \to (y \neq \emptyset \to y \in Tarski)$
17	4 16	pm2.61dne	$⊢ y \in Univ \to y \in Tarski$
18		grutr	$⊢ y \in Univ \to Tr y$
19	17 18	jca	$⊢ y \in Univ \to (y \in Tarski \land Tr y)$
20		grutsk1	$⊢ (y \in Tarski \land Tr y) \to y \in Univ$
21	19 20	impbii	$⊢ y \in Univ \leftrightarrow (y \in Tarski \land Tr y)$
22		treq	$⊢ x = y \to (Tr x \leftrightarrow Tr y)$
23	22	elrab	$⊢ y \in \{x \in Tarski \| Tr x\} \leftrightarrow (y \in Tarski \land Tr y)$
24	21 23	bitr4i	$⊢ y \in Univ \leftrightarrow y \in \{x \in Tarski \| Tr x\}$
25	24	eqriv	$⊢ Univ = \{x \in Tarski \| Tr x\}$

Metamath Proof Explorer

Theorem grutsk

Proof