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

Metamath Proof Explorer

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 )