Metamath Proof Explorer

Theorem eltskg

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

Ref Expression
Assertion eltskg ⊢ T ∈ V → T ∈ Tarski ↔ ∀ z ∈ T 𝒫 z ⊆ T ∧ ∃ w ∈ T 𝒫 z ⊆ w ∧ ∀ z ∈ 𝒫 T z ≈ T ∨ z ∈ T

Proof

Step Hyp Ref Expression
1 sseq2 ⊢ y = T → 𝒫 z ⊆ y ↔ 𝒫 z ⊆ T
2 rexeq ⊢ y = T → ∃ w ∈ y 𝒫 z ⊆ w ↔ ∃ w ∈ T 𝒫 z ⊆ w
3 1 2 anbi12d ⊢ y = T → 𝒫 z ⊆ y ∧ ∃ w ∈ y 𝒫 z ⊆ w ↔ 𝒫 z ⊆ T ∧ ∃ w ∈ T 𝒫 z ⊆ w
4 3 raleqbi1dv ⊢ y = T → ∀ z ∈ y 𝒫 z ⊆ y ∧ ∃ w ∈ y 𝒫 z ⊆ w ↔ ∀ z ∈ T 𝒫 z ⊆ T ∧ ∃ w ∈ T 𝒫 z ⊆ w
5 pweq ⊢ y = T → 𝒫 y = 𝒫 T
6 breq2 ⊢ y = T → z ≈ y ↔ z ≈ T
7 eleq2 ⊢ y = T → z ∈ y ↔ z ∈ T
8 6 7 orbi12d ⊢ y = T → z ≈ y ∨ z ∈ y ↔ z ≈ T ∨ z ∈ T
9 5 8 raleqbidv ⊢ y = T → ∀ z ∈ 𝒫 y z ≈ y ∨ z ∈ y ↔ ∀ z ∈ 𝒫 T z ≈ T ∨ z ∈ T
10 4 9 anbi12d ⊢ y = T → ∀ z ∈ y 𝒫 z ⊆ y ∧ ∃ w ∈ y 𝒫 z ⊆ w ∧ ∀ z ∈ 𝒫 y z ≈ y ∨ z ∈ y ↔ ∀ z ∈ T 𝒫 z ⊆ T ∧ ∃ w ∈ T 𝒫 z ⊆ w ∧ ∀ z ∈ 𝒫 T z ≈ T ∨ z ∈ T
11 df-tsk ⊢ Tarski = y | ∀ z ∈ y 𝒫 z ⊆ y ∧ ∃ w ∈ y 𝒫 z ⊆ w ∧ ∀ z ∈ 𝒫 y z ≈ y ∨ z ∈ y
12 10 11 elab2g ⊢ T ∈ V → T ∈ Tarski ↔ ∀ z ∈ T 𝒫 z ⊆ T ∧ ∃ w ∈ T 𝒫 z ⊆ w ∧ ∀ z ∈ 𝒫 T z ≈ T ∨ z ∈ T