Theorem prcinf 35048

Description: Any proper class is literally infinite, in the sense that it contains subsets of arbitrarily large finite cardinality. This proof holds regardless of whether the Axiom of Infinity is accepted or negated. (Contributed by BTernaryTau, 22-Jun-2025.)

Assertion

Ref	Expression
prcinf	⊢ (¬ 𝐴 ∈ V → ∀𝑛 ∈ ω ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛))

Distinct variable group:   𝐴,𝑛,𝑥

Proof of Theorem prcinf

Step	Hyp	Ref	Expression
1		elex 3498	. 2 ⊢ (𝐴 ∈ Fin → 𝐴 ∈ V)
2		isinf 9289	. 2 ⊢ (¬ 𝐴 ∈ Fin → ∀𝑛 ∈ ω ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛))
3	1, 2	nsyl5 159	1 ⊢ (¬ 𝐴 ∈ V → ∀𝑛 ∈ ω ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395  ∃wex 1774   ∈ wcel 2104  ∀wral 3057  Vcvv 3477   ⊆ wss 3963   class class class wbr 5150  ωcom 7881   ≈ cen 8976  Fincfn 8979

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1963  ax-7 2003  ax-8 2106  ax-9 2114  ax-10 2137  ax-12 2173  ax-ext 2704  ax-sep 5301  ax-nul 5308  ax-pr 5431  ax-un 7748

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1538  df-fal 1548  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2536  df-clab 2711  df-cleq 2725  df-clel 2812  df-ne 2937  df-ral 3058  df-rex 3067  df-rab 3433  df-v 3479  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4916  df-br 5151  df-opab 5213  df-tr 5268  df-id 5577  df-eprel 5583  df-po 5591  df-so 5592  df-fr 5636  df-we 5638  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-ord 6384  df-on 6385  df-lim 6386  df-suc 6387  df-fun 6561  df-fn 6562  df-f 6563  df-f1 6564  df-fo 6565  df-f1o 6566  df-om 7882  df-en 8980  df-fin 8983

This theorem is referenced by: (None)