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

Theorem isinf 8124
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.)
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 4622 . . . . . 6 (𝑛 = ∅ → (𝑥𝑛𝑥 ≈ ∅))
21anbi2d 739 . . . . 5 (𝑛 = ∅ → ((𝑥𝐴𝑥𝑛) ↔ (𝑥𝐴𝑥 ≈ ∅)))
32exbidv 1847 . . . 4 (𝑛 = ∅ → (∃𝑥(𝑥𝐴𝑥𝑛) ↔ ∃𝑥(𝑥𝐴𝑥 ≈ ∅)))
4 breq2 4622 . . . . . 6 (𝑛 = 𝑚 → (𝑥𝑛𝑥𝑚))
54anbi2d 739 . . . . 5 (𝑛 = 𝑚 → ((𝑥𝐴𝑥𝑛) ↔ (𝑥𝐴𝑥𝑚)))
65exbidv 1847 . . . 4 (𝑛 = 𝑚 → (∃𝑥(𝑥𝐴𝑥𝑛) ↔ ∃𝑥(𝑥𝐴𝑥𝑚)))
7 sseq1 3610 . . . . . . 7 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
87adantl 482 . . . . . 6 ((𝑛 = suc 𝑚𝑥 = 𝑦) → (𝑥𝐴𝑦𝐴))
9 breq1 4621 . . . . . . 7 (𝑥 = 𝑦 → (𝑥𝑛𝑦𝑛))
10 breq2 4622 . . . . . . 7 (𝑛 = suc 𝑚 → (𝑦𝑛𝑦 ≈ suc 𝑚))
119, 10sylan9bbr 736 . . . . . 6 ((𝑛 = suc 𝑚𝑥 = 𝑦) → (𝑥𝑛𝑦 ≈ suc 𝑚))
128, 11anbi12d 746 . . . . 5 ((𝑛 = suc 𝑚𝑥 = 𝑦) → ((𝑥𝐴𝑥𝑛) ↔ (𝑦𝐴𝑦 ≈ suc 𝑚)))
1312cbvexdva 2282 . . . 4 (𝑛 = suc 𝑚 → (∃𝑥(𝑥𝐴𝑥𝑛) ↔ ∃𝑦(𝑦𝐴𝑦 ≈ suc 𝑚)))
14 0ss 3949 . . . . . 6 ∅ ⊆ 𝐴
15 0ex 4755 . . . . . . 7 ∅ ∈ V
1615enref 7939 . . . . . 6 ∅ ≈ ∅
17 sseq1 3610 . . . . . . . 8 (𝑥 = ∅ → (𝑥𝐴 ↔ ∅ ⊆ 𝐴))
18 breq1 4621 . . . . . . . 8 (𝑥 = ∅ → (𝑥 ≈ ∅ ↔ ∅ ≈ ∅))
1917, 18anbi12d 746 . . . . . . 7 (𝑥 = ∅ → ((𝑥𝐴𝑥 ≈ ∅) ↔ (∅ ⊆ 𝐴 ∧ ∅ ≈ ∅)))
2015, 19spcev 3289 . . . . . 6 ((∅ ⊆ 𝐴 ∧ ∅ ≈ ∅) → ∃𝑥(𝑥𝐴𝑥 ≈ ∅))
2114, 16, 20mp2an 707 . . . . 5 𝑥(𝑥𝐴𝑥 ≈ ∅)
2221a1i 11 . . . 4 𝐴 ∈ Fin → ∃𝑥(𝑥𝐴𝑥 ≈ ∅))
23 ssdif0 3921 . . . . . . . . . . . . 13 (𝐴𝑥 ↔ (𝐴𝑥) = ∅)
24 eqss 3602 . . . . . . . . . . . . . . 15 (𝑥 = 𝐴 ↔ (𝑥𝐴𝐴𝑥))
25 breq1 4621 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝐴 → (𝑥𝑚𝐴𝑚))
2625biimpa 501 . . . . . . . . . . . . . . . . . 18 ((𝑥 = 𝐴𝑥𝑚) → 𝐴𝑚)
27 rspe 2998 . . . . . . . . . . . . . . . . . 18 ((𝑚 ∈ ω ∧ 𝐴𝑚) → ∃𝑚 ∈ ω 𝐴𝑚)
2826, 27sylan2 491 . . . . . . . . . . . . . . . . 17 ((𝑚 ∈ ω ∧ (𝑥 = 𝐴𝑥𝑚)) → ∃𝑚 ∈ ω 𝐴𝑚)
29 isfi 7930 . . . . . . . . . . . . . . . . 17 (𝐴 ∈ Fin ↔ ∃𝑚 ∈ ω 𝐴𝑚)
3028, 29sylibr 224 . . . . . . . . . . . . . . . 16 ((𝑚 ∈ ω ∧ (𝑥 = 𝐴𝑥𝑚)) → 𝐴 ∈ Fin)
3130expcom 451 . . . . . . . . . . . . . . 15 ((𝑥 = 𝐴𝑥𝑚) → (𝑚 ∈ ω → 𝐴 ∈ Fin))
3224, 31sylanbr 490 . . . . . . . . . . . . . 14 (((𝑥𝐴𝐴𝑥) ∧ 𝑥𝑚) → (𝑚 ∈ ω → 𝐴 ∈ Fin))
3332ex 450 . . . . . . . . . . . . 13 ((𝑥𝐴𝐴𝑥) → (𝑥𝑚 → (𝑚 ∈ ω → 𝐴 ∈ Fin)))
3423, 33sylan2br 493 . . . . . . . . . . . 12 ((𝑥𝐴 ∧ (𝐴𝑥) = ∅) → (𝑥𝑚 → (𝑚 ∈ ω → 𝐴 ∈ Fin)))
3534expcom 451 . . . . . . . . . . 11 ((𝐴𝑥) = ∅ → (𝑥𝐴 → (𝑥𝑚 → (𝑚 ∈ ω → 𝐴 ∈ Fin))))
36353impd 1278 . . . . . . . . . 10 ((𝐴𝑥) = ∅ → ((𝑥𝐴𝑥𝑚𝑚 ∈ ω) → 𝐴 ∈ Fin))
3736com12 32 . . . . . . . . 9 ((𝑥𝐴𝑥𝑚𝑚 ∈ ω) → ((𝐴𝑥) = ∅ → 𝐴 ∈ Fin))
3837con3d 148 . . . . . . . 8 ((𝑥𝐴𝑥𝑚𝑚 ∈ ω) → (¬ 𝐴 ∈ Fin → ¬ (𝐴𝑥) = ∅))
39 bren 7915 . . . . . . . . . . 11 (𝑥𝑚 ↔ ∃𝑓 𝑓:𝑥1-1-onto𝑚)
40 neq0 3911 . . . . . . . . . . . . . . 15 (¬ (𝐴𝑥) = ∅ ↔ ∃𝑧 𝑧 ∈ (𝐴𝑥))
41 eldifi 3715 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ (𝐴𝑥) → 𝑧𝐴)
4241snssd 4314 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ∈ (𝐴𝑥) → {𝑧} ⊆ 𝐴)
43 unss 3770 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥𝐴 ∧ {𝑧} ⊆ 𝐴) ↔ (𝑥 ∪ {𝑧}) ⊆ 𝐴)
4443biimpi 206 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥𝐴 ∧ {𝑧} ⊆ 𝐴) → (𝑥 ∪ {𝑧}) ⊆ 𝐴)
4542, 44sylan2 491 . . . . . . . . . . . . . . . . . . . 20 ((𝑥𝐴𝑧 ∈ (𝐴𝑥)) → (𝑥 ∪ {𝑧}) ⊆ 𝐴)
4645ad2ant2r 782 . . . . . . . . . . . . . . . . . . 19 (((𝑥𝐴𝑓:𝑥1-1-onto𝑚) ∧ (𝑧 ∈ (𝐴𝑥) ∧ 𝑚 ∈ ω)) → (𝑥 ∪ {𝑧}) ⊆ 𝐴)
47 vex 3192 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑧 ∈ V
48 vex 3192 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑚 ∈ V
4947, 48f1osn 6138 . . . . . . . . . . . . . . . . . . . . . . 23 {⟨𝑧, 𝑚⟩}:{𝑧}–1-1-onto→{𝑚}
5049jctr 564 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓:𝑥1-1-onto𝑚 → (𝑓:𝑥1-1-onto𝑚 ∧ {⟨𝑧, 𝑚⟩}:{𝑧}–1-1-onto→{𝑚}))
51 eldifn 3716 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 ∈ (𝐴𝑥) → ¬ 𝑧𝑥)
52 disjsn 4221 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑥 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧𝑥)
5351, 52sylibr 224 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 ∈ (𝐴𝑥) → (𝑥 ∩ {𝑧}) = ∅)
54 nnord 7027 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑚 ∈ ω → Ord 𝑚)
55 orddisj 5726 . . . . . . . . . . . . . . . . . . . . . . . 24 (Ord 𝑚 → (𝑚 ∩ {𝑚}) = ∅)
5654, 55syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑚 ∈ ω → (𝑚 ∩ {𝑚}) = ∅)
5753, 56anim12i 589 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑧 ∈ (𝐴𝑥) ∧ 𝑚 ∈ ω) → ((𝑥 ∩ {𝑧}) = ∅ ∧ (𝑚 ∩ {𝑚}) = ∅))
58 f1oun 6118 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑓:𝑥1-1-onto𝑚 ∧ {⟨𝑧, 𝑚⟩}:{𝑧}–1-1-onto→{𝑚}) ∧ ((𝑥 ∩ {𝑧}) = ∅ ∧ (𝑚 ∩ {𝑚}) = ∅)) → (𝑓 ∪ {⟨𝑧, 𝑚⟩}):(𝑥 ∪ {𝑧})–1-1-onto→(𝑚 ∪ {𝑚}))
5950, 57, 58syl2an 494 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓:𝑥1-1-onto𝑚 ∧ (𝑧 ∈ (𝐴𝑥) ∧ 𝑚 ∈ ω)) → (𝑓 ∪ {⟨𝑧, 𝑚⟩}):(𝑥 ∪ {𝑧})–1-1-onto→(𝑚 ∪ {𝑚}))
60 df-suc 5693 . . . . . . . . . . . . . . . . . . . . . . 23 suc 𝑚 = (𝑚 ∪ {𝑚})
61 f1oeq3 6091 . . . . . . . . . . . . . . . . . . . . . . 23 (suc 𝑚 = (𝑚 ∪ {𝑚}) → ((𝑓 ∪ {⟨𝑧, 𝑚⟩}):(𝑥 ∪ {𝑧})–1-1-onto→suc 𝑚 ↔ (𝑓 ∪ {⟨𝑧, 𝑚⟩}):(𝑥 ∪ {𝑧})–1-1-onto→(𝑚 ∪ {𝑚})))
6260, 61ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓 ∪ {⟨𝑧, 𝑚⟩}):(𝑥 ∪ {𝑧})–1-1-onto→suc 𝑚 ↔ (𝑓 ∪ {⟨𝑧, 𝑚⟩}):(𝑥 ∪ {𝑧})–1-1-onto→(𝑚 ∪ {𝑚}))
63 vex 3192 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑓 ∈ V
64 snex 4874 . . . . . . . . . . . . . . . . . . . . . . . . 25 {⟨𝑧, 𝑚⟩} ∈ V
6563, 64unex 6916 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 ∪ {⟨𝑧, 𝑚⟩}) ∈ V
66 f1oeq1 6089 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑚⟩}) → (𝑔:(𝑥 ∪ {𝑧})–1-1-onto→suc 𝑚 ↔ (𝑓 ∪ {⟨𝑧, 𝑚⟩}):(𝑥 ∪ {𝑧})–1-1-onto→suc 𝑚))
6765, 66spcev 3289 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓 ∪ {⟨𝑧, 𝑚⟩}):(𝑥 ∪ {𝑧})–1-1-onto→suc 𝑚 → ∃𝑔 𝑔:(𝑥 ∪ {𝑧})–1-1-onto→suc 𝑚)
68 bren 7915 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥 ∪ {𝑧}) ≈ suc 𝑚 ↔ ∃𝑔 𝑔:(𝑥 ∪ {𝑧})–1-1-onto→suc 𝑚)
6967, 68sylibr 224 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓 ∪ {⟨𝑧, 𝑚⟩}):(𝑥 ∪ {𝑧})–1-1-onto→suc 𝑚 → (𝑥 ∪ {𝑧}) ≈ suc 𝑚)
7062, 69sylbir 225 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓 ∪ {⟨𝑧, 𝑚⟩}):(𝑥 ∪ {𝑧})–1-1-onto→(𝑚 ∪ {𝑚}) → (𝑥 ∪ {𝑧}) ≈ suc 𝑚)
7159, 70syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑓:𝑥1-1-onto𝑚 ∧ (𝑧 ∈ (𝐴𝑥) ∧ 𝑚 ∈ ω)) → (𝑥 ∪ {𝑧}) ≈ suc 𝑚)
7271adantll 749 . . . . . . . . . . . . . . . . . . 19 (((𝑥𝐴𝑓:𝑥1-1-onto𝑚) ∧ (𝑧 ∈ (𝐴𝑥) ∧ 𝑚 ∈ ω)) → (𝑥 ∪ {𝑧}) ≈ suc 𝑚)
73 vex 3192 . . . . . . . . . . . . . . . . . . . . 21 𝑥 ∈ V
74 snex 4874 . . . . . . . . . . . . . . . . . . . . 21 {𝑧} ∈ V
7573, 74unex 6916 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∪ {𝑧}) ∈ V
76 sseq1 3610 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = (𝑥 ∪ {𝑧}) → (𝑦𝐴 ↔ (𝑥 ∪ {𝑧}) ⊆ 𝐴))
77 breq1 4621 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = (𝑥 ∪ {𝑧}) → (𝑦 ≈ suc 𝑚 ↔ (𝑥 ∪ {𝑧}) ≈ suc 𝑚))
7876, 77anbi12d 746 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝑥 ∪ {𝑧}) → ((𝑦𝐴𝑦 ≈ suc 𝑚) ↔ ((𝑥 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝑥 ∪ {𝑧}) ≈ suc 𝑚)))
7975, 78spcev 3289 . . . . . . . . . . . . . . . . . . 19 (((𝑥 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝑥 ∪ {𝑧}) ≈ suc 𝑚) → ∃𝑦(𝑦𝐴𝑦 ≈ suc 𝑚))
8046, 72, 79syl2anc 692 . . . . . . . . . . . . . . . . . 18 (((𝑥𝐴𝑓:𝑥1-1-onto𝑚) ∧ (𝑧 ∈ (𝐴𝑥) ∧ 𝑚 ∈ ω)) → ∃𝑦(𝑦𝐴𝑦 ≈ suc 𝑚))
8180expcom 451 . . . . . . . . . . . . . . . . 17 ((𝑧 ∈ (𝐴𝑥) ∧ 𝑚 ∈ ω) → ((𝑥𝐴𝑓:𝑥1-1-onto𝑚) → ∃𝑦(𝑦𝐴𝑦 ≈ suc 𝑚)))
8281ex 450 . . . . . . . . . . . . . . . 16 (𝑧 ∈ (𝐴𝑥) → (𝑚 ∈ ω → ((𝑥𝐴𝑓:𝑥1-1-onto𝑚) → ∃𝑦(𝑦𝐴𝑦 ≈ suc 𝑚))))
8382exlimiv 1855 . . . . . . . . . . . . . . 15 (∃𝑧 𝑧 ∈ (𝐴𝑥) → (𝑚 ∈ ω → ((𝑥𝐴𝑓:𝑥1-1-onto𝑚) → ∃𝑦(𝑦𝐴𝑦 ≈ suc 𝑚))))
8440, 83sylbi 207 . . . . . . . . . . . . . 14 (¬ (𝐴𝑥) = ∅ → (𝑚 ∈ ω → ((𝑥𝐴𝑓:𝑥1-1-onto𝑚) → ∃𝑦(𝑦𝐴𝑦 ≈ suc 𝑚))))
8584com13 88 . . . . . . . . . . . . 13 ((𝑥𝐴𝑓:𝑥1-1-onto𝑚) → (𝑚 ∈ ω → (¬ (𝐴𝑥) = ∅ → ∃𝑦(𝑦𝐴𝑦 ≈ suc 𝑚))))
8685expcom 451 . . . . . . . . . . . 12 (𝑓:𝑥1-1-onto𝑚 → (𝑥𝐴 → (𝑚 ∈ ω → (¬ (𝐴𝑥) = ∅ → ∃𝑦(𝑦𝐴𝑦 ≈ suc 𝑚)))))
8786exlimiv 1855 . . . . . . . . . . 11 (∃𝑓 𝑓:𝑥1-1-onto𝑚 → (𝑥𝐴 → (𝑚 ∈ ω → (¬ (𝐴𝑥) = ∅ → ∃𝑦(𝑦𝐴𝑦 ≈ suc 𝑚)))))
8839, 87sylbi 207 . . . . . . . . . 10 (𝑥𝑚 → (𝑥𝐴 → (𝑚 ∈ ω → (¬ (𝐴𝑥) = ∅ → ∃𝑦(𝑦𝐴𝑦 ≈ suc 𝑚)))))
8988com12 32 . . . . . . . . 9 (𝑥𝐴 → (𝑥𝑚 → (𝑚 ∈ ω → (¬ (𝐴𝑥) = ∅ → ∃𝑦(𝑦𝐴𝑦 ≈ suc 𝑚)))))
90893imp 1254 . . . . . . . 8 ((𝑥𝐴𝑥𝑚𝑚 ∈ ω) → (¬ (𝐴𝑥) = ∅ → ∃𝑦(𝑦𝐴𝑦 ≈ suc 𝑚)))
9138, 90syld 47 . . . . . . 7 ((𝑥𝐴𝑥𝑚𝑚 ∈ ω) → (¬ 𝐴 ∈ Fin → ∃𝑦(𝑦𝐴𝑦 ≈ suc 𝑚)))
92913expia 1264 . . . . . 6 ((𝑥𝐴𝑥𝑚) → (𝑚 ∈ ω → (¬ 𝐴 ∈ Fin → ∃𝑦(𝑦𝐴𝑦 ≈ suc 𝑚))))
9392exlimiv 1855 . . . . 5 (∃𝑥(𝑥𝐴𝑥𝑚) → (𝑚 ∈ ω → (¬ 𝐴 ∈ Fin → ∃𝑦(𝑦𝐴𝑦 ≈ suc 𝑚))))
9493com3l 89 . . . 4 (𝑚 ∈ ω → (¬ 𝐴 ∈ Fin → (∃𝑥(𝑥𝐴𝑥𝑚) → ∃𝑦(𝑦𝐴𝑦 ≈ suc 𝑚))))
953, 6, 13, 22, 94finds2 7048 . . 3 (𝑛 ∈ ω → (¬ 𝐴 ∈ Fin → ∃𝑥(𝑥𝐴𝑥𝑛)))
9695com12 32 . 2 𝐴 ∈ Fin → (𝑛 ∈ ω → ∃𝑥(𝑥𝐴𝑥𝑛)))
9796ralrimiv 2960 1 𝐴 ∈ Fin → ∀𝑛 ∈ ω ∃𝑥(𝑥𝐴𝑥𝑛))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384  w3a 1036   = wceq 1480  wex 1701  wcel 1987  wral 2907  wrex 2908  cdif 3556  cun 3557  cin 3558  wss 3559  c0 3896  {csn 4153  cop 4159   class class class wbr 4618  Ord word 5686  suc csuc 5689  1-1-ontowf1o 5851  ωcom 7019  cen 7903  Fincfn 7906
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3191  df-sbc 3422  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-br 4619  df-opab 4679  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-om 7020  df-en 7907  df-fin 7910
This theorem is referenced by:  fineqvlem  8125  isinffi  8769  domtriomlem  9215  ishashinf  13192
  Copyright terms: Public domain W3C validator