Description: A standard version of Axiom of Infinity, expanded to primitives, derived from our version of Infinity ax-inf and Regularity ax-reg .
This theorem should not be referenced in any proof. Instead, use ax-inf2 below so that the ordinary uses of Regularity can be more easily identified. (New usage is discouraged.) (Contributed by NM, 3-Nov-1996)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | axinf2 | ⊢ ∃ 𝑥 ( ∃ 𝑦 ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ¬ 𝑧 ∈ 𝑦 ) ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ∃ 𝑧 ( 𝑧 ∈ 𝑥 ∧ ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ ( 𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦 ) ) ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | peano1 | ⊢ ∅ ∈ ω | |
| 2 | peano2 | ⊢ ( 𝑦 ∈ ω → suc 𝑦 ∈ ω ) | |
| 3 | 2 | ax-gen | ⊢ ∀ 𝑦 ( 𝑦 ∈ ω → suc 𝑦 ∈ ω ) |
| 4 | zfinf | ⊢ ∃ 𝑥 ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ∃ 𝑧 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥 ) ) ) | |
| 5 | 4 | inf2 | ⊢ ∃ 𝑥 ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) |
| 6 | 5 | inf3 | ⊢ ω ∈ V |
| 7 | eleq2 | ⊢ ( 𝑥 = ω → ( ∅ ∈ 𝑥 ↔ ∅ ∈ ω ) ) | |
| 8 | eleq2 | ⊢ ( 𝑥 = ω → ( 𝑦 ∈ 𝑥 ↔ 𝑦 ∈ ω ) ) | |
| 9 | eleq2 | ⊢ ( 𝑥 = ω → ( suc 𝑦 ∈ 𝑥 ↔ suc 𝑦 ∈ ω ) ) | |
| 10 | 8 9 | imbi12d | ⊢ ( 𝑥 = ω → ( ( 𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥 ) ↔ ( 𝑦 ∈ ω → suc 𝑦 ∈ ω ) ) ) |
| 11 | 10 | albidv | ⊢ ( 𝑥 = ω → ( ∀ 𝑦 ( 𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥 ) ↔ ∀ 𝑦 ( 𝑦 ∈ ω → suc 𝑦 ∈ ω ) ) ) |
| 12 | 7 11 | anbi12d | ⊢ ( 𝑥 = ω → ( ( ∅ ∈ 𝑥 ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥 ) ) ↔ ( ∅ ∈ ω ∧ ∀ 𝑦 ( 𝑦 ∈ ω → suc 𝑦 ∈ ω ) ) ) ) |
| 13 | 6 12 | spcev | ⊢ ( ( ∅ ∈ ω ∧ ∀ 𝑦 ( 𝑦 ∈ ω → suc 𝑦 ∈ ω ) ) → ∃ 𝑥 ( ∅ ∈ 𝑥 ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥 ) ) ) |
| 14 | 1 3 13 | mp2an | ⊢ ∃ 𝑥 ( ∅ ∈ 𝑥 ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥 ) ) |
| 15 | 0el | ⊢ ( ∅ ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ¬ 𝑧 ∈ 𝑦 ) | |
| 16 | df-rex | ⊢ ( ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ¬ 𝑧 ∈ 𝑦 ↔ ∃ 𝑦 ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ¬ 𝑧 ∈ 𝑦 ) ) | |
| 17 | 15 16 | bitri | ⊢ ( ∅ ∈ 𝑥 ↔ ∃ 𝑦 ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ¬ 𝑧 ∈ 𝑦 ) ) |
| 18 | sucel | ⊢ ( suc 𝑦 ∈ 𝑥 ↔ ∃ 𝑧 ∈ 𝑥 ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ ( 𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦 ) ) ) | |
| 19 | df-rex | ⊢ ( ∃ 𝑧 ∈ 𝑥 ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ ( 𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦 ) ) ↔ ∃ 𝑧 ( 𝑧 ∈ 𝑥 ∧ ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ ( 𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦 ) ) ) ) | |
| 20 | 18 19 | bitri | ⊢ ( suc 𝑦 ∈ 𝑥 ↔ ∃ 𝑧 ( 𝑧 ∈ 𝑥 ∧ ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ ( 𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦 ) ) ) ) |
| 21 | 20 | imbi2i | ⊢ ( ( 𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥 ) ↔ ( 𝑦 ∈ 𝑥 → ∃ 𝑧 ( 𝑧 ∈ 𝑥 ∧ ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ ( 𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦 ) ) ) ) ) |
| 22 | 21 | albii | ⊢ ( ∀ 𝑦 ( 𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥 ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ∃ 𝑧 ( 𝑧 ∈ 𝑥 ∧ ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ ( 𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦 ) ) ) ) ) |
| 23 | 17 22 | anbi12i | ⊢ ( ( ∅ ∈ 𝑥 ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥 ) ) ↔ ( ∃ 𝑦 ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ¬ 𝑧 ∈ 𝑦 ) ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ∃ 𝑧 ( 𝑧 ∈ 𝑥 ∧ ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ ( 𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦 ) ) ) ) ) ) |
| 24 | 23 | exbii | ⊢ ( ∃ 𝑥 ( ∅ ∈ 𝑥 ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥 ) ) ↔ ∃ 𝑥 ( ∃ 𝑦 ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ¬ 𝑧 ∈ 𝑦 ) ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ∃ 𝑧 ( 𝑧 ∈ 𝑥 ∧ ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ ( 𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦 ) ) ) ) ) ) |
| 25 | 14 24 | mpbi | ⊢ ∃ 𝑥 ( ∃ 𝑦 ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ¬ 𝑧 ∈ 𝑦 ) ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ∃ 𝑧 ( 𝑧 ∈ 𝑥 ∧ ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ ( 𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦 ) ) ) ) ) |