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 )