Theorem eltskg

Description: Properties of a Tarski class. (Contributed by FL, 30-Dec-2010)

	Ref	Expression
Assertion	eltskg	⊢ ( 𝑇 ∈ 𝑉 → ( 𝑇 ∈ Tarski ↔ ( ∀ 𝑧 ∈ 𝑇 ( 𝒫 𝑧 ⊆ 𝑇 ∧ ∃ 𝑤 ∈ 𝑇 𝒫 𝑧 ⊆ 𝑤 ) ∧ ∀ 𝑧 ∈ 𝒫 𝑇 ( 𝑧 ≈ 𝑇 ∨ 𝑧 ∈ 𝑇 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		sseq2	⊢ ( 𝑦 = 𝑇 → ( 𝒫 𝑧 ⊆ 𝑦 ↔ 𝒫 𝑧 ⊆ 𝑇 ) )
2		rexeq	⊢ ( 𝑦 = 𝑇 → ( ∃ 𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤 ↔ ∃ 𝑤 ∈ 𝑇 𝒫 𝑧 ⊆ 𝑤 ) )
3	1 2	anbi12d	⊢ ( 𝑦 = 𝑇 → ( ( 𝒫 𝑧 ⊆ 𝑦 ∧ ∃ 𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤 ) ↔ ( 𝒫 𝑧 ⊆ 𝑇 ∧ ∃ 𝑤 ∈ 𝑇 𝒫 𝑧 ⊆ 𝑤 ) ) )
4	3	raleqbi1dv	⊢ ( 𝑦 = 𝑇 → ( ∀ 𝑧 ∈ 𝑦 ( 𝒫 𝑧 ⊆ 𝑦 ∧ ∃ 𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤 ) ↔ ∀ 𝑧 ∈ 𝑇 ( 𝒫 𝑧 ⊆ 𝑇 ∧ ∃ 𝑤 ∈ 𝑇 𝒫 𝑧 ⊆ 𝑤 ) ) )
5		pweq	⊢ ( 𝑦 = 𝑇 → 𝒫 𝑦 = 𝒫 𝑇 )
6		breq2	⊢ ( 𝑦 = 𝑇 → ( 𝑧 ≈ 𝑦 ↔ 𝑧 ≈ 𝑇 ) )
7		eleq2	⊢ ( 𝑦 = 𝑇 → ( 𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝑇 ) )
8	6 7	orbi12d	⊢ ( 𝑦 = 𝑇 → ( ( 𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦 ) ↔ ( 𝑧 ≈ 𝑇 ∨ 𝑧 ∈ 𝑇 ) ) )
9	5 8	raleqbidv	⊢ ( 𝑦 = 𝑇 → ( ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦 ) ↔ ∀ 𝑧 ∈ 𝒫 𝑇 ( 𝑧 ≈ 𝑇 ∨ 𝑧 ∈ 𝑇 ) ) )
10	4 9	anbi12d	⊢ ( 𝑦 = 𝑇 → ( ( ∀ 𝑧 ∈ 𝑦 ( 𝒫 𝑧 ⊆ 𝑦 ∧ ∃ 𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤 ) ∧ ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦 ) ) ↔ ( ∀ 𝑧 ∈ 𝑇 ( 𝒫 𝑧 ⊆ 𝑇 ∧ ∃ 𝑤 ∈ 𝑇 𝒫 𝑧 ⊆ 𝑤 ) ∧ ∀ 𝑧 ∈ 𝒫 𝑇 ( 𝑧 ≈ 𝑇 ∨ 𝑧 ∈ 𝑇 ) ) ) )
11		df-tsk	⊢ Tarski = { 𝑦 ∣ ( ∀ 𝑧 ∈ 𝑦 ( 𝒫 𝑧 ⊆ 𝑦 ∧ ∃ 𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤 ) ∧ ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦 ) ) }
12	10 11	elab2g	⊢ ( 𝑇 ∈ 𝑉 → ( 𝑇 ∈ Tarski ↔ ( ∀ 𝑧 ∈ 𝑇 ( 𝒫 𝑧 ⊆ 𝑇 ∧ ∃ 𝑤 ∈ 𝑇 𝒫 𝑧 ⊆ 𝑤 ) ∧ ∀ 𝑧 ∈ 𝒫 𝑇 ( 𝑧 ≈ 𝑇 ∨ 𝑧 ∈ 𝑇 ) ) ) )