Metamath Proof Explorer

Theorem tsken

Description: Third axiom of a Tarski class. A subset of a Tarski class is either equipotent to the class or an element of the class. (Contributed by FL, 30-Dec-2010) (Revised by Mario Carneiro, 20-Sep-2014)

Ref Expression
Assertion tsken ⊢ T ∈ Tarski ∧ A ⊆ T → A ≈ T ∨ A ∈ T

Proof

Step Hyp Ref Expression
1 eltskg ⊢ T ∈ Tarski → T ∈ Tarski ↔ ∀ x ∈ T 𝒫 x ⊆ T ∧ ∃ y ∈ T 𝒫 x ⊆ y ∧ ∀ x ∈ 𝒫 T x ≈ T ∨ x ∈ T
2 1 ibi ⊢ T ∈ Tarski → ∀ x ∈ T 𝒫 x ⊆ T ∧ ∃ y ∈ T 𝒫 x ⊆ y ∧ ∀ x ∈ 𝒫 T x ≈ T ∨ x ∈ T
3 2 simprd ⊢ T ∈ Tarski → ∀ x ∈ 𝒫 T x ≈ T ∨ x ∈ T
4 elpw2g ⊢ T ∈ Tarski → A ∈ 𝒫 T ↔ A ⊆ T
5 4 biimpar ⊢ T ∈ Tarski ∧ A ⊆ T → A ∈ 𝒫 T
6 breq1 ⊢ x = A → x ≈ T ↔ A ≈ T
7 eleq1 ⊢ x = A → x ∈ T ↔ A ∈ T
8 6 7 orbi12d ⊢ x = A → x ≈ T ∨ x ∈ T ↔ A ≈ T ∨ A ∈ T
9 8 rspccva ⊢ ∀ x ∈ 𝒫 T x ≈ T ∨ x ∈ T ∧ A ∈ 𝒫 T → A ≈ T ∨ A ∈ T
10 3 5 9 syl2an2r ⊢ T ∈ Tarski ∧ A ⊆ T → A ≈ T ∨ A ∈ T