Metamath Proof Explorer

Theorem isinffi

Description: An infinite set contains subsets equinumerous to every finite set. Extension of isinf from finite ordinals to all finite sets. (Contributed by Stefan O'Rear, 8-Oct-2014)

Ref Expression
Assertion isinffi ⊢¬A∈Fin∧B∈Fin→∃ff:B⟶1-1A

Proof

Step Hyp Ref Expression
1 ficardom ⊢B∈Fin→card⁡B∈ω
2 isinf ⊢¬A∈Fin→∀a∈ω∃cc⊆A∧c≈a
3 breq2 ⊢a=card⁡B→c≈a↔c≈card⁡B
4 3 anbi2d ⊢a=card⁡B→c⊆A∧c≈a↔c⊆A∧c≈card⁡B
5 4 exbidv ⊢a=card⁡B→∃cc⊆A∧c≈a↔∃cc⊆A∧c≈card⁡B
6 5 rspcva ⊢card⁡B∈ω∧∀a∈ω∃cc⊆A∧c≈a→∃cc⊆A∧c≈card⁡B
7 1 2 6 syl2anr ⊢¬A∈Fin∧B∈Fin→∃cc⊆A∧c≈card⁡B
8 simprr ⊢¬A∈Fin∧B∈Fin∧c⊆A∧c≈card⁡B→c≈card⁡B
9 ficardid ⊢B∈Fin→card⁡B≈B
10 9 ad2antlr ⊢¬A∈Fin∧B∈Fin∧c⊆A∧c≈card⁡B→card⁡B≈B
11 entr ⊢c≈card⁡B∧card⁡B≈B→c≈B
12 8 10 11 syl2anc ⊢¬A∈Fin∧B∈Fin∧c⊆A∧c≈card⁡B→c≈B
13 12 ensymd ⊢¬A∈Fin∧B∈Fin∧c⊆A∧c≈card⁡B→B≈c
14 bren ⊢B≈c↔∃ff:B⟶1-1 ontoc
15 13 14 sylib ⊢¬A∈Fin∧B∈Fin∧c⊆A∧c≈card⁡B→∃ff:B⟶1-1 ontoc
16 f1of1 ⊢f:B⟶1-1 ontoc→f:B⟶1-1c
17 simplrl ⊢¬A∈Fin∧B∈Fin∧c⊆A∧c≈card⁡B∧f:B⟶1-1 ontoc→c⊆A
18 f1ss ⊢f:B⟶1-1c∧c⊆A→f:B⟶1-1A
19 16 17 18 syl2an2 ⊢¬A∈Fin∧B∈Fin∧c⊆A∧c≈card⁡B∧f:B⟶1-1 ontoc→f:B⟶1-1A
20 19 ex ⊢¬A∈Fin∧B∈Fin∧c⊆A∧c≈card⁡B→f:B⟶1-1 ontoc→f:B⟶1-1A
21 20 eximdv ⊢¬A∈Fin∧B∈Fin∧c⊆A∧c≈card⁡B→∃ff:B⟶1-1 ontoc→∃ff:B⟶1-1A
22 15 21 mpd ⊢¬A∈Fin∧B∈Fin∧c⊆A∧c≈card⁡B→∃ff:B⟶1-1A
23 7 22 exlimddv ⊢¬A∈Fin∧B∈Fin→∃ff:B⟶1-1A