Description: The class of well-founded sets models the Axiom of Separation ax-sep . Actually, our statement is stronger, since it is an instance of Separation only when all quantifiers in ph are relativized to W . Part of Corollary II.2.5 of Kunen2 p. 112. (Contributed by Eric Schmidt, 29-Sep-2025)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | wfax.1 | ⊢ 𝑊 = ∪ ( 𝑅1 “ On ) | |
| Assertion | wfaxsep | ⊢ ∀ 𝑧 ∈ 𝑊 ∃ 𝑦 ∈ 𝑊 ∀ 𝑥 ∈ 𝑊 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | wfax.1 | ⊢ 𝑊 = ∪ ( 𝑅1 “ On ) | |
| 2 | ssclaxsep | ⊢ ( ∀ 𝑧 ∈ 𝑊 𝒫 𝑧 ⊆ 𝑊 → ∀ 𝑧 ∈ 𝑊 ∃ 𝑦 ∈ 𝑊 ∀ 𝑥 ∈ 𝑊 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) ) | |
| 3 | pwwf | ⊢ ( 𝑧 ∈ ∪ ( 𝑅1 “ On ) ↔ 𝒫 𝑧 ∈ ∪ ( 𝑅1 “ On ) ) | |
| 4 | r1elssi | ⊢ ( 𝒫 𝑧 ∈ ∪ ( 𝑅1 “ On ) → 𝒫 𝑧 ⊆ ∪ ( 𝑅1 “ On ) ) | |
| 5 | 3 4 | sylbi | ⊢ ( 𝑧 ∈ ∪ ( 𝑅1 “ On ) → 𝒫 𝑧 ⊆ ∪ ( 𝑅1 “ On ) ) |
| 6 | 1 | eleq2i | ⊢ ( 𝑧 ∈ 𝑊 ↔ 𝑧 ∈ ∪ ( 𝑅1 “ On ) ) |
| 7 | 1 | sseq2i | ⊢ ( 𝒫 𝑧 ⊆ 𝑊 ↔ 𝒫 𝑧 ⊆ ∪ ( 𝑅1 “ On ) ) |
| 8 | 5 6 7 | 3imtr4i | ⊢ ( 𝑧 ∈ 𝑊 → 𝒫 𝑧 ⊆ 𝑊 ) |
| 9 | 2 8 | mprg | ⊢ ∀ 𝑧 ∈ 𝑊 ∃ 𝑦 ∈ 𝑊 ∀ 𝑥 ∈ 𝑊 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) |