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

Metamath Proof Explorer

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 )