Metamath Proof Explorer

Theorem wfaxpow

Description: The class of well-founded sets models the Axioms of Power Sets. Part of Corollary II.2.9 of Kunen2 p. 113. (Contributed by Eric Schmidt, 19-Oct-2025)

Ref Expression
Hypothesis wfax.1 ⊢ W = ⋃ R1 On
Assertion wfaxpow ⊢ ∀ x ∈ W ∃ y ∈ W ∀ z ∈ W ∀ w ∈ W w ∈ z → w ∈ x → z ∈ y

Proof

Step Hyp Ref Expression
1 wfax.1 ⊢ W = ⋃ R1 On
2 trwf ⊢ Tr ⁡ ⋃ R1 On
3 treq ⊢ W = ⋃ R1 On → Tr ⁡ W ↔ Tr ⁡ ⋃ R1 On
4 1 3 ax-mp ⊢ Tr ⁡ W ↔ Tr ⁡ ⋃ R1 On
5 2 4 mpbir ⊢ Tr ⁡ W
6 pwclaxpow ⊢ Tr ⁡ W ∧ ∀ x ∈ W 𝒫 x ∩ W ∈ W → ∀ x ∈ W ∃ y ∈ W ∀ z ∈ W ∀ w ∈ W w ∈ z → w ∈ x → z ∈ y
7 5 6 mpan ⊢ ∀ x ∈ W 𝒫 x ∩ W ∈ W → ∀ x ∈ W ∃ y ∈ W ∀ z ∈ W ∀ w ∈ W w ∈ z → w ∈ x → z ∈ y
8 pwwf ⊢ x ∈ ⋃ R1 On ↔ 𝒫 x ∈ ⋃ R1 On
9 8 biimpi ⊢ x ∈ ⋃ R1 On → 𝒫 x ∈ ⋃ R1 On
10 r1elssi ⊢ 𝒫 x ∈ ⋃ R1 On → 𝒫 x ⊆ ⋃ R1 On
11 dfss2 ⊢ 𝒫 x ⊆ ⋃ R1 On ↔ 𝒫 x ∩ ⋃ R1 On = 𝒫 x
12 eleq1 ⊢ 𝒫 x ∩ ⋃ R1 On = 𝒫 x → 𝒫 x ∩ ⋃ R1 On ∈ ⋃ R1 On ↔ 𝒫 x ∈ ⋃ R1 On
13 11 12 sylbi ⊢ 𝒫 x ⊆ ⋃ R1 On → 𝒫 x ∩ ⋃ R1 On ∈ ⋃ R1 On ↔ 𝒫 x ∈ ⋃ R1 On
14 9 10 13 3syl ⊢ x ∈ ⋃ R1 On → 𝒫 x ∩ ⋃ R1 On ∈ ⋃ R1 On ↔ 𝒫 x ∈ ⋃ R1 On
15 9 14 mpbird ⊢ x ∈ ⋃ R1 On → 𝒫 x ∩ ⋃ R1 On ∈ ⋃ R1 On
16 1 eleq2i ⊢ x ∈ W ↔ x ∈ ⋃ R1 On
17 1 ineq2i ⊢ 𝒫 x ∩ W = 𝒫 x ∩ ⋃ R1 On
18 17 1 eleq12i ⊢ 𝒫 x ∩ W ∈ W ↔ 𝒫 x ∩ ⋃ R1 On ∈ ⋃ R1 On
19 15 16 18 3imtr4i ⊢ x ∈ W → 𝒫 x ∩ W ∈ W
20 7 19 mprg ⊢ ∀ x ∈ W ∃ y ∈ W ∀ z ∈ W ∀ w ∈ W w ∈ z → w ∈ x → z ∈ y