Metamath Proof Explorer


Theorem phplem2

Description: Lemma for Pigeonhole Principle. Equinumerosity of successors implies equinumerosity of the original natural numbers. (Contributed by NM, 28-May-1998) (Revised by Mario Carneiro, 24-Jun-2015) Avoid ax-pow . (Revised by BTernaryTau, 4-Nov-2024)

Ref Expression
Hypothesis phplem2.1 𝐴 ∈ V
Assertion phplem2 ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( suc 𝐴 ≈ suc 𝐵𝐴𝐵 ) )

Proof

Step Hyp Ref Expression
1 phplem2.1 𝐴 ∈ V
2 bren ( suc 𝐴 ≈ suc 𝐵 ↔ ∃ 𝑓 𝑓 : suc 𝐴1-1-onto→ suc 𝐵 )
3 f1of1 ( 𝑓 : suc 𝐴1-1-onto→ suc 𝐵𝑓 : suc 𝐴1-1→ suc 𝐵 )
4 nnfi ( 𝐴 ∈ ω → 𝐴 ∈ Fin )
5 sssucid 𝐴 ⊆ suc 𝐴
6 f1imaenfi ( ( 𝑓 : suc 𝐴1-1→ suc 𝐵𝐴 ⊆ suc 𝐴𝐴 ∈ Fin ) → ( 𝑓𝐴 ) ≈ 𝐴 )
7 5 6 mp3an2 ( ( 𝑓 : suc 𝐴1-1→ suc 𝐵𝐴 ∈ Fin ) → ( 𝑓𝐴 ) ≈ 𝐴 )
8 3 4 7 syl2anr ( ( 𝐴 ∈ ω ∧ 𝑓 : suc 𝐴1-1-onto→ suc 𝐵 ) → ( 𝑓𝐴 ) ≈ 𝐴 )
9 ensymfib ( 𝐴 ∈ Fin → ( 𝐴 ≈ ( 𝑓𝐴 ) ↔ ( 𝑓𝐴 ) ≈ 𝐴 ) )
10 4 9 syl ( 𝐴 ∈ ω → ( 𝐴 ≈ ( 𝑓𝐴 ) ↔ ( 𝑓𝐴 ) ≈ 𝐴 ) )
11 10 adantr ( ( 𝐴 ∈ ω ∧ 𝑓 : suc 𝐴1-1-onto→ suc 𝐵 ) → ( 𝐴 ≈ ( 𝑓𝐴 ) ↔ ( 𝑓𝐴 ) ≈ 𝐴 ) )
12 8 11 mpbird ( ( 𝐴 ∈ ω ∧ 𝑓 : suc 𝐴1-1-onto→ suc 𝐵 ) → 𝐴 ≈ ( 𝑓𝐴 ) )
13 nnord ( 𝐴 ∈ ω → Ord 𝐴 )
14 orddif ( Ord 𝐴𝐴 = ( suc 𝐴 ∖ { 𝐴 } ) )
15 13 14 syl ( 𝐴 ∈ ω → 𝐴 = ( suc 𝐴 ∖ { 𝐴 } ) )
16 15 imaeq2d ( 𝐴 ∈ ω → ( 𝑓𝐴 ) = ( 𝑓 “ ( suc 𝐴 ∖ { 𝐴 } ) ) )
17 f1ofn ( 𝑓 : suc 𝐴1-1-onto→ suc 𝐵𝑓 Fn suc 𝐴 )
18 1 sucid 𝐴 ∈ suc 𝐴
19 fnsnfv ( ( 𝑓 Fn suc 𝐴𝐴 ∈ suc 𝐴 ) → { ( 𝑓𝐴 ) } = ( 𝑓 “ { 𝐴 } ) )
20 17 18 19 sylancl ( 𝑓 : suc 𝐴1-1-onto→ suc 𝐵 → { ( 𝑓𝐴 ) } = ( 𝑓 “ { 𝐴 } ) )
21 20 difeq2d ( 𝑓 : suc 𝐴1-1-onto→ suc 𝐵 → ( ( 𝑓 “ suc 𝐴 ) ∖ { ( 𝑓𝐴 ) } ) = ( ( 𝑓 “ suc 𝐴 ) ∖ ( 𝑓 “ { 𝐴 } ) ) )
22 imadmrn ( 𝑓 “ dom 𝑓 ) = ran 𝑓
23 22 eqcomi ran 𝑓 = ( 𝑓 “ dom 𝑓 )
24 f1ofo ( 𝑓 : suc 𝐴1-1-onto→ suc 𝐵𝑓 : suc 𝐴onto→ suc 𝐵 )
25 forn ( 𝑓 : suc 𝐴onto→ suc 𝐵 → ran 𝑓 = suc 𝐵 )
26 24 25 syl ( 𝑓 : suc 𝐴1-1-onto→ suc 𝐵 → ran 𝑓 = suc 𝐵 )
27 f1odm ( 𝑓 : suc 𝐴1-1-onto→ suc 𝐵 → dom 𝑓 = suc 𝐴 )
28 27 imaeq2d ( 𝑓 : suc 𝐴1-1-onto→ suc 𝐵 → ( 𝑓 “ dom 𝑓 ) = ( 𝑓 “ suc 𝐴 ) )
29 23 26 28 3eqtr3a ( 𝑓 : suc 𝐴1-1-onto→ suc 𝐵 → suc 𝐵 = ( 𝑓 “ suc 𝐴 ) )
30 29 difeq1d ( 𝑓 : suc 𝐴1-1-onto→ suc 𝐵 → ( suc 𝐵 ∖ { ( 𝑓𝐴 ) } ) = ( ( 𝑓 “ suc 𝐴 ) ∖ { ( 𝑓𝐴 ) } ) )
31 dff1o3 ( 𝑓 : suc 𝐴1-1-onto→ suc 𝐵 ↔ ( 𝑓 : suc 𝐴onto→ suc 𝐵 ∧ Fun 𝑓 ) )
32 imadif ( Fun 𝑓 → ( 𝑓 “ ( suc 𝐴 ∖ { 𝐴 } ) ) = ( ( 𝑓 “ suc 𝐴 ) ∖ ( 𝑓 “ { 𝐴 } ) ) )
33 31 32 simplbiim ( 𝑓 : suc 𝐴1-1-onto→ suc 𝐵 → ( 𝑓 “ ( suc 𝐴 ∖ { 𝐴 } ) ) = ( ( 𝑓 “ suc 𝐴 ) ∖ ( 𝑓 “ { 𝐴 } ) ) )
34 21 30 33 3eqtr4rd ( 𝑓 : suc 𝐴1-1-onto→ suc 𝐵 → ( 𝑓 “ ( suc 𝐴 ∖ { 𝐴 } ) ) = ( suc 𝐵 ∖ { ( 𝑓𝐴 ) } ) )
35 16 34 sylan9eq ( ( 𝐴 ∈ ω ∧ 𝑓 : suc 𝐴1-1-onto→ suc 𝐵 ) → ( 𝑓𝐴 ) = ( suc 𝐵 ∖ { ( 𝑓𝐴 ) } ) )
36 12 35 breqtrd ( ( 𝐴 ∈ ω ∧ 𝑓 : suc 𝐴1-1-onto→ suc 𝐵 ) → 𝐴 ≈ ( suc 𝐵 ∖ { ( 𝑓𝐴 ) } ) )
37 fnfvelrn ( ( 𝑓 Fn suc 𝐴𝐴 ∈ suc 𝐴 ) → ( 𝑓𝐴 ) ∈ ran 𝑓 )
38 17 18 37 sylancl ( 𝑓 : suc 𝐴1-1-onto→ suc 𝐵 → ( 𝑓𝐴 ) ∈ ran 𝑓 )
39 25 eleq2d ( 𝑓 : suc 𝐴onto→ suc 𝐵 → ( ( 𝑓𝐴 ) ∈ ran 𝑓 ↔ ( 𝑓𝐴 ) ∈ suc 𝐵 ) )
40 24 39 syl ( 𝑓 : suc 𝐴1-1-onto→ suc 𝐵 → ( ( 𝑓𝐴 ) ∈ ran 𝑓 ↔ ( 𝑓𝐴 ) ∈ suc 𝐵 ) )
41 38 40 mpbid ( 𝑓 : suc 𝐴1-1-onto→ suc 𝐵 → ( 𝑓𝐴 ) ∈ suc 𝐵 )
42 phplem1 ( ( 𝐵 ∈ ω ∧ ( 𝑓𝐴 ) ∈ suc 𝐵 ) → 𝐵 ≈ ( suc 𝐵 ∖ { ( 𝑓𝐴 ) } ) )
43 41 42 sylan2 ( ( 𝐵 ∈ ω ∧ 𝑓 : suc 𝐴1-1-onto→ suc 𝐵 ) → 𝐵 ≈ ( suc 𝐵 ∖ { ( 𝑓𝐴 ) } ) )
44 nnfi ( 𝐵 ∈ ω → 𝐵 ∈ Fin )
45 ensymfib ( 𝐵 ∈ Fin → ( 𝐵 ≈ ( suc 𝐵 ∖ { ( 𝑓𝐴 ) } ) ↔ ( suc 𝐵 ∖ { ( 𝑓𝐴 ) } ) ≈ 𝐵 ) )
46 44 45 syl ( 𝐵 ∈ ω → ( 𝐵 ≈ ( suc 𝐵 ∖ { ( 𝑓𝐴 ) } ) ↔ ( suc 𝐵 ∖ { ( 𝑓𝐴 ) } ) ≈ 𝐵 ) )
47 46 adantr ( ( 𝐵 ∈ ω ∧ 𝑓 : suc 𝐴1-1-onto→ suc 𝐵 ) → ( 𝐵 ≈ ( suc 𝐵 ∖ { ( 𝑓𝐴 ) } ) ↔ ( suc 𝐵 ∖ { ( 𝑓𝐴 ) } ) ≈ 𝐵 ) )
48 43 47 mpbid ( ( 𝐵 ∈ ω ∧ 𝑓 : suc 𝐴1-1-onto→ suc 𝐵 ) → ( suc 𝐵 ∖ { ( 𝑓𝐴 ) } ) ≈ 𝐵 )
49 entrfil ( ( 𝐴 ∈ Fin ∧ 𝐴 ≈ ( suc 𝐵 ∖ { ( 𝑓𝐴 ) } ) ∧ ( suc 𝐵 ∖ { ( 𝑓𝐴 ) } ) ≈ 𝐵 ) → 𝐴𝐵 )
50 4 49 syl3an1 ( ( 𝐴 ∈ ω ∧ 𝐴 ≈ ( suc 𝐵 ∖ { ( 𝑓𝐴 ) } ) ∧ ( suc 𝐵 ∖ { ( 𝑓𝐴 ) } ) ≈ 𝐵 ) → 𝐴𝐵 )
51 48 50 syl3an3 ( ( 𝐴 ∈ ω ∧ 𝐴 ≈ ( suc 𝐵 ∖ { ( 𝑓𝐴 ) } ) ∧ ( 𝐵 ∈ ω ∧ 𝑓 : suc 𝐴1-1-onto→ suc 𝐵 ) ) → 𝐴𝐵 )
52 51 3expa ( ( ( 𝐴 ∈ ω ∧ 𝐴 ≈ ( suc 𝐵 ∖ { ( 𝑓𝐴 ) } ) ) ∧ ( 𝐵 ∈ ω ∧ 𝑓 : suc 𝐴1-1-onto→ suc 𝐵 ) ) → 𝐴𝐵 )
53 36 52 syldanl ( ( ( 𝐴 ∈ ω ∧ 𝑓 : suc 𝐴1-1-onto→ suc 𝐵 ) ∧ ( 𝐵 ∈ ω ∧ 𝑓 : suc 𝐴1-1-onto→ suc 𝐵 ) ) → 𝐴𝐵 )
54 53 anandirs ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝑓 : suc 𝐴1-1-onto→ suc 𝐵 ) → 𝐴𝐵 )
55 54 ex ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝑓 : suc 𝐴1-1-onto→ suc 𝐵𝐴𝐵 ) )
56 55 exlimdv ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( ∃ 𝑓 𝑓 : suc 𝐴1-1-onto→ suc 𝐵𝐴𝐵 ) )
57 2 56 syl5bi ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( suc 𝐴 ≈ suc 𝐵𝐴𝐵 ) )