Metamath Proof Explorer

Theorem pwclaxpow

Description: Suppose M is a transitive class that is closed under power sets intersected with M . Then, M models the Axiom of Power Sets ax-pow . One direction of Lemma II.2.8 of Kunen2 p. 113. (Contributed by Eric Schmidt, 19-Oct-2025)

Ref Expression
Assertion pwclaxpow ⊢ Tr ⁡ M ∧ ∀ x ∈ M 𝒫 x ∩ M ∈ M → ∀ x ∈ M ∃ y ∈ M ∀ z ∈ M ∀ w ∈ M w ∈ z → w ∈ x → z ∈ y

Proof

Step Hyp Ref Expression
1 velpw ⊢ z ∈ 𝒫 x ↔ z ⊆ x
2 ssabso ⊢ Tr ⁡ M ∧ z ∈ M → z ⊆ x ↔ ∀ w ∈ M w ∈ z → w ∈ x
3 1 2 bitrid ⊢ Tr ⁡ M ∧ z ∈ M → z ∈ 𝒫 x ↔ ∀ w ∈ M w ∈ z → w ∈ x
4 elin ⊢ z ∈ 𝒫 x ∩ M ↔ z ∈ 𝒫 x ∧ z ∈ M
5 4 simplbi2com ⊢ z ∈ M → z ∈ 𝒫 x → z ∈ 𝒫 x ∩ M
6 5 adantl ⊢ Tr ⁡ M ∧ z ∈ M → z ∈ 𝒫 x → z ∈ 𝒫 x ∩ M
7 3 6 sylbird ⊢ Tr ⁡ M ∧ z ∈ M → ∀ w ∈ M w ∈ z → w ∈ x → z ∈ 𝒫 x ∩ M
8 7 ralrimiva ⊢ Tr ⁡ M → ∀ z ∈ M ∀ w ∈ M w ∈ z → w ∈ x → z ∈ 𝒫 x ∩ M
9 eleq2 ⊢ y = 𝒫 x ∩ M → z ∈ y ↔ z ∈ 𝒫 x ∩ M
10 9 imbi2d ⊢ y = 𝒫 x ∩ M → ∀ w ∈ M w ∈ z → w ∈ x → z ∈ y ↔ ∀ w ∈ M w ∈ z → w ∈ x → z ∈ 𝒫 x ∩ M
11 10 ralbidv ⊢ y = 𝒫 x ∩ M → ∀ z ∈ M ∀ w ∈ M w ∈ z → w ∈ x → z ∈ y ↔ ∀ z ∈ M ∀ w ∈ M w ∈ z → w ∈ x → z ∈ 𝒫 x ∩ M
12 11 rspcev ⊢ 𝒫 x ∩ M ∈ M ∧ ∀ z ∈ M ∀ w ∈ M w ∈ z → w ∈ x → z ∈ 𝒫 x ∩ M → ∃ y ∈ M ∀ z ∈ M ∀ w ∈ M w ∈ z → w ∈ x → z ∈ y
13 8 12 sylan2 ⊢ 𝒫 x ∩ M ∈ M ∧ Tr ⁡ M → ∃ y ∈ M ∀ z ∈ M ∀ w ∈ M w ∈ z → w ∈ x → z ∈ y
14 13 expcom ⊢ Tr ⁡ M → 𝒫 x ∩ M ∈ M → ∃ y ∈ M ∀ z ∈ M ∀ w ∈ M w ∈ z → w ∈ x → z ∈ y
15 14 ralimdv ⊢ Tr ⁡ M → ∀ x ∈ M 𝒫 x ∩ M ∈ M → ∀ x ∈ M ∃ y ∈ M ∀ z ∈ M ∀ w ∈ M w ∈ z → w ∈ x → z ∈ y
16 15 imp ⊢ Tr ⁡ M ∧ ∀ x ∈ M 𝒫 x ∩ M ∈ M → ∀ x ∈ M ∃ y ∈ M ∀ z ∈ M ∀ w ∈ M w ∈ z → w ∈ x → z ∈ y