Theorem omelaxinf2 44979

Description: A transitive class that contains ω models the Axiom of Infinity ax-inf2 9677. 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 9674. (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 5268	. . 3 ⊢ (Tr 𝑀 → (ω ∈ 𝑀 → ω ⊆ 𝑀))
2	1	imp 406	. 2 ⊢ ((Tr 𝑀 ∧ ω ∈ 𝑀) → ω ⊆ 𝑀)
3		omssaxinf2 44978	. 2 ⊢ ((ω ⊆ 𝑀 ∧ ω ∈ 𝑀) → ∃𝑥 ∈ 𝑀 (∃𝑦 ∈ 𝑀 (𝑦 ∈ 𝑥 ∧ ∀𝑧 ∈ 𝑀 ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑥 → ∃𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 ∧ ∀𝑤 ∈ 𝑀 (𝑤 ∈ 𝑧 ↔ (𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦))))))
4	2, 3	sylancom 588	1 ⊢ ((Tr 𝑀 ∧ ω ∈ 𝑀) → ∃𝑥 ∈ 𝑀 (∃𝑦 ∈ 𝑀 (𝑦 ∈ 𝑥 ∧ ∀𝑧 ∈ 𝑀 ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑥 → ∃𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 ∧ ∀𝑤 ∈ 𝑀 (𝑤 ∈ 𝑧 ↔ (𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦))))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848   ∈ wcel 2108  ∀wral 3060  ∃wrex 3069   ⊆ wss 3950  Tr wtr 5257  ωcom 7883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5294  ax-nul 5304  ax-pr 5430  ax-un 7751

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2728  df-clel 2815  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-pss 3970  df-nul 4333  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4906  df-br 5142  df-opab 5204  df-tr 5258  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5635  df-we 5637  df-ord 6385  df-on 6386  df-lim 6387  df-suc 6388  df-om 7884

This theorem is referenced by:  wfaxinf2  44991