Metamath Proof Explorer

Theorem tskwun

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

Ref Expression
Assertion tskwun ⊢ T ∈ Tarski ∧ Tr ⁡ T ∧ T ≠ ∅ → T ∈ WUni

Proof

Step Hyp Ref Expression
1 simp2 ⊢ T ∈ Tarski ∧ Tr ⁡ T ∧ T ≠ ∅ → Tr ⁡ T
2 simp3 ⊢ T ∈ Tarski ∧ Tr ⁡ T ∧ T ≠ ∅ → T ≠ ∅
3 tskuni ⊢ T ∈ Tarski ∧ Tr ⁡ T ∧ x ∈ T → ⋃ x ∈ T
4 3 3expa ⊢ T ∈ Tarski ∧ Tr ⁡ T ∧ x ∈ T → ⋃ x ∈ T
5 4 3adantl3 ⊢ T ∈ Tarski ∧ Tr ⁡ T ∧ T ≠ ∅ ∧ x ∈ T → ⋃ x ∈ T
6 tskpw ⊢ T ∈ Tarski ∧ x ∈ T → 𝒫 x ∈ T
7 6 3ad2antl1 ⊢ T ∈ Tarski ∧ Tr ⁡ T ∧ T ≠ ∅ ∧ x ∈ T → 𝒫 x ∈ T
8 tskpr ⊢ T ∈ Tarski ∧ x ∈ T ∧ y ∈ T → x y ∈ T
9 8 3exp ⊢ T ∈ Tarski → x ∈ T → y ∈ T → x y ∈ T
10 9 3ad2ant1 ⊢ T ∈ Tarski ∧ Tr ⁡ T ∧ T ≠ ∅ → x ∈ T → y ∈ T → x y ∈ T
11 10 imp31 ⊢ T ∈ Tarski ∧ Tr ⁡ T ∧ T ≠ ∅ ∧ x ∈ T ∧ y ∈ T → x y ∈ T
12 11 ralrimiva ⊢ T ∈ Tarski ∧ Tr ⁡ T ∧ T ≠ ∅ ∧ x ∈ T → ∀ y ∈ T x y ∈ T
13 5 7 12 3jca ⊢ T ∈ Tarski ∧ Tr ⁡ T ∧ T ≠ ∅ ∧ x ∈ T → ⋃ x ∈ T ∧ 𝒫 x ∈ T ∧ ∀ y ∈ T x y ∈ T
14 13 ralrimiva ⊢ T ∈ Tarski ∧ Tr ⁡ T ∧ T ≠ ∅ → ∀ x ∈ T ⋃ x ∈ T ∧ 𝒫 x ∈ T ∧ ∀ y ∈ T x y ∈ T
15 iswun ⊢ T ∈ Tarski → T ∈ WUni ↔ Tr ⁡ T ∧ T ≠ ∅ ∧ ∀ x ∈ T ⋃ x ∈ T ∧ 𝒫 x ∈ T ∧ ∀ y ∈ T x y ∈ T
16 15 3ad2ant1 ⊢ T ∈ Tarski ∧ Tr ⁡ T ∧ T ≠ ∅ → T ∈ WUni ↔ Tr ⁡ T ∧ T ≠ ∅ ∧ ∀ x ∈ T ⋃ x ∈ T ∧ 𝒫 x ∈ T ∧ ∀ y ∈ T x y ∈ T
17 1 2 14 16 mpbir3and ⊢ T ∈ Tarski ∧ Tr ⁡ T ∧ T ≠ ∅ → T ∈ WUni