This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 biimtrid ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( suc 𝐴 ≈ suc 𝐵 → 𝐴 ≈ 𝐵 ) )