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∈𝒫Tz≈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∈𝒫yz≈y∨z∈y↔∀z∈𝒫Tz≈T∨z∈T
10 4 9 anbi12d ⊢y=T→∀z∈y𝒫z⊆y∧∃w∈y𝒫z⊆w∧∀z∈𝒫yz≈y∨z∈y↔∀z∈T𝒫z⊆T∧∃w∈T𝒫z⊆w∧∀z∈𝒫Tz≈T∨z∈T
11 df-tsk ⊢Tarski=y|∀z∈y𝒫z⊆y∧∃w∈y𝒫z⊆w∧∀z∈𝒫yz≈y∨z∈y
12 10 11 elab2g ⊢T∈V→T∈Tarski↔∀z∈T𝒫z⊆T∧∃w∈T𝒫z⊆w∧∀z∈𝒫Tz≈T∨z∈T