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	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇 ∧ 𝐵 ∈ 𝑇 ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑇 )

Proof

Step	Hyp	Ref	Expression
1		dfopg	⊢ ( ( 𝐴 ∈ 𝑇 ∧ 𝐵 ∈ 𝑇 ) → ⟨ 𝐴 , 𝐵 ⟩ = { { 𝐴 } , { 𝐴 , 𝐵 } } )
2	1	3adant1	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇 ∧ 𝐵 ∈ 𝑇 ) → ⟨ 𝐴 , 𝐵 ⟩ = { { 𝐴 } , { 𝐴 , 𝐵 } } )
3		simp1	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇 ∧ 𝐵 ∈ 𝑇 ) → 𝑇 ∈ Tarski )
4		tsksn	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇 ) → { 𝐴 } ∈ 𝑇 )
5	4	3adant3	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇 ∧ 𝐵 ∈ 𝑇 ) → { 𝐴 } ∈ 𝑇 )
6		tskpr	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇 ∧ 𝐵 ∈ 𝑇 ) → { 𝐴 , 𝐵 } ∈ 𝑇 )
7		tskpr	⊢ ( ( 𝑇 ∈ Tarski ∧ { 𝐴 } ∈ 𝑇 ∧ { 𝐴 , 𝐵 } ∈ 𝑇 ) → { { 𝐴 } , { 𝐴 , 𝐵 } } ∈ 𝑇 )
8	3 5 6 7	syl3anc	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇 ∧ 𝐵 ∈ 𝑇 ) → { { 𝐴 } , { 𝐴 , 𝐵 } } ∈ 𝑇 )
9	2 8	eqeltrd	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇 ∧ 𝐵 ∈ 𝑇 ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑇 )