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 → ∃ f f : B ⟶ 1-1 A

Proof

Step Hyp Ref Expression
1 ficardom ⊢ B ∈ Fin → card ⁡ B ∈ ω
2 isinf ⊢ ¬ A ∈ Fin → ∀ a ∈ ω ∃ c c ⊆ 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 → ∃ c c ⊆ A ∧ c ≈ a ↔ ∃ c c ⊆ A ∧ c ≈ card ⁡ B
6 5 rspcva ⊢ card ⁡ B ∈ ω ∧ ∀ a ∈ ω ∃ c c ⊆ A ∧ c ≈ a → ∃ c c ⊆ A ∧ c ≈ card ⁡ B
7 1 2 6 syl2anr ⊢ ¬ A ∈ Fin ∧ B ∈ Fin → ∃ c c ⊆ 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 ↔ ∃ f f : B ⟶ 1-1 onto c
15 13 14 sylib ⊢ ¬ A ∈ Fin ∧ B ∈ Fin ∧ c ⊆ A ∧ c ≈ card ⁡ B → ∃ f f : B ⟶ 1-1 onto c
16 f1of1 ⊢ f : B ⟶ 1-1 onto c → f : B ⟶ 1-1 c
17 simplrl ⊢ ¬ A ∈ Fin ∧ B ∈ Fin ∧ c ⊆ A ∧ c ≈ card ⁡ B ∧ f : B ⟶ 1-1 onto c → c ⊆ A
18 f1ss ⊢ f : B ⟶ 1-1 c ∧ c ⊆ A → f : B ⟶ 1-1 A
19 16 17 18 syl2an2 ⊢ ¬ A ∈ Fin ∧ B ∈ Fin ∧ c ⊆ A ∧ c ≈ card ⁡ B ∧ f : B ⟶ 1-1 onto c → f : B ⟶ 1-1 A
20 19 ex ⊢ ¬ A ∈ Fin ∧ B ∈ Fin ∧ c ⊆ A ∧ c ≈ card ⁡ B → f : B ⟶ 1-1 onto c → f : B ⟶ 1-1 A
21 20 eximdv ⊢ ¬ A ∈ Fin ∧ B ∈ Fin ∧ c ⊆ A ∧ c ≈ card ⁡ B → ∃ f f : B ⟶ 1-1 onto c → ∃ f f : B ⟶ 1-1 A
22 15 21 mpd ⊢ ¬ A ∈ Fin ∧ B ∈ Fin ∧ c ⊆ A ∧ c ≈ card ⁡ B → ∃ f f : B ⟶ 1-1 A
23 7 22 exlimddv ⊢ ¬ A ∈ Fin ∧ B ∈ Fin → ∃ f f : B ⟶ 1-1 A