MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  isinf Structured version   Visualization version   GIF version

Theorem isinf 9293
Description: Any set that is not finite is literally infinite, in the sense that it contains subsets of arbitrarily large finite cardinality. (It cannot be proven that the set has countably infinite subsets unless AC is invoked.) The proof does not require the Axiom of Infinity. (Contributed by Mario Carneiro, 15-Jan-2013.) Avoid ax-pow 5370. (Revised by BTernaryTau, 2-Jan-2025.)
Assertion
Ref Expression
isinf 𝐴 ∈ Fin → ∀𝑛 ∈ ω ∃𝑥(𝑥𝐴𝑥𝑛))
Distinct variable group:   𝐴,𝑛,𝑥

Proof of Theorem isinf
Dummy variables 𝑚 𝑦 𝑓 𝑔 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 breq2 5151 . . . . . 6 (𝑛 = ∅ → (𝑥𝑛𝑥 ≈ ∅))
21anbi2d 630 . . . . 5 (𝑛 = ∅ → ((𝑥𝐴𝑥𝑛) ↔ (𝑥𝐴𝑥 ≈ ∅)))
32exbidv 1918 . . . 4 (𝑛 = ∅ → (∃𝑥(𝑥𝐴𝑥𝑛) ↔ ∃𝑥(𝑥𝐴𝑥 ≈ ∅)))
4 breq2 5151 . . . . . 6 (𝑛 = 𝑚 → (𝑥𝑛𝑥𝑚))
54anbi2d 630 . . . . 5 (𝑛 = 𝑚 → ((𝑥𝐴𝑥𝑛) ↔ (𝑥𝐴𝑥𝑚)))
65exbidv 1918 . . . 4 (𝑛 = 𝑚 → (∃𝑥(𝑥𝐴𝑥𝑛) ↔ ∃𝑥(𝑥𝐴𝑥𝑚)))
7 sseq1 4020 . . . . . . 7 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
87adantl 481 . . . . . 6 ((𝑛 = suc 𝑚𝑥 = 𝑦) → (𝑥𝐴𝑦𝐴))
9 breq1 5150 . . . . . . 7 (𝑥 = 𝑦 → (𝑥𝑛𝑦𝑛))
10 breq2 5151 . . . . . . 7 (𝑛 = suc 𝑚 → (𝑦𝑛𝑦 ≈ suc 𝑚))
119, 10sylan9bbr 510 . . . . . 6 ((𝑛 = suc 𝑚𝑥 = 𝑦) → (𝑥𝑛𝑦 ≈ suc 𝑚))
128, 11anbi12d 632 . . . . 5 ((𝑛 = suc 𝑚𝑥 = 𝑦) → ((𝑥𝐴𝑥𝑛) ↔ (𝑦𝐴𝑦 ≈ suc 𝑚)))
1312cbvexdvaw 2035 . . . 4 (𝑛 = suc 𝑚 → (∃𝑥(𝑥𝐴𝑥𝑛) ↔ ∃𝑦(𝑦𝐴𝑦 ≈ suc 𝑚)))
14 0ss 4405 . . . . . 6 ∅ ⊆ 𝐴
15 peano1 7910 . . . . . . 7 ∅ ∈ ω
16 enrefnn 9085 . . . . . . 7 (∅ ∈ ω → ∅ ≈ ∅)
1715, 16ax-mp 5 . . . . . 6 ∅ ≈ ∅
18 0ex 5312 . . . . . . 7 ∅ ∈ V
19 sseq1 4020 . . . . . . . 8 (𝑥 = ∅ → (𝑥𝐴 ↔ ∅ ⊆ 𝐴))
20 breq1 5150 . . . . . . . 8 (𝑥 = ∅ → (𝑥 ≈ ∅ ↔ ∅ ≈ ∅))
2119, 20anbi12d 632 . . . . . . 7 (𝑥 = ∅ → ((𝑥𝐴𝑥 ≈ ∅) ↔ (∅ ⊆ 𝐴 ∧ ∅ ≈ ∅)))
2218, 21spcev 3605 . . . . . 6 ((∅ ⊆ 𝐴 ∧ ∅ ≈ ∅) → ∃𝑥(𝑥𝐴𝑥 ≈ ∅))
2314, 17, 22mp2an 692 . . . . 5 𝑥(𝑥𝐴𝑥 ≈ ∅)
2423a1i 11 . . . 4 𝐴 ∈ Fin → ∃𝑥(𝑥𝐴𝑥 ≈ ∅))
25 ssdif0 4371 . . . . . . . . . . . . 13 (𝐴𝑥 ↔ (𝐴𝑥) = ∅)
26 eqss 4010 . . . . . . . . . . . . . . 15 (𝑥 = 𝐴 ↔ (𝑥𝐴𝐴𝑥))
27 breq1 5150 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝐴 → (𝑥𝑚𝐴𝑚))
2827biimpa 476 . . . . . . . . . . . . . . . . . 18 ((𝑥 = 𝐴𝑥𝑚) → 𝐴𝑚)
29 rspe 3246 . . . . . . . . . . . . . . . . . 18 ((𝑚 ∈ ω ∧ 𝐴𝑚) → ∃𝑚 ∈ ω 𝐴𝑚)
3028, 29sylan2 593 . . . . . . . . . . . . . . . . 17 ((𝑚 ∈ ω ∧ (𝑥 = 𝐴𝑥𝑚)) → ∃𝑚 ∈ ω 𝐴𝑚)
31 isfi 9014 . . . . . . . . . . . . . . . . 17 (𝐴 ∈ Fin ↔ ∃𝑚 ∈ ω 𝐴𝑚)
3230, 31sylibr 234 . . . . . . . . . . . . . . . 16 ((𝑚 ∈ ω ∧ (𝑥 = 𝐴𝑥𝑚)) → 𝐴 ∈ Fin)
3332expcom 413 . . . . . . . . . . . . . . 15 ((𝑥 = 𝐴𝑥𝑚) → (𝑚 ∈ ω → 𝐴 ∈ Fin))
3426, 33sylanbr 582 . . . . . . . . . . . . . 14 (((𝑥𝐴𝐴𝑥) ∧ 𝑥𝑚) → (𝑚 ∈ ω → 𝐴 ∈ Fin))
3534ex 412 . . . . . . . . . . . . 13 ((𝑥𝐴𝐴𝑥) → (𝑥𝑚 → (𝑚 ∈ ω → 𝐴 ∈ Fin)))
3625, 35sylan2br 595 . . . . . . . . . . . 12 ((𝑥𝐴 ∧ (𝐴𝑥) = ∅) → (𝑥𝑚 → (𝑚 ∈ ω → 𝐴 ∈ Fin)))
3736expcom 413 . . . . . . . . . . 11 ((𝐴𝑥) = ∅ → (𝑥𝐴 → (𝑥𝑚 → (𝑚 ∈ ω → 𝐴 ∈ Fin))))
38373impd 1347 . . . . . . . . . 10 ((𝐴𝑥) = ∅ → ((𝑥𝐴𝑥𝑚𝑚 ∈ ω) → 𝐴 ∈ Fin))
3938com12 32 . . . . . . . . 9 ((𝑥𝐴𝑥𝑚𝑚 ∈ ω) → ((𝐴𝑥) = ∅ → 𝐴 ∈ Fin))
4039con3d 152 . . . . . . . 8 ((𝑥𝐴𝑥𝑚𝑚 ∈ ω) → (¬ 𝐴 ∈ Fin → ¬ (𝐴𝑥) = ∅))
41 bren 8993 . . . . . . . . . 10 (𝑥𝑚 ↔ ∃𝑓 𝑓:𝑥1-1-onto𝑚)
42 neq0 4357 . . . . . . . . . . . . . 14 (¬ (𝐴𝑥) = ∅ ↔ ∃𝑧 𝑧 ∈ (𝐴𝑥))
43 eldifi 4140 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ∈ (𝐴𝑥) → 𝑧𝐴)
4443snssd 4813 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ (𝐴𝑥) → {𝑧} ⊆ 𝐴)
45 unss 4199 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥𝐴 ∧ {𝑧} ⊆ 𝐴) ↔ (𝑥 ∪ {𝑧}) ⊆ 𝐴)
4645biimpi 216 . . . . . . . . . . . . . . . . . . . 20 ((𝑥𝐴 ∧ {𝑧} ⊆ 𝐴) → (𝑥 ∪ {𝑧}) ⊆ 𝐴)
4744, 46sylan2 593 . . . . . . . . . . . . . . . . . . 19 ((𝑥𝐴𝑧 ∈ (𝐴𝑥)) → (𝑥 ∪ {𝑧}) ⊆ 𝐴)
4847ad2ant2r 747 . . . . . . . . . . . . . . . . . 18 (((𝑥𝐴𝑓:𝑥1-1-onto𝑚) ∧ (𝑧 ∈ (𝐴𝑥) ∧ 𝑚 ∈ ω)) → (𝑥 ∪ {𝑧}) ⊆ 𝐴)
49 vex 3481 . . . . . . . . . . . . . . . . . . . . . . 23 𝑧 ∈ V
50 vex 3481 . . . . . . . . . . . . . . . . . . . . . . 23 𝑚 ∈ V
5149, 50f1osn 6888 . . . . . . . . . . . . . . . . . . . . . 22 {⟨𝑧, 𝑚⟩}:{𝑧}–1-1-onto→{𝑚}
5251jctr 524 . . . . . . . . . . . . . . . . . . . . 21 (𝑓:𝑥1-1-onto𝑚 → (𝑓:𝑥1-1-onto𝑚 ∧ {⟨𝑧, 𝑚⟩}:{𝑧}–1-1-onto→{𝑚}))
53 eldifn 4141 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 ∈ (𝐴𝑥) → ¬ 𝑧𝑥)
54 disjsn 4715 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧𝑥)
5553, 54sylibr 234 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ (𝐴𝑥) → (𝑥 ∩ {𝑧}) = ∅)
56 nnord 7894 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑚 ∈ ω → Ord 𝑚)
57 orddisj 6423 . . . . . . . . . . . . . . . . . . . . . . 23 (Ord 𝑚 → (𝑚 ∩ {𝑚}) = ∅)
5856, 57syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 ∈ ω → (𝑚 ∩ {𝑚}) = ∅)
5955, 58anim12i 613 . . . . . . . . . . . . . . . . . . . . 21 ((𝑧 ∈ (𝐴𝑥) ∧ 𝑚 ∈ ω) → ((𝑥 ∩ {𝑧}) = ∅ ∧ (𝑚 ∩ {𝑚}) = ∅))
60 f1oun 6867 . . . . . . . . . . . . . . . . . . . . 21 (((𝑓:𝑥1-1-onto𝑚 ∧ {⟨𝑧, 𝑚⟩}:{𝑧}–1-1-onto→{𝑚}) ∧ ((𝑥 ∩ {𝑧}) = ∅ ∧ (𝑚 ∩ {𝑚}) = ∅)) → (𝑓 ∪ {⟨𝑧, 𝑚⟩}):(𝑥 ∪ {𝑧})–1-1-onto→(𝑚 ∪ {𝑚}))
6152, 59, 60syl2an 596 . . . . . . . . . . . . . . . . . . . 20 ((𝑓:𝑥1-1-onto𝑚 ∧ (𝑧 ∈ (𝐴𝑥) ∧ 𝑚 ∈ ω)) → (𝑓 ∪ {⟨𝑧, 𝑚⟩}):(𝑥 ∪ {𝑧})–1-1-onto→(𝑚 ∪ {𝑚}))
62 df-suc 6391 . . . . . . . . . . . . . . . . . . . . . 22 suc 𝑚 = (𝑚 ∪ {𝑚})
63 f1oeq3 6838 . . . . . . . . . . . . . . . . . . . . . 22 (suc 𝑚 = (𝑚 ∪ {𝑚}) → ((𝑓 ∪ {⟨𝑧, 𝑚⟩}):(𝑥 ∪ {𝑧})–1-1-onto→suc 𝑚 ↔ (𝑓 ∪ {⟨𝑧, 𝑚⟩}):(𝑥 ∪ {𝑧})–1-1-onto→(𝑚 ∪ {𝑚})))
6462, 63ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓 ∪ {⟨𝑧, 𝑚⟩}):(𝑥 ∪ {𝑧})–1-1-onto→suc 𝑚 ↔ (𝑓 ∪ {⟨𝑧, 𝑚⟩}):(𝑥 ∪ {𝑧})–1-1-onto→(𝑚 ∪ {𝑚}))
65 vex 3481 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑓 ∈ V
66 snex 5441 . . . . . . . . . . . . . . . . . . . . . . . 24 {⟨𝑧, 𝑚⟩} ∈ V
6765, 66unex 7762 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 ∪ {⟨𝑧, 𝑚⟩}) ∈ V
68 f1oeq1 6836 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑚⟩}) → (𝑔:(𝑥 ∪ {𝑧})–1-1-onto→suc 𝑚 ↔ (𝑓 ∪ {⟨𝑧, 𝑚⟩}):(𝑥 ∪ {𝑧})–1-1-onto→suc 𝑚))
6967, 68spcev 3605 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓 ∪ {⟨𝑧, 𝑚⟩}):(𝑥 ∪ {𝑧})–1-1-onto→suc 𝑚 → ∃𝑔 𝑔:(𝑥 ∪ {𝑧})–1-1-onto→suc 𝑚)
70 bren 8993 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥 ∪ {𝑧}) ≈ suc 𝑚 ↔ ∃𝑔 𝑔:(𝑥 ∪ {𝑧})–1-1-onto→suc 𝑚)
7169, 70sylibr 234 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓 ∪ {⟨𝑧, 𝑚⟩}):(𝑥 ∪ {𝑧})–1-1-onto→suc 𝑚 → (𝑥 ∪ {𝑧}) ≈ suc 𝑚)
7264, 71sylbir 235 . . . . . . . . . . . . . . . . . . . 20 ((𝑓 ∪ {⟨𝑧, 𝑚⟩}):(𝑥 ∪ {𝑧})–1-1-onto→(𝑚 ∪ {𝑚}) → (𝑥 ∪ {𝑧}) ≈ suc 𝑚)
7361, 72syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝑓:𝑥1-1-onto𝑚 ∧ (𝑧 ∈ (𝐴𝑥) ∧ 𝑚 ∈ ω)) → (𝑥 ∪ {𝑧}) ≈ suc 𝑚)
7473adantll 714 . . . . . . . . . . . . . . . . . 18 (((𝑥𝐴𝑓:𝑥1-1-onto𝑚) ∧ (𝑧 ∈ (𝐴𝑥) ∧ 𝑚 ∈ ω)) → (𝑥 ∪ {𝑧}) ≈ suc 𝑚)
75 vex 3481 . . . . . . . . . . . . . . . . . . . 20 𝑥 ∈ V
76 snex 5441 . . . . . . . . . . . . . . . . . . . 20 {𝑧} ∈ V
7775, 76unex 7762 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∪ {𝑧}) ∈ V
78 sseq1 4020 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝑥 ∪ {𝑧}) → (𝑦𝐴 ↔ (𝑥 ∪ {𝑧}) ⊆ 𝐴))
79 breq1 5150 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝑥 ∪ {𝑧}) → (𝑦 ≈ suc 𝑚 ↔ (𝑥 ∪ {𝑧}) ≈ suc 𝑚))
8078, 79anbi12d 632 . . . . . . . . . . . . . . . . . . 19 (𝑦 = (𝑥 ∪ {𝑧}) → ((𝑦𝐴𝑦 ≈ suc 𝑚) ↔ ((𝑥 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝑥 ∪ {𝑧}) ≈ suc 𝑚)))
8177, 80spcev 3605 . . . . . . . . . . . . . . . . . 18 (((𝑥 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝑥 ∪ {𝑧}) ≈ suc 𝑚) → ∃𝑦(𝑦𝐴𝑦 ≈ suc 𝑚))
8248, 74, 81syl2anc 584 . . . . . . . . . . . . . . . . 17 (((𝑥𝐴𝑓:𝑥1-1-onto𝑚) ∧ (𝑧 ∈ (𝐴𝑥) ∧ 𝑚 ∈ ω)) → ∃𝑦(𝑦𝐴𝑦 ≈ suc 𝑚))
8382expcom 413 . . . . . . . . . . . . . . . 16 ((𝑧 ∈ (𝐴𝑥) ∧ 𝑚 ∈ ω) → ((𝑥𝐴𝑓:𝑥1-1-onto𝑚) → ∃𝑦(𝑦𝐴𝑦 ≈ suc 𝑚)))
8483ex 412 . . . . . . . . . . . . . . 15 (𝑧 ∈ (𝐴𝑥) → (𝑚 ∈ ω → ((𝑥𝐴𝑓:𝑥1-1-onto𝑚) → ∃𝑦(𝑦𝐴𝑦 ≈ suc 𝑚))))
8584exlimiv 1927 . . . . . . . . . . . . . 14 (∃𝑧 𝑧 ∈ (𝐴𝑥) → (𝑚 ∈ ω → ((𝑥𝐴𝑓:𝑥1-1-onto𝑚) → ∃𝑦(𝑦𝐴𝑦 ≈ suc 𝑚))))
8642, 85sylbi 217 . . . . . . . . . . . . 13 (¬ (𝐴𝑥) = ∅ → (𝑚 ∈ ω → ((𝑥𝐴𝑓:𝑥1-1-onto𝑚) → ∃𝑦(𝑦𝐴𝑦 ≈ suc 𝑚))))
8786com13 88 . . . . . . . . . . . 12 ((𝑥𝐴𝑓:𝑥1-1-onto𝑚) → (𝑚 ∈ ω → (¬ (𝐴𝑥) = ∅ → ∃𝑦(𝑦𝐴𝑦 ≈ suc 𝑚))))
8887expcom 413 . . . . . . . . . . 11 (𝑓:𝑥1-1-onto𝑚 → (𝑥𝐴 → (𝑚 ∈ ω → (¬ (𝐴𝑥) = ∅ → ∃𝑦(𝑦𝐴𝑦 ≈ suc 𝑚)))))
8988exlimiv 1927 . . . . . . . . . 10 (∃𝑓 𝑓:𝑥1-1-onto𝑚 → (𝑥𝐴 → (𝑚 ∈ ω → (¬ (𝐴𝑥) = ∅ → ∃𝑦(𝑦𝐴𝑦 ≈ suc 𝑚)))))
9041, 89sylbi 217 . . . . . . . . 9 (𝑥𝑚 → (𝑥𝐴 → (𝑚 ∈ ω → (¬ (𝐴𝑥) = ∅ → ∃𝑦(𝑦𝐴𝑦 ≈ suc 𝑚)))))
91903imp21 1113 . . . . . . . 8 ((𝑥𝐴𝑥𝑚𝑚 ∈ ω) → (¬ (𝐴𝑥) = ∅ → ∃𝑦(𝑦𝐴𝑦 ≈ suc 𝑚)))
9240, 91syld 47 . . . . . . 7 ((𝑥𝐴𝑥𝑚𝑚 ∈ ω) → (¬ 𝐴 ∈ Fin → ∃𝑦(𝑦𝐴𝑦 ≈ suc 𝑚)))
93923expia 1120 . . . . . 6 ((𝑥𝐴𝑥𝑚) → (𝑚 ∈ ω → (¬ 𝐴 ∈ Fin → ∃𝑦(𝑦𝐴𝑦 ≈ suc 𝑚))))
9493exlimiv 1927 . . . . 5 (∃𝑥(𝑥𝐴𝑥𝑚) → (𝑚 ∈ ω → (¬ 𝐴 ∈ Fin → ∃𝑦(𝑦𝐴𝑦 ≈ suc 𝑚))))
9594com3l 89 . . . 4 (𝑚 ∈ ω → (¬ 𝐴 ∈ Fin → (∃𝑥(𝑥𝐴𝑥𝑚) → ∃𝑦(𝑦𝐴𝑦 ≈ suc 𝑚))))
963, 6, 13, 24, 95finds2 7920 . . 3 (𝑛 ∈ ω → (¬ 𝐴 ∈ Fin → ∃𝑥(𝑥𝐴𝑥𝑛)))
9796com12 32 . 2 𝐴 ∈ Fin → (𝑛 ∈ ω → ∃𝑥(𝑥𝐴𝑥𝑛)))
9897ralrimiv 3142 1 𝐴 ∈ Fin → ∀𝑛 ∈ ω ∃𝑥(𝑥𝐴𝑥𝑛))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  w3a 1086   = wceq 1536  wex 1775  wcel 2105  wral 3058  wrex 3067  cdif 3959  cun 3960  cin 3961  wss 3962  c0 4338  {csn 4630  cop 4636   class class class wbr 5147  Ord word 6384  suc csuc 6387  1-1-ontowf1o 6561  ωcom 7886  cen 8980  Fincfn 8983
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437  ax-un 7753
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-om 7887  df-en 8984  df-fin 8987
This theorem is referenced by:  fineqvlem  9295  isinffi  10029  domtriomlem  10479  ishashinf  14498  prcinf  35086  ctbssinf  37388
  Copyright terms: Public domain W3C validator