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 ( ( ¬ 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ∃ 𝑓 𝑓 : 𝐵 –1-1→ 𝐴 )

Proof

Step Hyp Ref Expression
1 ficardom ⊢ ( 𝐵 ∈ Fin → ( card ‘ 𝐵 ) ∈ ω )
2 isinf ⊢ ( ¬ 𝐴 ∈ Fin → ∀ 𝑎 ∈ ω ∃ 𝑐 ( 𝑐 ⊆ 𝐴 ∧ 𝑐 ≈ 𝑎 ) )
3 breq2 ⊢ ( 𝑎 = ( card ‘ 𝐵 ) → ( 𝑐 ≈ 𝑎 ↔ 𝑐 ≈ ( card ‘ 𝐵 ) ) )
4 3 anbi2d ⊢ ( 𝑎 = ( card ‘ 𝐵 ) → ( ( 𝑐 ⊆ 𝐴 ∧ 𝑐 ≈ 𝑎 ) ↔ ( 𝑐 ⊆ 𝐴 ∧ 𝑐 ≈ ( card ‘ 𝐵 ) ) ) )
5 4 exbidv ⊢ ( 𝑎 = ( card ‘ 𝐵 ) → ( ∃ 𝑐 ( 𝑐 ⊆ 𝐴 ∧ 𝑐 ≈ 𝑎 ) ↔ ∃ 𝑐 ( 𝑐 ⊆ 𝐴 ∧ 𝑐 ≈ ( card ‘ 𝐵 ) ) ) )
6 5 rspcva ⊢ ( ( ( card ‘ 𝐵 ) ∈ ω ∧ ∀ 𝑎 ∈ ω ∃ 𝑐 ( 𝑐 ⊆ 𝐴 ∧ 𝑐 ≈ 𝑎 ) ) → ∃ 𝑐 ( 𝑐 ⊆ 𝐴 ∧ 𝑐 ≈ ( card ‘ 𝐵 ) ) )
7 1 2 6 syl2anr ⊢ ( ( ¬ 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ∃ 𝑐 ( 𝑐 ⊆ 𝐴 ∧ 𝑐 ≈ ( card ‘ 𝐵 ) ) )
8 simprr ⊢ ( ( ( ¬ 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( 𝑐 ⊆ 𝐴 ∧ 𝑐 ≈ ( card ‘ 𝐵 ) ) ) → 𝑐 ≈ ( card ‘ 𝐵 ) )
9 ficardid ⊢ ( 𝐵 ∈ Fin → ( card ‘ 𝐵 ) ≈ 𝐵 )
10 9 ad2antlr ⊢ ( ( ( ¬ 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( 𝑐 ⊆ 𝐴 ∧ 𝑐 ≈ ( card ‘ 𝐵 ) ) ) → ( card ‘ 𝐵 ) ≈ 𝐵 )
11 entr ⊢ ( ( 𝑐 ≈ ( card ‘ 𝐵 ) ∧ ( card ‘ 𝐵 ) ≈ 𝐵 ) → 𝑐 ≈ 𝐵 )
12 8 10 11 syl2anc ⊢ ( ( ( ¬ 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( 𝑐 ⊆ 𝐴 ∧ 𝑐 ≈ ( card ‘ 𝐵 ) ) ) → 𝑐 ≈ 𝐵 )
13 12 ensymd ⊢ ( ( ( ¬ 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( 𝑐 ⊆ 𝐴 ∧ 𝑐 ≈ ( card ‘ 𝐵 ) ) ) → 𝐵 ≈ 𝑐 )
14 bren ⊢ ( 𝐵 ≈ 𝑐 ↔ ∃ 𝑓 𝑓 : 𝐵 –1-1-onto→ 𝑐 )
15 13 14 sylib ⊢ ( ( ( ¬ 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( 𝑐 ⊆ 𝐴 ∧ 𝑐 ≈ ( card ‘ 𝐵 ) ) ) → ∃ 𝑓 𝑓 : 𝐵 –1-1-onto→ 𝑐 )
16 f1of1 ⊢ ( 𝑓 : 𝐵 –1-1-onto→ 𝑐 → 𝑓 : 𝐵 –1-1→ 𝑐 )
17 simplrl ⊢ ( ( ( ( ¬ 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( 𝑐 ⊆ 𝐴 ∧ 𝑐 ≈ ( card ‘ 𝐵 ) ) ) ∧ 𝑓 : 𝐵 –1-1-onto→ 𝑐 ) → 𝑐 ⊆ 𝐴 )
18 f1ss ⊢ ( ( 𝑓 : 𝐵 –1-1→ 𝑐 ∧ 𝑐 ⊆ 𝐴 ) → 𝑓 : 𝐵 –1-1→ 𝐴 )
19 16 17 18 syl2an2 ⊢ ( ( ( ( ¬ 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( 𝑐 ⊆ 𝐴 ∧ 𝑐 ≈ ( card ‘ 𝐵 ) ) ) ∧ 𝑓 : 𝐵 –1-1-onto→ 𝑐 ) → 𝑓 : 𝐵 –1-1→ 𝐴 )
20 19 ex ⊢ ( ( ( ¬ 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( 𝑐 ⊆ 𝐴 ∧ 𝑐 ≈ ( card ‘ 𝐵 ) ) ) → ( 𝑓 : 𝐵 –1-1-onto→ 𝑐 → 𝑓 : 𝐵 –1-1→ 𝐴 ) )
21 20 eximdv ⊢ ( ( ( ¬ 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( 𝑐 ⊆ 𝐴 ∧ 𝑐 ≈ ( card ‘ 𝐵 ) ) ) → ( ∃ 𝑓 𝑓 : 𝐵 –1-1-onto→ 𝑐 → ∃ 𝑓 𝑓 : 𝐵 –1-1→ 𝐴 ) )
22 15 21 mpd ⊢ ( ( ( ¬ 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( 𝑐 ⊆ 𝐴 ∧ 𝑐 ≈ ( card ‘ 𝐵 ) ) ) → ∃ 𝑓 𝑓 : 𝐵 –1-1→ 𝐴 )
23 7 22 exlimddv ⊢ ( ( ¬ 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ∃ 𝑓 𝑓 : 𝐵 –1-1→ 𝐴 )