Description: The class of well-founded sets models the Axiom of Union ax-un . Part of Corollary II.2.5 of Kunen2 p. 112. (Contributed by Eric Schmidt, 19-Oct-2025)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | wfax.1 | ⊢ 𝑊 = ∪ ( 𝑅1 “ On ) | |
| Assertion | wfaxun | ⊢ ∀ 𝑥 ∈ 𝑊 ∃ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑊 ( ∃ 𝑤 ∈ 𝑊 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | wfax.1 | ⊢ 𝑊 = ∪ ( 𝑅1 “ On ) | |
| 2 | uniclaxun | ⊢ ( ∀ 𝑥 ∈ 𝑊 ∪ 𝑥 ∈ 𝑊 → ∀ 𝑥 ∈ 𝑊 ∃ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑊 ( ∃ 𝑤 ∈ 𝑊 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) ) | |
| 3 | uniwf | ⊢ ( 𝑥 ∈ ∪ ( 𝑅1 “ On ) ↔ ∪ 𝑥 ∈ ∪ ( 𝑅1 “ On ) ) | |
| 4 | 1 | eleq2i | ⊢ ( 𝑥 ∈ 𝑊 ↔ 𝑥 ∈ ∪ ( 𝑅1 “ On ) ) |
| 5 | 1 | eleq2i | ⊢ ( ∪ 𝑥 ∈ 𝑊 ↔ ∪ 𝑥 ∈ ∪ ( 𝑅1 “ On ) ) |
| 6 | 3 4 5 | 3bitr4i | ⊢ ( 𝑥 ∈ 𝑊 ↔ ∪ 𝑥 ∈ 𝑊 ) |
| 7 | 6 | biimpi | ⊢ ( 𝑥 ∈ 𝑊 → ∪ 𝑥 ∈ 𝑊 ) |
| 8 | 2 7 | mprg | ⊢ ∀ 𝑥 ∈ 𝑊 ∃ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑊 ( ∃ 𝑤 ∈ 𝑊 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) |