Metamath Proof Explorer

Theorem phplem4

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)

Ref Expression
Hypotheses phplem2.1 ⊢ 𝐴 ∈ V
phplem2.2 ⊢ 𝐵 ∈ V
Assertion phplem4 ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( suc 𝐴 ≈ suc 𝐵 → 𝐴 ≈ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 phplem2.1 ⊢ 𝐴 ∈ V
2 phplem2.2 ⊢ 𝐵 ∈ V
3 bren ⊢ ( suc 𝐴 ≈ suc 𝐵 ↔ ∃ 𝑓 𝑓 : suc 𝐴 –1-1-onto→ suc 𝐵 )
4 f1of1 ⊢ ( 𝑓 : suc 𝐴 –1-1-onto→ suc 𝐵 → 𝑓 : suc 𝐴 –1-1→ suc 𝐵 )
5 4 adantl ⊢ ( ( 𝐴 ∈ ω ∧ 𝑓 : suc 𝐴 –1-1-onto→ suc 𝐵 ) → 𝑓 : suc 𝐴 –1-1→ suc 𝐵 )
6 2 sucex ⊢ suc 𝐵 ∈ V
7 sssucid ⊢ 𝐴 ⊆ suc 𝐴
8 f1imaen2g ⊢ ( ( ( 𝑓 : suc 𝐴 –1-1→ suc 𝐵 ∧ suc 𝐵 ∈ V ) ∧ ( 𝐴 ⊆ suc 𝐴 ∧ 𝐴 ∈ V ) ) → ( 𝑓 “ 𝐴 ) ≈ 𝐴 )
9 7 1 8 mpanr12 ⊢ ( ( 𝑓 : suc 𝐴 –1-1→ suc 𝐵 ∧ suc 𝐵 ∈ V ) → ( 𝑓 “ 𝐴 ) ≈ 𝐴 )
10 5 6 9 sylancl ⊢ ( ( 𝐴 ∈ ω ∧ 𝑓 : suc 𝐴 –1-1-onto→ suc 𝐵 ) → ( 𝑓 “ 𝐴 ) ≈ 𝐴 )
11 10 ensymd ⊢ ( ( 𝐴 ∈ ω ∧ 𝑓 : suc 𝐴 –1-1-onto→ suc 𝐵 ) → 𝐴 ≈ ( 𝑓 “ 𝐴 ) )
12 nnord ⊢ ( 𝐴 ∈ ω → Ord 𝐴 )
13 orddif ⊢ ( Ord 𝐴 → 𝐴 = ( suc 𝐴 ∖ { 𝐴 } ) )
14 12 13 syl ⊢ ( 𝐴 ∈ ω → 𝐴 = ( suc 𝐴 ∖ { 𝐴 } ) )
15 14 imaeq2d ⊢ ( 𝐴 ∈ ω → ( 𝑓 “ 𝐴 ) = ( 𝑓 “ ( suc 𝐴 ∖ { 𝐴 } ) ) )
16 f1ofn ⊢ ( 𝑓 : suc 𝐴 –1-1-onto→ suc 𝐵 → 𝑓 Fn suc 𝐴 )
17 1 sucid ⊢ 𝐴 ∈ suc 𝐴
18 fnsnfv ⊢ ( ( 𝑓 Fn suc 𝐴 ∧ 𝐴 ∈ suc 𝐴 ) → { ( 𝑓 ‘ 𝐴 ) } = ( 𝑓 “ { 𝐴 } ) )
19 16 17 18 sylancl ⊢ ( 𝑓 : suc 𝐴 –1-1-onto→ suc 𝐵 → { ( 𝑓 ‘ 𝐴 ) } = ( 𝑓 “ { 𝐴 } ) )
20 19 difeq2d ⊢ ( 𝑓 : suc 𝐴 –1-1-onto→ suc 𝐵 → ( ( 𝑓 “ suc 𝐴 ) ∖ { ( 𝑓 ‘ 𝐴 ) } ) = ( ( 𝑓 “ suc 𝐴 ) ∖ ( 𝑓 “ { 𝐴 } ) ) )
21 imadmrn ⊢ ( 𝑓 “ dom 𝑓 ) = ran 𝑓
22 21 eqcomi ⊢ ran 𝑓 = ( 𝑓 “ dom 𝑓 )
23 f1ofo ⊢ ( 𝑓 : suc 𝐴 –1-1-onto→ suc 𝐵 → 𝑓 : suc 𝐴 –onto→ suc 𝐵 )
24 forn ⊢ ( 𝑓 : suc 𝐴 –onto→ suc 𝐵 → ran 𝑓 = suc 𝐵 )
25 23 24 syl ⊢ ( 𝑓 : suc 𝐴 –1-1-onto→ suc 𝐵 → ran 𝑓 = suc 𝐵 )
26 f1odm ⊢ ( 𝑓 : suc 𝐴 –1-1-onto→ suc 𝐵 → dom 𝑓 = suc 𝐴 )
27 26 imaeq2d ⊢ ( 𝑓 : suc 𝐴 –1-1-onto→ suc 𝐵 → ( 𝑓 “ dom 𝑓 ) = ( 𝑓 “ suc 𝐴 ) )
28 22 25 27 3eqtr3a ⊢ ( 𝑓 : suc 𝐴 –1-1-onto→ suc 𝐵 → suc 𝐵 = ( 𝑓 “ suc 𝐴 ) )
29 28 difeq1d ⊢ ( 𝑓 : suc 𝐴 –1-1-onto→ suc 𝐵 → ( suc 𝐵 ∖ { ( 𝑓 ‘ 𝐴 ) } ) = ( ( 𝑓 “ suc 𝐴 ) ∖ { ( 𝑓 ‘ 𝐴 ) } ) )
30 dff1o3 ⊢ ( 𝑓 : suc 𝐴 –1-1-onto→ suc 𝐵 ↔ ( 𝑓 : suc 𝐴 –onto→ suc 𝐵 ∧ Fun ◡ 𝑓 ) )
31 imadif ⊢ ( Fun ◡ 𝑓 → ( 𝑓 “ ( suc 𝐴 ∖ { 𝐴 } ) ) = ( ( 𝑓 “ suc 𝐴 ) ∖ ( 𝑓 “ { 𝐴 } ) ) )
32 30 31 simplbiim ⊢ ( 𝑓 : suc 𝐴 –1-1-onto→ suc 𝐵 → ( 𝑓 “ ( suc 𝐴 ∖ { 𝐴 } ) ) = ( ( 𝑓 “ suc 𝐴 ) ∖ ( 𝑓 “ { 𝐴 } ) ) )
33 20 29 32 3eqtr4rd ⊢ ( 𝑓 : suc 𝐴 –1-1-onto→ suc 𝐵 → ( 𝑓 “ ( suc 𝐴 ∖ { 𝐴 } ) ) = ( suc 𝐵 ∖ { ( 𝑓 ‘ 𝐴 ) } ) )
34 15 33 sylan9eq ⊢ ( ( 𝐴 ∈ ω ∧ 𝑓 : suc 𝐴 –1-1-onto→ suc 𝐵 ) → ( 𝑓 “ 𝐴 ) = ( suc 𝐵 ∖ { ( 𝑓 ‘ 𝐴 ) } ) )
35 11 34 breqtrd ⊢ ( ( 𝐴 ∈ ω ∧ 𝑓 : suc 𝐴 –1-1-onto→ suc 𝐵 ) → 𝐴 ≈ ( suc 𝐵 ∖ { ( 𝑓 ‘ 𝐴 ) } ) )
36 fnfvelrn ⊢ ( ( 𝑓 Fn suc 𝐴 ∧ 𝐴 ∈ suc 𝐴 ) → ( 𝑓 ‘ 𝐴 ) ∈ ran 𝑓 )
37 16 17 36 sylancl ⊢ ( 𝑓 : suc 𝐴 –1-1-onto→ suc 𝐵 → ( 𝑓 ‘ 𝐴 ) ∈ ran 𝑓 )
38 24 eleq2d ⊢ ( 𝑓 : suc 𝐴 –onto→ suc 𝐵 → ( ( 𝑓 ‘ 𝐴 ) ∈ ran 𝑓 ↔ ( 𝑓 ‘ 𝐴 ) ∈ suc 𝐵 ) )
39 23 38 syl ⊢ ( 𝑓 : suc 𝐴 –1-1-onto→ suc 𝐵 → ( ( 𝑓 ‘ 𝐴 ) ∈ ran 𝑓 ↔ ( 𝑓 ‘ 𝐴 ) ∈ suc 𝐵 ) )
40 37 39 mpbid ⊢ ( 𝑓 : suc 𝐴 –1-1-onto→ suc 𝐵 → ( 𝑓 ‘ 𝐴 ) ∈ suc 𝐵 )
41 fvex ⊢ ( 𝑓 ‘ 𝐴 ) ∈ V
42 2 41 phplem3 ⊢ ( ( 𝐵 ∈ ω ∧ ( 𝑓 ‘ 𝐴 ) ∈ suc 𝐵 ) → 𝐵 ≈ ( suc 𝐵 ∖ { ( 𝑓 ‘ 𝐴 ) } ) )
43 40 42 sylan2 ⊢ ( ( 𝐵 ∈ ω ∧ 𝑓 : suc 𝐴 –1-1-onto→ suc 𝐵 ) → 𝐵 ≈ ( suc 𝐵 ∖ { ( 𝑓 ‘ 𝐴 ) } ) )
44 43 ensymd ⊢ ( ( 𝐵 ∈ ω ∧ 𝑓 : suc 𝐴 –1-1-onto→ suc 𝐵 ) → ( suc 𝐵 ∖ { ( 𝑓 ‘ 𝐴 ) } ) ≈ 𝐵 )
45 entr ⊢ ( ( 𝐴 ≈ ( suc 𝐵 ∖ { ( 𝑓 ‘ 𝐴 ) } ) ∧ ( suc 𝐵 ∖ { ( 𝑓 ‘ 𝐴 ) } ) ≈ 𝐵 ) → 𝐴 ≈ 𝐵 )
46 35 44 45 syl2an ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝑓 : suc 𝐴 –1-1-onto→ suc 𝐵 ) ∧ ( 𝐵 ∈ ω ∧ 𝑓 : suc 𝐴 –1-1-onto→ suc 𝐵 ) ) → 𝐴 ≈ 𝐵 )
47 46 anandirs ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝑓 : suc 𝐴 –1-1-onto→ suc 𝐵 ) → 𝐴 ≈ 𝐵 )
48 47 ex ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝑓 : suc 𝐴 –1-1-onto→ suc 𝐵 → 𝐴 ≈ 𝐵 ) )
49 48 exlimdv ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( ∃ 𝑓 𝑓 : suc 𝐴 –1-1-onto→ suc 𝐵 → 𝐴 ≈ 𝐵 ) )
50 3 49 syl5bi ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( suc 𝐴 ≈ suc 𝐵 → 𝐴 ≈ 𝐵 ) )