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

Proof

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