Metamath Proof Explorer

Theorem tskop

Description: If A and B are members of a Tarski class, their ordered pair is also an element of the class. JFM CLASSES2 th. 4. (Contributed by FL, 22-Feb-2011)

		Ref	Expression
	Assertion	tskop	$⊢ (T \in Tarski \land A \in T \land B \in T) \to ⟨A, B⟩ \in T$

Proof

Step	Hyp	Ref	Expression
1		dfopg	$⊢ (A \in T \land B \in T) \to ⟨A, B⟩ = \{\{A\}, \{A, B\}\}$
2	1	3adant1	$⊢ (T \in Tarski \land A \in T \land B \in T) \to ⟨A, B⟩ = \{\{A\}, \{A, B\}\}$
3		simp1	$⊢ (T \in Tarski \land A \in T \land B \in T) \to T \in Tarski$
4		tsksn	$⊢ (T \in Tarski \land A \in T) \to \{A\} \in T$
5	4	3adant3	$⊢ (T \in Tarski \land A \in T \land B \in T) \to \{A\} \in T$
6		tskpr	$⊢ (T \in Tarski \land A \in T \land B \in T) \to \{A, B\} \in T$
7		tskpr	$⊢ (T \in Tarski \land \{A\} \in T \land \{A, B\} \in T) \to \{\{A\}, \{A, B\}\} \in T$
8	3 5 6 7	syl3anc	$⊢ (T \in Tarski \land A \in T \land B \in T) \to \{\{A\}, \{A, B\}\} \in T$
9	2 8	eqeltrd	$⊢ (T \in Tarski \land A \in T \land B \in T) \to ⟨A, B⟩ \in T$