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

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	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝐴 ⊆ 𝑇 ) → ( 𝐴 ≈ 𝑇 ∨ 𝐴 ∈ 𝑇 ) )

Proof

Step	Hyp	Ref	Expression
1		eltskg	⊢ ( 𝑇 ∈ Tarski → ( 𝑇 ∈ Tarski ↔ ( ∀ 𝑥 ∈ 𝑇 ( 𝒫 𝑥 ⊆ 𝑇 ∧ ∃ 𝑦 ∈ 𝑇 𝒫 𝑥 ⊆ 𝑦 ) ∧ ∀ 𝑥 ∈ 𝒫 𝑇 ( 𝑥 ≈ 𝑇 ∨ 𝑥 ∈ 𝑇 ) ) ) )
2	1	ibi	⊢ ( 𝑇 ∈ Tarski → ( ∀ 𝑥 ∈ 𝑇 ( 𝒫 𝑥 ⊆ 𝑇 ∧ ∃ 𝑦 ∈ 𝑇 𝒫 𝑥 ⊆ 𝑦 ) ∧ ∀ 𝑥 ∈ 𝒫 𝑇 ( 𝑥 ≈ 𝑇 ∨ 𝑥 ∈ 𝑇 ) ) )
3	2	simprd	⊢ ( 𝑇 ∈ Tarski → ∀ 𝑥 ∈ 𝒫 𝑇 ( 𝑥 ≈ 𝑇 ∨ 𝑥 ∈ 𝑇 ) )
4		elpw2g	⊢ ( 𝑇 ∈ Tarski → ( 𝐴 ∈ 𝒫 𝑇 ↔ 𝐴 ⊆ 𝑇 ) )
5	4	biimpar	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝐴 ⊆ 𝑇 ) → 𝐴 ∈ 𝒫 𝑇 )
6		breq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ≈ 𝑇 ↔ 𝐴 ≈ 𝑇 ) )
7		eleq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ 𝑇 ↔ 𝐴 ∈ 𝑇 ) )
8	6 7	orbi12d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ≈ 𝑇 ∨ 𝑥 ∈ 𝑇 ) ↔ ( 𝐴 ≈ 𝑇 ∨ 𝐴 ∈ 𝑇 ) ) )
9	8	rspccva	⊢ ( ( ∀ 𝑥 ∈ 𝒫 𝑇 ( 𝑥 ≈ 𝑇 ∨ 𝑥 ∈ 𝑇 ) ∧ 𝐴 ∈ 𝒫 𝑇 ) → ( 𝐴 ≈ 𝑇 ∨ 𝐴 ∈ 𝑇 ) )
10	3 5 9	syl2an2r	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝐴 ⊆ 𝑇 ) → ( 𝐴 ≈ 𝑇 ∨ 𝐴 ∈ 𝑇 ) )