Theorem tskun

Description: The union of two elements of a transitive Tarski class is in the set. (Contributed by Mario Carneiro, 20-Sep-2014)

	Ref	Expression
Assertion	tskun	|- ( ( ( T e. Tarski /\ Tr T ) /\ A e. T /\ B e. T ) -> ( A u. B ) e. T )

Proof

Step	Hyp	Ref	Expression
1		uniprg	|- ( ( A e. T /\ B e. T ) -> U. { A , B } = ( A u. B ) )
2	1	3adant1	|- ( ( ( T e. Tarski /\ Tr T ) /\ A e. T /\ B e. T ) -> U. { A , B } = ( A u. B ) )
3		simp1l	|- ( ( ( T e. Tarski /\ Tr T ) /\ A e. T /\ B e. T ) -> T e. Tarski )
4		simp1r	|- ( ( ( T e. Tarski /\ Tr T ) /\ A e. T /\ B e. T ) -> Tr T )
5		tskpr	|- ( ( T e. Tarski /\ A e. T /\ B e. T ) -> { A , B } e. T )
6	5	3adant1r	|- ( ( ( T e. Tarski /\ Tr T ) /\ A e. T /\ B e. T ) -> { A , B } e. T )
7		tskuni	|- ( ( T e. Tarski /\ Tr T /\ { A , B } e. T ) -> U. { A , B } e. T )
8	3 4 6 7	syl3anc	|- ( ( ( T e. Tarski /\ Tr T ) /\ A e. T /\ B e. T ) -> U. { A , B } e. T )
9	2 8	eqeltrrd	|- ( ( ( T e. Tarski /\ Tr T ) /\ A e. T /\ B e. T ) -> ( A u. B ) e. T )