Theorem tskwun

Description: A nonempty transitive Tarski class is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Assertion	tskwun	⊢ ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝑇 ≠ ∅ ) → 𝑇 ∈ WUni )

Proof

Step	Hyp	Ref	Expression
1		simp2	⊢ ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝑇 ≠ ∅ ) → Tr 𝑇 )
2		simp3	⊢ ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝑇 ≠ ∅ ) → 𝑇 ≠ ∅ )
3		tskuni	⊢ ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝑥 ∈ 𝑇 ) → ∪ 𝑥 ∈ 𝑇 )
4	3	3expa	⊢ ( ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ) ∧ 𝑥 ∈ 𝑇 ) → ∪ 𝑥 ∈ 𝑇 )
5	4	3adantl3	⊢ ( ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝑇 ≠ ∅ ) ∧ 𝑥 ∈ 𝑇 ) → ∪ 𝑥 ∈ 𝑇 )
6		tskpw	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑥 ∈ 𝑇 ) → 𝒫 𝑥 ∈ 𝑇 )
7	6	3ad2antl1	⊢ ( ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝑇 ≠ ∅ ) ∧ 𝑥 ∈ 𝑇 ) → 𝒫 𝑥 ∈ 𝑇 )
8		tskpr	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑥 ∈ 𝑇 ∧ 𝑦 ∈ 𝑇 ) → { 𝑥 , 𝑦 } ∈ 𝑇 )
9	8	3exp	⊢ ( 𝑇 ∈ Tarski → ( 𝑥 ∈ 𝑇 → ( 𝑦 ∈ 𝑇 → { 𝑥 , 𝑦 } ∈ 𝑇 ) ) )
10	9	3ad2ant1	⊢ ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝑇 ≠ ∅ ) → ( 𝑥 ∈ 𝑇 → ( 𝑦 ∈ 𝑇 → { 𝑥 , 𝑦 } ∈ 𝑇 ) ) )
11	10	imp31	⊢ ( ( ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝑇 ≠ ∅ ) ∧ 𝑥 ∈ 𝑇 ) ∧ 𝑦 ∈ 𝑇 ) → { 𝑥 , 𝑦 } ∈ 𝑇 )
12	11	ralrimiva	⊢ ( ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝑇 ≠ ∅ ) ∧ 𝑥 ∈ 𝑇 ) → ∀ 𝑦 ∈ 𝑇 { 𝑥 , 𝑦 } ∈ 𝑇 )
13	5 7 12	3jca	⊢ ( ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝑇 ≠ ∅ ) ∧ 𝑥 ∈ 𝑇 ) → ( ∪ 𝑥 ∈ 𝑇 ∧ 𝒫 𝑥 ∈ 𝑇 ∧ ∀ 𝑦 ∈ 𝑇 { 𝑥 , 𝑦 } ∈ 𝑇 ) )
14	13	ralrimiva	⊢ ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝑇 ≠ ∅ ) → ∀ 𝑥 ∈ 𝑇 ( ∪ 𝑥 ∈ 𝑇 ∧ 𝒫 𝑥 ∈ 𝑇 ∧ ∀ 𝑦 ∈ 𝑇 { 𝑥 , 𝑦 } ∈ 𝑇 ) )
15		iswun	⊢ ( 𝑇 ∈ Tarski → ( 𝑇 ∈ WUni ↔ ( Tr 𝑇 ∧ 𝑇 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑇 ( ∪ 𝑥 ∈ 𝑇 ∧ 𝒫 𝑥 ∈ 𝑇 ∧ ∀ 𝑦 ∈ 𝑇 { 𝑥 , 𝑦 } ∈ 𝑇 ) ) ) )
16	15	3ad2ant1	⊢ ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝑇 ≠ ∅ ) → ( 𝑇 ∈ WUni ↔ ( Tr 𝑇 ∧ 𝑇 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑇 ( ∪ 𝑥 ∈ 𝑇 ∧ 𝒫 𝑥 ∈ 𝑇 ∧ ∀ 𝑦 ∈ 𝑇 { 𝑥 , 𝑦 } ∈ 𝑇 ) ) ) )
17	1 2 14 16	mpbir3and	⊢ ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝑇 ≠ ∅ ) → 𝑇 ∈ WUni )