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 ⊢ 𝑊 = ∪ ( 𝑅1 “ On )
Assertion wfaxpow ∀ 𝑥 ∈ 𝑊 ∃ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑊 ( ∀ 𝑤 ∈ 𝑊 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 )

Proof

Step Hyp Ref Expression
1 wfax.1 ⊢ 𝑊 = ∪ ( 𝑅1 “ On )
2 trwf ⊢ Tr ∪ ( 𝑅1 “ On )
3 treq ⊢ ( 𝑊 = ∪ ( 𝑅1 “ On ) → ( Tr 𝑊 ↔ Tr ∪ ( 𝑅1 “ On ) ) )
4 1 3 ax-mp ⊢ ( Tr 𝑊 ↔ Tr ∪ ( 𝑅1 “ On ) )
5 2 4 mpbir ⊢ Tr 𝑊
6 pwclaxpow ⊢ ( ( Tr 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ( 𝒫 𝑥 ∩ 𝑊 ) ∈ 𝑊 ) → ∀ 𝑥 ∈ 𝑊 ∃ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑊 ( ∀ 𝑤 ∈ 𝑊 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) )
7 5 6 mpan ⊢ ( ∀ 𝑥 ∈ 𝑊 ( 𝒫 𝑥 ∩ 𝑊 ) ∈ 𝑊 → ∀ 𝑥 ∈ 𝑊 ∃ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑊 ( ∀ 𝑤 ∈ 𝑊 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) )
8 pwwf ⊢ ( 𝑥 ∈ ∪ ( 𝑅1 “ On ) ↔ 𝒫 𝑥 ∈ ∪ ( 𝑅1 “ On ) )
9 8 biimpi ⊢ ( 𝑥 ∈ ∪ ( 𝑅1 “ On ) → 𝒫 𝑥 ∈ ∪ ( 𝑅1 “ On ) )
10 r1elssi ⊢ ( 𝒫 𝑥 ∈ ∪ ( 𝑅1 “ On ) → 𝒫 𝑥 ⊆ ∪ ( 𝑅1 “ On ) )
11 dfss2 ⊢ ( 𝒫 𝑥 ⊆ ∪ ( 𝑅1 “ On ) ↔ ( 𝒫 𝑥 ∩ ∪ ( 𝑅1 “ On ) ) = 𝒫 𝑥 )
12 eleq1 ⊢ ( ( 𝒫 𝑥 ∩ ∪ ( 𝑅1 “ On ) ) = 𝒫 𝑥 → ( ( 𝒫 𝑥 ∩ ∪ ( 𝑅1 “ On ) ) ∈ ∪ ( 𝑅1 “ On ) ↔ 𝒫 𝑥 ∈ ∪ ( 𝑅1 “ On ) ) )
13 11 12 sylbi ⊢ ( 𝒫 𝑥 ⊆ ∪ ( 𝑅1 “ On ) → ( ( 𝒫 𝑥 ∩ ∪ ( 𝑅1 “ On ) ) ∈ ∪ ( 𝑅1 “ On ) ↔ 𝒫 𝑥 ∈ ∪ ( 𝑅1 “ On ) ) )
14 9 10 13 3syl ⊢ ( 𝑥 ∈ ∪ ( 𝑅1 “ On ) → ( ( 𝒫 𝑥 ∩ ∪ ( 𝑅1 “ On ) ) ∈ ∪ ( 𝑅1 “ On ) ↔ 𝒫 𝑥 ∈ ∪ ( 𝑅1 “ On ) ) )
15 9 14 mpbird ⊢ ( 𝑥 ∈ ∪ ( 𝑅1 “ On ) → ( 𝒫 𝑥 ∩ ∪ ( 𝑅1 “ On ) ) ∈ ∪ ( 𝑅1 “ On ) )
16 1 eleq2i ⊢ ( 𝑥 ∈ 𝑊 ↔ 𝑥 ∈ ∪ ( 𝑅1 “ On ) )
17 1 ineq2i ⊢ ( 𝒫 𝑥 ∩ 𝑊 ) = ( 𝒫 𝑥 ∩ ∪ ( 𝑅1 “ On ) )
18 17 1 eleq12i ⊢ ( ( 𝒫 𝑥 ∩ 𝑊 ) ∈ 𝑊 ↔ ( 𝒫 𝑥 ∩ ∪ ( 𝑅1 “ On ) ) ∈ ∪ ( 𝑅1 “ On ) )
19 15 16 18 3imtr4i ⊢ ( 𝑥 ∈ 𝑊 → ( 𝒫 𝑥 ∩ 𝑊 ) ∈ 𝑊 )
20 7 19 mprg ⊢ ∀ 𝑥 ∈ 𝑊 ∃ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑊 ( ∀ 𝑤 ∈ 𝑊 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 )