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 ( ( ω ⊆ 𝑀 ∧ ω ∈ 𝑀 ) → ∃ 𝑥 ∈ 𝑀 ( ∃ 𝑦 ∈ 𝑀 ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝑀 ¬ 𝑧 ∈ 𝑦 ) ∧ ∀ 𝑦 ∈ 𝑀 ( 𝑦 ∈ 𝑥 → ∃ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑥 ∧ ∀ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑧 ↔ ( 𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦 ) ) ) ) ) )

Proof

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