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	⊢ ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ) → 𝑇 ∈ Univ )

Proof

Step	Hyp	Ref	Expression
1		simpr	⊢ ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ) → Tr 𝑇 )
2		tskpw	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑥 ∈ 𝑇 ) → 𝒫 𝑥 ∈ 𝑇 )
3	2	adantlr	⊢ ( ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ) ∧ 𝑥 ∈ 𝑇 ) → 𝒫 𝑥 ∈ 𝑇 )
4		tskpr	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑥 ∈ 𝑇 ∧ 𝑦 ∈ 𝑇 ) → { 𝑥 , 𝑦 } ∈ 𝑇 )
5	4	3expa	⊢ ( ( ( 𝑇 ∈ Tarski ∧ 𝑥 ∈ 𝑇 ) ∧ 𝑦 ∈ 𝑇 ) → { 𝑥 , 𝑦 } ∈ 𝑇 )
6	5	ralrimiva	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑥 ∈ 𝑇 ) → ∀ 𝑦 ∈ 𝑇 { 𝑥 , 𝑦 } ∈ 𝑇 )
7	6	adantlr	⊢ ( ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ) ∧ 𝑥 ∈ 𝑇 ) → ∀ 𝑦 ∈ 𝑇 { 𝑥 , 𝑦 } ∈ 𝑇 )
8		elmapg	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑥 ∈ 𝑇 ) → ( 𝑦 ∈ ( 𝑇 ↑m 𝑥 ) ↔ 𝑦 : 𝑥 ⟶ 𝑇 ) )
9	8	adantlr	⊢ ( ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ) ∧ 𝑥 ∈ 𝑇 ) → ( 𝑦 ∈ ( 𝑇 ↑m 𝑥 ) ↔ 𝑦 : 𝑥 ⟶ 𝑇 ) )
10		tskurn	⊢ ( ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ) ∧ 𝑥 ∈ 𝑇 ∧ 𝑦 : 𝑥 ⟶ 𝑇 ) → ∪ ran 𝑦 ∈ 𝑇 )
11	10	3expia	⊢ ( ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ) ∧ 𝑥 ∈ 𝑇 ) → ( 𝑦 : 𝑥 ⟶ 𝑇 → ∪ ran 𝑦 ∈ 𝑇 ) )
12	9 11	sylbid	⊢ ( ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ) ∧ 𝑥 ∈ 𝑇 ) → ( 𝑦 ∈ ( 𝑇 ↑m 𝑥 ) → ∪ ran 𝑦 ∈ 𝑇 ) )
13	12	ralrimiv	⊢ ( ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ) ∧ 𝑥 ∈ 𝑇 ) → ∀ 𝑦 ∈ ( 𝑇 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑇 )
14	3 7 13	3jca	⊢ ( ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ) ∧ 𝑥 ∈ 𝑇 ) → ( 𝒫 𝑥 ∈ 𝑇 ∧ ∀ 𝑦 ∈ 𝑇 { 𝑥 , 𝑦 } ∈ 𝑇 ∧ ∀ 𝑦 ∈ ( 𝑇 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑇 ) )
15	14	ralrimiva	⊢ ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ) → ∀ 𝑥 ∈ 𝑇 ( 𝒫 𝑥 ∈ 𝑇 ∧ ∀ 𝑦 ∈ 𝑇 { 𝑥 , 𝑦 } ∈ 𝑇 ∧ ∀ 𝑦 ∈ ( 𝑇 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑇 ) )
16		elgrug	⊢ ( 𝑇 ∈ Tarski → ( 𝑇 ∈ Univ ↔ ( Tr 𝑇 ∧ ∀ 𝑥 ∈ 𝑇 ( 𝒫 𝑥 ∈ 𝑇 ∧ ∀ 𝑦 ∈ 𝑇 { 𝑥 , 𝑦 } ∈ 𝑇 ∧ ∀ 𝑦 ∈ ( 𝑇 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑇 ) ) ) )
17	16	adantr	⊢ ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ) → ( 𝑇 ∈ Univ ↔ ( Tr 𝑇 ∧ ∀ 𝑥 ∈ 𝑇 ( 𝒫 𝑥 ∈ 𝑇 ∧ ∀ 𝑦 ∈ 𝑇 { 𝑥 , 𝑦 } ∈ 𝑇 ∧ ∀ 𝑦 ∈ ( 𝑇 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑇 ) ) ) )
18	1 15 17	mpbir2and	⊢ ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ) → 𝑇 ∈ Univ )