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 ∈ Tarski ∧ A ∈ T ∧ B ∈ T → A B ∈ T

Proof

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