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 )