Metamath Proof Explorer

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 \in Tarski \land Tr T) \to T \in Univ$

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ (T \in Tarski \land Tr T) \to Tr T$
2		tskpw	$⊢ (T \in Tarski \land x \in T) \to 𝒫 x \in T$
3	2	adantlr	$⊢ ((T \in Tarski \land Tr T) \land x \in T) \to 𝒫 x \in T$
4		tskpr	$⊢ (T \in Tarski \land x \in T \land y \in T) \to \{x, y\} \in T$
5	4	3expa	$⊢ ((T \in Tarski \land x \in T) \land y \in T) \to \{x, y\} \in T$
6	5	ralrimiva	$⊢ (T \in Tarski \land x \in T) \to \forall y \in T \{x, y\} \in T$
7	6	adantlr	$⊢ ((T \in Tarski \land Tr T) \land x \in T) \to \forall y \in T \{x, y\} \in T$
8		elmapg	$⊢ (T \in Tarski \land x \in T) \to (y \in (T^{x}) \leftrightarrow y : x ⟶ T)$
9	8	adantlr	$⊢ ((T \in Tarski \land Tr T) \land x \in T) \to (y \in (T^{x}) \leftrightarrow y : x ⟶ T)$
10		tskurn	$⊢ ((T \in Tarski \land Tr T) \land x \in T \land y : x ⟶ T) \to ⋃ ran y \in T$
11	10	3expia	$⊢ ((T \in Tarski \land Tr T) \land x \in T) \to (y : x ⟶ T \to ⋃ ran y \in T)$
12	9 11	sylbid	$⊢ ((T \in Tarski \land Tr T) \land x \in T) \to (y \in (T^{x}) \to ⋃ ran y \in T)$
13	12	ralrimiv	$⊢ ((T \in Tarski \land Tr T) \land x \in T) \to \forall y \in (T^{x}) ⋃ ran y \in T$
14	3 7 13	3jca	$⊢ ((T \in Tarski \land Tr T) \land x \in T) \to (𝒫 x \in T \land \forall y \in T \{x, y\} \in T \land \forall y \in (T^{x}) ⋃ ran y \in T)$
15	14	ralrimiva	$⊢ (T \in Tarski \land Tr T) \to \forall x \in T (𝒫 x \in T \land \forall y \in T \{x, y\} \in T \land \forall y \in (T^{x}) ⋃ ran y \in T)$
16		elgrug	$⊢ T \in Tarski \to (T \in Univ \leftrightarrow (Tr T \land \forall x \in T (𝒫 x \in T \land \forall y \in T \{x, y\} \in T \land \forall y \in (T^{x}) ⋃ ran y \in T)))$
17	16	adantr	$⊢ (T \in Tarski \land Tr T) \to (T \in Univ \leftrightarrow (Tr T \land \forall x \in T (𝒫 x \in T \land \forall y \in T \{x, y\} \in T \land \forall y \in (T^{x}) ⋃ ran y \in T)))$
18	1 15 17	mpbir2and	$⊢ (T \in Tarski \land Tr T) \to T \in Univ$