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 \in Tarski \land Tr T) \land A \in T \land B \in T) \to A^{B} \in T$

Proof

Step	Hyp	Ref	Expression
1		ne0i	$⊢ A \in T \to T \neq \emptyset$
2		tskwun	$⊢ (T \in Tarski \land Tr T \land T \neq \emptyset) \to T \in WUni$
3	2	3expa	$⊢ ((T \in Tarski \land Tr T) \land T \neq \emptyset) \to T \in WUni$
4	1 3	sylan2	$⊢ ((T \in Tarski \land Tr T) \land A \in T) \to T \in WUni$
5	4	3adant3	$⊢ ((T \in Tarski \land Tr T) \land A \in T \land B \in T) \to T \in WUni$
6		simp2	$⊢ ((T \in Tarski \land Tr T) \land A \in T \land B \in T) \to A \in T$
7		simp3	$⊢ ((T \in Tarski \land Tr T) \land A \in T \land B \in T) \to B \in T$
8	5 6 7	wunmap	$⊢ ((T \in Tarski \land Tr T) \land A \in T \land B \in T) \to A^{B} \in T$