Theorem tskwe2

Description: A Tarski class is well-orderable. (Contributed by Mario Carneiro, 20-Jun-2013)

	Ref	Expression
Assertion	tskwe2	⊢ ( 𝑇 ∈ Tarski → 𝑇 ∈ dom card )

Proof

Step	Hyp	Ref	Expression
1		elpwi	⊢ ( 𝑦 ∈ 𝒫 𝑇 → 𝑦 ⊆ 𝑇 )
2		tskssel	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑦 ⊆ 𝑇 ∧ 𝑦 ≺ 𝑇 ) → 𝑦 ∈ 𝑇 )
3	2	3exp	⊢ ( 𝑇 ∈ Tarski → ( 𝑦 ⊆ 𝑇 → ( 𝑦 ≺ 𝑇 → 𝑦 ∈ 𝑇 ) ) )
4	1 3	syl5	⊢ ( 𝑇 ∈ Tarski → ( 𝑦 ∈ 𝒫 𝑇 → ( 𝑦 ≺ 𝑇 → 𝑦 ∈ 𝑇 ) ) )
5	4	ralrimiv	⊢ ( 𝑇 ∈ Tarski → ∀ 𝑦 ∈ 𝒫 𝑇 ( 𝑦 ≺ 𝑇 → 𝑦 ∈ 𝑇 ) )
6		rabss	⊢ ( { 𝑦 ∈ 𝒫 𝑇 ∣ 𝑦 ≺ 𝑇 } ⊆ 𝑇 ↔ ∀ 𝑦 ∈ 𝒫 𝑇 ( 𝑦 ≺ 𝑇 → 𝑦 ∈ 𝑇 ) )
7	5 6	sylibr	⊢ ( 𝑇 ∈ Tarski → { 𝑦 ∈ 𝒫 𝑇 ∣ 𝑦 ≺ 𝑇 } ⊆ 𝑇 )
8		tskwe	⊢ ( ( 𝑇 ∈ Tarski ∧ { 𝑦 ∈ 𝒫 𝑇 ∣ 𝑦 ≺ 𝑇 } ⊆ 𝑇 ) → 𝑇 ∈ dom card )
9	7 8	mpdan	⊢ ( 𝑇 ∈ Tarski → 𝑇 ∈ dom card )