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