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

Proof

Step	Hyp	Ref	Expression
1		simp1	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇 ∧ 𝐵 ∈ 𝑇 ) → 𝑇 ∈ Tarski )
2		prssi	⊢ ( ( 𝐴 ∈ 𝑇 ∧ 𝐵 ∈ 𝑇 ) → { 𝐴 , 𝐵 } ⊆ 𝑇 )
3	2	3adant1	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇 ∧ 𝐵 ∈ 𝑇 ) → { 𝐴 , 𝐵 } ⊆ 𝑇 )
4		prfi	⊢ { 𝐴 , 𝐵 } ∈ Fin
5		isfinite	⊢ ( { 𝐴 , 𝐵 } ∈ Fin ↔ { 𝐴 , 𝐵 } ≺ ω )
6	4 5	mpbi	⊢ { 𝐴 , 𝐵 } ≺ ω
7		ne0i	⊢ ( 𝐴 ∈ 𝑇 → 𝑇 ≠ ∅ )
8		tskinf	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) → ω ≼ 𝑇 )
9	7 8	sylan2	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇 ) → ω ≼ 𝑇 )
10		sdomdomtr	⊢ ( ( { 𝐴 , 𝐵 } ≺ ω ∧ ω ≼ 𝑇 ) → { 𝐴 , 𝐵 } ≺ 𝑇 )
11	6 9 10	sylancr	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇 ) → { 𝐴 , 𝐵 } ≺ 𝑇 )
12	11	3adant3	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇 ∧ 𝐵 ∈ 𝑇 ) → { 𝐴 , 𝐵 } ≺ 𝑇 )
13		tskssel	⊢ ( ( 𝑇 ∈ Tarski ∧ { 𝐴 , 𝐵 } ⊆ 𝑇 ∧ { 𝐴 , 𝐵 } ≺ 𝑇 ) → { 𝐴 , 𝐵 } ∈ 𝑇 )
14	1 3 12 13	syl3anc	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇 ∧ 𝐵 ∈ 𝑇 ) → { 𝐴 , 𝐵 } ∈ 𝑇 )