Metamath Proof Explorer

Theorem eltsk2g

Description: Properties of a Tarski class. (Contributed by FL, 30-Dec-2010) (Revised by Mario Carneiro, 20-Sep-2014)

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

Proof

Step Hyp Ref Expression
1 eltskg ⊢ T ∈ V → T ∈ Tarski ↔ ∀ z ∈ T 𝒫 z ⊆ T ∧ ∃ w ∈ T 𝒫 z ⊆ w ∧ ∀ z ∈ 𝒫 T z ≈ T ∨ z ∈ T
2 nfra1 ⊢ Ⅎ z ∀ z ∈ T 𝒫 z ⊆ T
3 pweq ⊢ z = w → 𝒫 z = 𝒫 w
4 3 sseq1d ⊢ z = w → 𝒫 z ⊆ T ↔ 𝒫 w ⊆ T
5 4 rspccva ⊢ ∀ z ∈ T 𝒫 z ⊆ T ∧ w ∈ T → 𝒫 w ⊆ T
6 5 adantlr ⊢ ∀ z ∈ T 𝒫 z ⊆ T ∧ z ∈ T ∧ w ∈ T → 𝒫 w ⊆ T
7 vpwex ⊢ 𝒫 z ∈ V
8 7 elpw ⊢ 𝒫 z ∈ 𝒫 w ↔ 𝒫 z ⊆ w
9 ssel ⊢ 𝒫 w ⊆ T → 𝒫 z ∈ 𝒫 w → 𝒫 z ∈ T
10 8 9 biimtrrid ⊢ 𝒫 w ⊆ T → 𝒫 z ⊆ w → 𝒫 z ∈ T
11 6 10 syl ⊢ ∀ z ∈ T 𝒫 z ⊆ T ∧ z ∈ T ∧ w ∈ T → 𝒫 z ⊆ w → 𝒫 z ∈ T
12 11 rexlimdva ⊢ ∀ z ∈ T 𝒫 z ⊆ T ∧ z ∈ T → ∃ w ∈ T 𝒫 z ⊆ w → 𝒫 z ∈ T
13 2 12 ralimdaa ⊢ ∀ z ∈ T 𝒫 z ⊆ T → ∀ z ∈ T ∃ w ∈ T 𝒫 z ⊆ w → ∀ z ∈ T 𝒫 z ∈ T
14 13 imdistani ⊢ ∀ z ∈ T 𝒫 z ⊆ T ∧ ∀ z ∈ T ∃ w ∈ T 𝒫 z ⊆ w → ∀ z ∈ T 𝒫 z ⊆ T ∧ ∀ z ∈ T 𝒫 z ∈ T
15 r19.26 ⊢ ∀ z ∈ T 𝒫 z ⊆ T ∧ ∃ w ∈ T 𝒫 z ⊆ w ↔ ∀ z ∈ T 𝒫 z ⊆ T ∧ ∀ z ∈ T ∃ w ∈ T 𝒫 z ⊆ w
16 r19.26 ⊢ ∀ z ∈ T 𝒫 z ⊆ T ∧ 𝒫 z ∈ T ↔ ∀ z ∈ T 𝒫 z ⊆ T ∧ ∀ z ∈ T 𝒫 z ∈ T
17 14 15 16 3imtr4i ⊢ ∀ z ∈ T 𝒫 z ⊆ T ∧ ∃ w ∈ T 𝒫 z ⊆ w → ∀ z ∈ T 𝒫 z ⊆ T ∧ 𝒫 z ∈ T
18 ssid ⊢ 𝒫 z ⊆ 𝒫 z
19 sseq2 ⊢ w = 𝒫 z → 𝒫 z ⊆ w ↔ 𝒫 z ⊆ 𝒫 z
20 19 rspcev ⊢ 𝒫 z ∈ T ∧ 𝒫 z ⊆ 𝒫 z → ∃ w ∈ T 𝒫 z ⊆ w
21 18 20 mpan2 ⊢ 𝒫 z ∈ T → ∃ w ∈ T 𝒫 z ⊆ w
22 21 anim2i ⊢ 𝒫 z ⊆ T ∧ 𝒫 z ∈ T → 𝒫 z ⊆ T ∧ ∃ w ∈ T 𝒫 z ⊆ w
23 22 ralimi ⊢ ∀ z ∈ T 𝒫 z ⊆ T ∧ 𝒫 z ∈ T → ∀ z ∈ T 𝒫 z ⊆ T ∧ ∃ w ∈ T 𝒫 z ⊆ w
24 17 23 impbii ⊢ ∀ z ∈ T 𝒫 z ⊆ T ∧ ∃ w ∈ T 𝒫 z ⊆ w ↔ ∀ z ∈ T 𝒫 z ⊆ T ∧ 𝒫 z ∈ T
25 24 anbi1i ⊢ ∀ z ∈ T 𝒫 z ⊆ T ∧ ∃ w ∈ T 𝒫 z ⊆ w ∧ ∀ z ∈ 𝒫 T z ≈ T ∨ z ∈ T ↔ ∀ z ∈ T 𝒫 z ⊆ T ∧ 𝒫 z ∈ T ∧ ∀ z ∈ 𝒫 T z ≈ T ∨ z ∈ T
26 1 25 bitrdi ⊢ T ∈ V → T ∈ Tarski ↔ ∀ z ∈ T 𝒫 z ⊆ T ∧ 𝒫 z ∈ T ∧ ∀ z ∈ 𝒫 T z ≈ T ∨ z ∈ T