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

Metamath Proof Explorer

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 ↔ ( ∀ 𝑧 ∈ 𝑇 ( 𝒫 𝑧 ⊆ 𝑇 ∧ ∃ 𝑤 ∈ 𝑇 𝒫 𝑧 ⊆ 𝑤 ) ∧ ∀ 𝑧 ∈ 𝒫 𝑇 ( 𝑧 ≈ 𝑇 ∨ 𝑧 ∈ 𝑇 ) ) ) )