This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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