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