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

Metamath Proof Explorer

Theorem tskmap

Description: Set exponentiation is an element of a transitive Tarski class. JFM CLASSES2 th. 67 (partly). (Contributed by FL, 15-Apr-2011) (Proof shortened by Mario Carneiro, 20-Sep-2014)

Ref Expression
Assertion tskmap 
|- ( ( ( T e. Tarski /\ Tr T ) /\ A e. T /\ B e. T ) -> ( A ^m B ) e. T )

Proof

Step Hyp Ref Expression
1 ne0i 
 |-  ( A e. T -> T =/= (/) )
2 tskwun 
 |-  ( ( T e. Tarski /\ Tr T /\ T =/= (/) ) -> T e. WUni )
3 2 3expa 
 |-  ( ( ( T e. Tarski /\ Tr T ) /\ T =/= (/) ) -> T e. WUni )
4 1 3 sylan2 
 |-  ( ( ( T e. Tarski /\ Tr T ) /\ A e. T ) -> T e. WUni )
5 4 3adant3 
 |-  ( ( ( T e. Tarski /\ Tr T ) /\ A e. T /\ B e. T ) -> T e. WUni )
6 simp2 
 |-  ( ( ( T e. Tarski /\ Tr T ) /\ A e. T /\ B e. T ) -> A e. T )
7 simp3 
 |-  ( ( ( T e. Tarski /\ Tr T ) /\ A e. T /\ B e. T ) -> B e. T )
8 5 6 7 wunmap 
 |-  ( ( ( T e. Tarski /\ Tr T ) /\ A e. T /\ B e. T ) -> ( A ^m B ) e. T )