This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝑇 ∈ 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 )