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

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (T \in Tarski \land A \in T \land B \in T) \to T \in Tarski$
2		prssi	$⊢ (A \in T \land B \in T) \to \{A, B\} \subseteq T$
3	2	3adant1	$⊢ (T \in Tarski \land A \in T \land B \in T) \to \{A, B\} \subseteq T$
4		prfi	$⊢ \{A, B\} \in Fin$
5		isfinite	$⊢ \{A, B\} \in Fin \leftrightarrow \{A, B\} ≺ ω$
6	4 5	mpbi	$⊢ \{A, B\} ≺ ω$
7		ne0i	$⊢ A \in T \to T \neq \emptyset$
8		tskinf	$⊢ (T \in Tarski \land T \neq \emptyset) \to ω ≼ T$
9	7 8	sylan2	$⊢ (T \in Tarski \land A \in T) \to ω ≼ T$
10		sdomdomtr	$⊢ (\{A, B\} ≺ ω \land ω ≼ T) \to \{A, B\} ≺ T$
11	6 9 10	sylancr	$⊢ (T \in Tarski \land A \in T) \to \{A, B\} ≺ T$
12	11	3adant3	$⊢ (T \in Tarski \land A \in T \land B \in T) \to \{A, B\} ≺ T$
13		tskssel	$⊢ (T \in Tarski \land \{A, B\} \subseteq T \land \{A, B\} ≺ T) \to \{A, B\} \in T$
14	1 3 12 13	syl3anc	$⊢ (T \in Tarski \land A \in T \land B \in T) \to \{A, B\} \in T$