Theorem omelaxinf2 44948

Description: A transitive class that contains ω models the Axiom of Infinity ax-inf2 9648. Lemma II.2.11(7) of [Kunen2] p. 114. Kunen has the additional hypotheses that the Extensionality, Separation, Pairing, and Union axioms are true in 𝑀. This, apparently, is because Kunen's statement of the Axiom of Infinity uses the defined notions ∅ and suc, and these axioms guarantee that these notions are well-defined. When we state the axiom using primitives only, the need for these hypotheses disappears.

The antecedent of this theorem is not enough to guarantee that the class models the alternate axiom ax-inf 9645. (Contributed by Eric Schmidt, 19-Oct-2025.)

Assertion

Ref	Expression
omelaxinf2	⊢ ((Tr 𝑀 ∧ ω ∈ 𝑀) → ∃𝑥 ∈ 𝑀 (∃𝑦 ∈ 𝑀 (𝑦 ∈ 𝑥 ∧ ∀𝑧 ∈ 𝑀 ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑥 → ∃𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 ∧ ∀𝑤 ∈ 𝑀 (𝑤 ∈ 𝑧 ↔ (𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦))))))

Distinct variable groups:   𝑥,𝑦,𝑧,𝑤   𝑥,𝑀,𝑦,𝑧

Allowed substitution hint:   𝑀(𝑤)

Proof of Theorem omelaxinf2

Step	Hyp	Ref	Expression
1		trss 5238	. . 3 ⊢ (Tr 𝑀 → (ω ∈ 𝑀 → ω ⊆ 𝑀))
2	1	imp 406	. 2 ⊢ ((Tr 𝑀 ∧ ω ∈ 𝑀) → ω ⊆ 𝑀)
3		omssaxinf2 44947	. 2 ⊢ ((ω ⊆ 𝑀 ∧ ω ∈ 𝑀) → ∃𝑥 ∈ 𝑀 (∃𝑦 ∈ 𝑀 (𝑦 ∈ 𝑥 ∧ ∀𝑧 ∈ 𝑀 ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑥 → ∃𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 ∧ ∀𝑤 ∈ 𝑀 (𝑤 ∈ 𝑧 ↔ (𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦))))))
4	2, 3	sylancom 588	1 ⊢ ((Tr 𝑀 ∧ ω ∈ 𝑀) → ∃𝑥 ∈ 𝑀 (∃𝑦 ∈ 𝑀 (𝑦 ∈ 𝑥 ∧ ∀𝑧 ∈ 𝑀 ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑥 → ∃𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 ∧ ∀𝑤 ∈ 𝑀 (𝑤 ∈ 𝑧 ↔ (𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦))))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   ∈ wcel 2107  ∀wral 3050  ∃wrex 3059   ⊆ wss 3924  Tr wtr 5227  ωcom 7856

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706  ax-sep 5264  ax-nul 5274  ax-pr 5400  ax-un 7724

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-ne 2932  df-ral 3051  df-rex 3060  df-rab 3414  df-v 3459  df-dif 3927  df-un 3929  df-in 3931  df-ss 3941  df-pss 3944  df-nul 4307  df-if 4499  df-pw 4575  df-sn 4600  df-pr 4602  df-op 4606  df-uni 4882  df-br 5118  df-opab 5180  df-tr 5228  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-ord 6353  df-on 6354  df-lim 6355  df-suc 6356  df-om 7857

This theorem is referenced by:  wfaxinf2  44960