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

Metamath Proof Explorer

Theorem tskpr

Description: If A and B are members of a Tarski class, their unordered pair is also an element of the class. JFM CLASSES2 th. 3 (partly). (Contributed by FL, 22-Feb-2011) (Proof shortened by Mario Carneiro, 20-Jun-2013)

Ref Expression
Assertion tskpr 
|- ( ( T e. Tarski /\ A e. T /\ B e. T ) -> { A , B } e. T )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( T e. Tarski /\ A e. T /\ B e. T ) -> T e. Tarski )
2 prssi 
 |-  ( ( A e. T /\ B e. T ) -> { A , B } C_ T )
3 2 3adant1 
 |-  ( ( T e. Tarski /\ A e. T /\ B e. T ) -> { A , B } C_ T )
4 prfi 
 |-  { A , B } e. Fin
5 isfinite 
 |-  ( { A , B } e. Fin <-> { A , B } ~< _om )
6 4 5 mpbi 
 |-  { A , B } ~< _om
7 ne0i 
 |-  ( A e. T -> T =/= (/) )
8 tskinf 
 |-  ( ( T e. Tarski /\ T =/= (/) ) -> _om ~<_ T )
9 7 8 sylan2 
 |-  ( ( T e. Tarski /\ A e. T ) -> _om ~<_ T )
10 sdomdomtr 
 |-  ( ( { A , B } ~< _om /\ _om ~<_ T ) -> { A , B } ~< T )
11 6 9 10 sylancr 
 |-  ( ( T e. Tarski /\ A e. T ) -> { A , B } ~< T )
12 11 3adant3 
 |-  ( ( T e. Tarski /\ A e. T /\ B e. T ) -> { A , B } ~< T )
13 tskssel 
 |-  ( ( T e. Tarski /\ { A , B } C_ T /\ { A , B } ~< T ) -> { A , B } e. T )
14 1 3 12 13 syl3anc 
 |-  ( ( T e. Tarski /\ A e. T /\ B e. T ) -> { A , B } e. T )