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 𝑀 ∧ ∀ 𝑥 ∈ 𝑀 ( 𝒫 𝑥 ∩ 𝑀 ) ∈ 𝑀 ) → ∀ 𝑥 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		velpw	⊢ ( 𝑧 ∈ 𝒫 𝑥 ↔ 𝑧 ⊆ 𝑥 )
2		ssabso	⊢ ( ( Tr 𝑀 ∧ 𝑧 ∈ 𝑀 ) → ( 𝑧 ⊆ 𝑥 ↔ ∀ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) ) )
3	1 2	bitrid	⊢ ( ( Tr 𝑀 ∧ 𝑧 ∈ 𝑀 ) → ( 𝑧 ∈ 𝒫 𝑥 ↔ ∀ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) ) )
4		elin	⊢ ( 𝑧 ∈ ( 𝒫 𝑥 ∩ 𝑀 ) ↔ ( 𝑧 ∈ 𝒫 𝑥 ∧ 𝑧 ∈ 𝑀 ) )
5	4	simplbi2com	⊢ ( 𝑧 ∈ 𝑀 → ( 𝑧 ∈ 𝒫 𝑥 → 𝑧 ∈ ( 𝒫 𝑥 ∩ 𝑀 ) ) )
6	5	adantl	⊢ ( ( Tr 𝑀 ∧ 𝑧 ∈ 𝑀 ) → ( 𝑧 ∈ 𝒫 𝑥 → 𝑧 ∈ ( 𝒫 𝑥 ∩ 𝑀 ) ) )
7	3 6	sylbird	⊢ ( ( Tr 𝑀 ∧ 𝑧 ∈ 𝑀 ) → ( ∀ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → 𝑧 ∈ ( 𝒫 𝑥 ∩ 𝑀 ) ) )
8	7	ralrimiva	⊢ ( Tr 𝑀 → ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → 𝑧 ∈ ( 𝒫 𝑥 ∩ 𝑀 ) ) )
9		eleq2	⊢ ( 𝑦 = ( 𝒫 𝑥 ∩ 𝑀 ) → ( 𝑧 ∈ 𝑦 ↔ 𝑧 ∈ ( 𝒫 𝑥 ∩ 𝑀 ) ) )
10	9	imbi2d	⊢ ( 𝑦 = ( 𝒫 𝑥 ∩ 𝑀 ) → ( ( ∀ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) ↔ ( ∀ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → 𝑧 ∈ ( 𝒫 𝑥 ∩ 𝑀 ) ) ) )
11	10	ralbidv	⊢ ( 𝑦 = ( 𝒫 𝑥 ∩ 𝑀 ) → ( ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) ↔ ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → 𝑧 ∈ ( 𝒫 𝑥 ∩ 𝑀 ) ) ) )
12	11	rspcev	⊢ ( ( ( 𝒫 𝑥 ∩ 𝑀 ) ∈ 𝑀 ∧ ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → 𝑧 ∈ ( 𝒫 𝑥 ∩ 𝑀 ) ) ) → ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) )
13	8 12	sylan2	⊢ ( ( ( 𝒫 𝑥 ∩ 𝑀 ) ∈ 𝑀 ∧ Tr 𝑀 ) → ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) )
14	13	expcom	⊢ ( Tr 𝑀 → ( ( 𝒫 𝑥 ∩ 𝑀 ) ∈ 𝑀 → ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) ) )
15	14	ralimdv	⊢ ( Tr 𝑀 → ( ∀ 𝑥 ∈ 𝑀 ( 𝒫 𝑥 ∩ 𝑀 ) ∈ 𝑀 → ∀ 𝑥 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) ) )
16	15	imp	⊢ ( ( Tr 𝑀 ∧ ∀ 𝑥 ∈ 𝑀 ( 𝒫 𝑥 ∩ 𝑀 ) ∈ 𝑀 ) → ∀ 𝑥 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) )