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 Tarski Tr T A T B T A B T

Proof

Step Hyp Ref Expression
1 ne0i A T T
2 tskwun T Tarski Tr T T T WUni
3 2 3expa T Tarski Tr T T T WUni
4 1 3 sylan2 T Tarski Tr T A T T WUni
5 4 3adant3 T Tarski Tr T A T B T T WUni
6 simp2 T Tarski Tr T A T B T A T
7 simp3 T Tarski Tr T A T B T B T
8 5 6 7 wunmap T Tarski Tr T A T B T A B T