Metamath Proof Explorer

Theorem omssaxinf2

Description: A class that contains all ordinals up to and including _om models the Axiom of Infinity ax-inf2 . The antecedent of this theorem is not enough to guarantee that the class models the alternate axiom ax-inf . (Contributed by Eric Schmidt, 19-Oct-2025)

Ref Expression
Assertion omssaxinf2 ⊢ ω ⊆ M ∧ ω ∈ M → ∃ x ∈ M ∃ y ∈ M y ∈ x ∧ ∀ z ∈ M ¬ z ∈ y ∧ ∀ y ∈ M y ∈ x → ∃ z ∈ M z ∈ x ∧ ∀ w ∈ M w ∈ z ↔ w ∈ y ∨ w = y

Proof

Step Hyp Ref Expression
1 peano1 ⊢ ∅ ∈ ω
2 ssel ⊢ ω ⊆ M → ∅ ∈ ω → ∅ ∈ M
3 1 2 mpi ⊢ ω ⊆ M → ∅ ∈ M
4 noel ⊢ ¬ z ∈ ∅
5 4 rgenw ⊢ ∀ z ∈ M ¬ z ∈ ∅
6 eleq1 ⊢ y = ∅ → y ∈ ω ↔ ∅ ∈ ω
7 eleq2 ⊢ y = ∅ → z ∈ y ↔ z ∈ ∅
8 7 notbid ⊢ y = ∅ → ¬ z ∈ y ↔ ¬ z ∈ ∅
9 8 ralbidv ⊢ y = ∅ → ∀ z ∈ M ¬ z ∈ y ↔ ∀ z ∈ M ¬ z ∈ ∅
10 6 9 anbi12d ⊢ y = ∅ → y ∈ ω ∧ ∀ z ∈ M ¬ z ∈ y ↔ ∅ ∈ ω ∧ ∀ z ∈ M ¬ z ∈ ∅
11 10 rspcev ⊢ ∅ ∈ M ∧ ∅ ∈ ω ∧ ∀ z ∈ M ¬ z ∈ ∅ → ∃ y ∈ M y ∈ ω ∧ ∀ z ∈ M ¬ z ∈ y
12 1 5 11 mpanr12 ⊢ ∅ ∈ M → ∃ y ∈ M y ∈ ω ∧ ∀ z ∈ M ¬ z ∈ y
13 3 12 syl ⊢ ω ⊆ M → ∃ y ∈ M y ∈ ω ∧ ∀ z ∈ M ¬ z ∈ y
14 ssel ⊢ ω ⊆ M → suc ⁡ y ∈ ω → suc ⁡ y ∈ M
15 peano2 ⊢ y ∈ ω → suc ⁡ y ∈ ω
16 14 15 impel ⊢ ω ⊆ M ∧ y ∈ ω → suc ⁡ y ∈ M
17 15 adantl ⊢ ω ⊆ M ∧ y ∈ ω → suc ⁡ y ∈ ω
18 vex ⊢ w ∈ V
19 18 elsuc ⊢ w ∈ suc ⁡ y ↔ w ∈ y ∨ w = y
20 19 rgenw ⊢ ∀ w ∈ M w ∈ suc ⁡ y ↔ w ∈ y ∨ w = y
21 eleq1 ⊢ z = suc ⁡ y → z ∈ ω ↔ suc ⁡ y ∈ ω
22 eleq2 ⊢ z = suc ⁡ y → w ∈ z ↔ w ∈ suc ⁡ y
23 22 bibi1d ⊢ z = suc ⁡ y → w ∈ z ↔ w ∈ y ∨ w = y ↔ w ∈ suc ⁡ y ↔ w ∈ y ∨ w = y
24 23 ralbidv ⊢ z = suc ⁡ y → ∀ w ∈ M w ∈ z ↔ w ∈ y ∨ w = y ↔ ∀ w ∈ M w ∈ suc ⁡ y ↔ w ∈ y ∨ w = y
25 21 24 anbi12d ⊢ z = suc ⁡ y → z ∈ ω ∧ ∀ w ∈ M w ∈ z ↔ w ∈ y ∨ w = y ↔ suc ⁡ y ∈ ω ∧ ∀ w ∈ M w ∈ suc ⁡ y ↔ w ∈ y ∨ w = y
26 25 rspcev ⊢ suc ⁡ y ∈ M ∧ suc ⁡ y ∈ ω ∧ ∀ w ∈ M w ∈ suc ⁡ y ↔ w ∈ y ∨ w = y → ∃ z ∈ M z ∈ ω ∧ ∀ w ∈ M w ∈ z ↔ w ∈ y ∨ w = y
27 20 26 mpanr2 ⊢ suc ⁡ y ∈ M ∧ suc ⁡ y ∈ ω → ∃ z ∈ M z ∈ ω ∧ ∀ w ∈ M w ∈ z ↔ w ∈ y ∨ w = y
28 16 17 27 syl2anc ⊢ ω ⊆ M ∧ y ∈ ω → ∃ z ∈ M z ∈ ω ∧ ∀ w ∈ M w ∈ z ↔ w ∈ y ∨ w = y
29 28 ex ⊢ ω ⊆ M → y ∈ ω → ∃ z ∈ M z ∈ ω ∧ ∀ w ∈ M w ∈ z ↔ w ∈ y ∨ w = y
30 29 ralrimivw ⊢ ω ⊆ M → ∀ y ∈ M y ∈ ω → ∃ z ∈ M z ∈ ω ∧ ∀ w ∈ M w ∈ z ↔ w ∈ y ∨ w = y
31 eleq2 ⊢ x = ω → y ∈ x ↔ y ∈ ω
32 31 anbi1d ⊢ x = ω → y ∈ x ∧ ∀ z ∈ M ¬ z ∈ y ↔ y ∈ ω ∧ ∀ z ∈ M ¬ z ∈ y
33 32 rexbidv ⊢ x = ω → ∃ y ∈ M y ∈ x ∧ ∀ z ∈ M ¬ z ∈ y ↔ ∃ y ∈ M y ∈ ω ∧ ∀ z ∈ M ¬ z ∈ y
34 eleq2 ⊢ x = ω → z ∈ x ↔ z ∈ ω
35 34 anbi1d ⊢ x = ω → z ∈ x ∧ ∀ w ∈ M w ∈ z ↔ w ∈ y ∨ w = y ↔ z ∈ ω ∧ ∀ w ∈ M w ∈ z ↔ w ∈ y ∨ w = y
36 35 rexbidv ⊢ x = ω → ∃ z ∈ M z ∈ x ∧ ∀ w ∈ M w ∈ z ↔ w ∈ y ∨ w = y ↔ ∃ z ∈ M z ∈ ω ∧ ∀ w ∈ M w ∈ z ↔ w ∈ y ∨ w = y
37 31 36 imbi12d ⊢ x = ω → y ∈ x → ∃ z ∈ M z ∈ x ∧ ∀ w ∈ M w ∈ z ↔ w ∈ y ∨ w = y ↔ y ∈ ω → ∃ z ∈ M z ∈ ω ∧ ∀ w ∈ M w ∈ z ↔ w ∈ y ∨ w = y
38 37 ralbidv ⊢ x = ω → ∀ y ∈ M y ∈ x → ∃ z ∈ M z ∈ x ∧ ∀ w ∈ M w ∈ z ↔ w ∈ y ∨ w = y ↔ ∀ y ∈ M y ∈ ω → ∃ z ∈ M z ∈ ω ∧ ∀ w ∈ M w ∈ z ↔ w ∈ y ∨ w = y
39 33 38 anbi12d ⊢ x = ω → ∃ y ∈ M y ∈ x ∧ ∀ z ∈ M ¬ z ∈ y ∧ ∀ y ∈ M y ∈ x → ∃ z ∈ M z ∈ x ∧ ∀ w ∈ M w ∈ z ↔ w ∈ y ∨ w = y ↔ ∃ y ∈ M y ∈ ω ∧ ∀ z ∈ M ¬ z ∈ y ∧ ∀ y ∈ M y ∈ ω → ∃ z ∈ M z ∈ ω ∧ ∀ w ∈ M w ∈ z ↔ w ∈ y ∨ w = y
40 39 rspcev ⊢ ω ∈ M ∧ ∃ y ∈ M y ∈ ω ∧ ∀ z ∈ M ¬ z ∈ y ∧ ∀ y ∈ M y ∈ ω → ∃ z ∈ M z ∈ ω ∧ ∀ w ∈ M w ∈ z ↔ w ∈ y ∨ w = y → ∃ x ∈ M ∃ y ∈ M y ∈ x ∧ ∀ z ∈ M ¬ z ∈ y ∧ ∀ y ∈ M y ∈ x → ∃ z ∈ M z ∈ x ∧ ∀ w ∈ M w ∈ z ↔ w ∈ y ∨ w = y
41 40 expcom ⊢ ∃ y ∈ M y ∈ ω ∧ ∀ z ∈ M ¬ z ∈ y ∧ ∀ y ∈ M y ∈ ω → ∃ z ∈ M z ∈ ω ∧ ∀ w ∈ M w ∈ z ↔ w ∈ y ∨ w = y → ω ∈ M → ∃ x ∈ M ∃ y ∈ M y ∈ x ∧ ∀ z ∈ M ¬ z ∈ y ∧ ∀ y ∈ M y ∈ x → ∃ z ∈ M z ∈ x ∧ ∀ w ∈ M w ∈ z ↔ w ∈ y ∨ w = y
42 13 30 41 syl2anc ⊢ ω ⊆ M → ω ∈ M → ∃ x ∈ M ∃ y ∈ M y ∈ x ∧ ∀ z ∈ M ¬ z ∈ y ∧ ∀ y ∈ M y ∈ x → ∃ z ∈ M z ∈ x ∧ ∀ w ∈ M w ∈ z ↔ w ∈ y ∨ w = y
43 42 imp ⊢ ω ⊆ M ∧ ω ∈ M → ∃ x ∈ M ∃ y ∈ M y ∈ x ∧ ∀ z ∈ M ¬ z ∈ y ∧ ∀ y ∈ M y ∈ x → ∃ z ∈ M z ∈ x ∧ ∀ w ∈ M w ∈ z ↔ w ∈ y ∨ w = y