Theorem tskwun

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

	Ref	Expression
Assertion	tskwun	|- ( ( T e. Tarski /\ Tr T /\ T =/= (/) ) -> T e. WUni )

Proof

Step	Hyp	Ref	Expression
1		simp2	|- ( ( T e. Tarski /\ Tr T /\ T =/= (/) ) -> Tr T )
2		simp3	|- ( ( T e. Tarski /\ Tr T /\ T =/= (/) ) -> T =/= (/) )
3		tskuni	|- ( ( T e. Tarski /\ Tr T /\ x e. T ) -> U. x e. T )
4	3	3expa	|- ( ( ( T e. Tarski /\ Tr T ) /\ x e. T ) -> U. x e. T )
5	4	3adantl3	|- ( ( ( T e. Tarski /\ Tr T /\ T =/= (/) ) /\ x e. T ) -> U. x e. T )
6		tskpw	|- ( ( T e. Tarski /\ x e. T ) -> ~P x e. T )
7	6	3ad2antl1	|- ( ( ( T e. Tarski /\ Tr T /\ T =/= (/) ) /\ x e. T ) -> ~P x e. T )
8		tskpr	|- ( ( T e. Tarski /\ x e. T /\ y e. T ) -> { x , y } e. T )
9	8	3exp	|- ( T e. Tarski -> ( x e. T -> ( y e. T -> { x , y } e. T ) ) )
10	9	3ad2ant1	|- ( ( T e. Tarski /\ Tr T /\ T =/= (/) ) -> ( x e. T -> ( y e. T -> { x , y } e. T ) ) )
11	10	imp31	|- ( ( ( ( T e. Tarski /\ Tr T /\ T =/= (/) ) /\ x e. T ) /\ y e. T ) -> { x , y } e. T )
12	11	ralrimiva	|- ( ( ( T e. Tarski /\ Tr T /\ T =/= (/) ) /\ x e. T ) -> A. y e. T { x , y } e. T )
13	5 7 12	3jca	|- ( ( ( T e. Tarski /\ Tr T /\ T =/= (/) ) /\ x e. T ) -> ( U. x e. T /\ ~P x e. T /\ A. y e. T { x , y } e. T ) )
14	13	ralrimiva	|- ( ( T e. Tarski /\ Tr T /\ T =/= (/) ) -> A. x e. T ( U. x e. T /\ ~P x e. T /\ A. y e. T { x , y } e. T ) )
15		iswun	|- ( T e. Tarski -> ( T e. WUni <-> ( Tr T /\ T =/= (/) /\ A. x e. T ( U. x e. T /\ ~P x e. T /\ A. y e. T { x , y } e. T ) ) ) )
16	15	3ad2ant1	|- ( ( T e. Tarski /\ Tr T /\ T =/= (/) ) -> ( T e. WUni <-> ( Tr T /\ T =/= (/) /\ A. x e. T ( U. x e. T /\ ~P x e. T /\ A. y e. T { x , y } e. T ) ) ) )
17	1 2 14 16	mpbir3and	|- ( ( T e. Tarski /\ Tr T /\ T =/= (/) ) -> T e. WUni )