Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  phplem4 GIF version

Theorem phplem4 6758
 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.)
Hypotheses
Ref Expression
phplem2.1 𝐴 ∈ V
phplem2.2 𝐵 ∈ V
Assertion
Ref Expression
phplem4 ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (suc 𝐴 ≈ suc 𝐵𝐴𝐵))

Proof of Theorem phplem4
Dummy variable 𝑓 is distinct from all other variables.
StepHypRef Expression
1 bren 6650 . 2 (suc 𝐴 ≈ suc 𝐵 ↔ ∃𝑓 𝑓:suc 𝐴1-1-onto→suc 𝐵)
2 f1of1 5375 . . . . . . . . . 10 (𝑓:suc 𝐴1-1-onto→suc 𝐵𝑓:suc 𝐴1-1→suc 𝐵)
32adantl 275 . . . . . . . . 9 ((𝐴 ∈ ω ∧ 𝑓:suc 𝐴1-1-onto→suc 𝐵) → 𝑓:suc 𝐴1-1→suc 𝐵)
4 phplem2.2 . . . . . . . . . 10 𝐵 ∈ V
54sucex 4424 . . . . . . . . 9 suc 𝐵 ∈ V
6 sssucid 4346 . . . . . . . . . 10 𝐴 ⊆ suc 𝐴
7 phplem2.1 . . . . . . . . . 10 𝐴 ∈ V
8 f1imaen2g 6696 . . . . . . . . . 10 (((𝑓:suc 𝐴1-1→suc 𝐵 ∧ suc 𝐵 ∈ V) ∧ (𝐴 ⊆ suc 𝐴𝐴 ∈ V)) → (𝑓𝐴) ≈ 𝐴)
96, 7, 8mpanr12 436 . . . . . . . . 9 ((𝑓:suc 𝐴1-1→suc 𝐵 ∧ suc 𝐵 ∈ V) → (𝑓𝐴) ≈ 𝐴)
103, 5, 9sylancl 410 . . . . . . . 8 ((𝐴 ∈ ω ∧ 𝑓:suc 𝐴1-1-onto→suc 𝐵) → (𝑓𝐴) ≈ 𝐴)
1110ensymd 6686 . . . . . . 7 ((𝐴 ∈ ω ∧ 𝑓:suc 𝐴1-1-onto→suc 𝐵) → 𝐴 ≈ (𝑓𝐴))
12 nnord 4534 . . . . . . . . . 10 (𝐴 ∈ ω → Ord 𝐴)
13 orddif 4471 . . . . . . . . . 10 (Ord 𝐴𝐴 = (suc 𝐴 ∖ {𝐴}))
1412, 13syl 14 . . . . . . . . 9 (𝐴 ∈ ω → 𝐴 = (suc 𝐴 ∖ {𝐴}))
1514imaeq2d 4890 . . . . . . . 8 (𝐴 ∈ ω → (𝑓𝐴) = (𝑓 “ (suc 𝐴 ∖ {𝐴})))
16 f1ofn 5377 . . . . . . . . . . 11 (𝑓:suc 𝐴1-1-onto→suc 𝐵𝑓 Fn suc 𝐴)
177sucid 4348 . . . . . . . . . . 11 𝐴 ∈ suc 𝐴
18 fnsnfv 5489 . . . . . . . . . . 11 ((𝑓 Fn suc 𝐴𝐴 ∈ suc 𝐴) → {(𝑓𝐴)} = (𝑓 “ {𝐴}))
1916, 17, 18sylancl 410 . . . . . . . . . 10 (𝑓:suc 𝐴1-1-onto→suc 𝐵 → {(𝑓𝐴)} = (𝑓 “ {𝐴}))
2019difeq2d 3200 . . . . . . . . 9 (𝑓:suc 𝐴1-1-onto→suc 𝐵 → ((𝑓 “ suc 𝐴) ∖ {(𝑓𝐴)}) = ((𝑓 “ suc 𝐴) ∖ (𝑓 “ {𝐴})))
21 imadmrn 4900 . . . . . . . . . . . 12 (𝑓 “ dom 𝑓) = ran 𝑓
2221eqcomi 2144 . . . . . . . . . . 11 ran 𝑓 = (𝑓 “ dom 𝑓)
23 f1ofo 5383 . . . . . . . . . . . 12 (𝑓:suc 𝐴1-1-onto→suc 𝐵𝑓:suc 𝐴onto→suc 𝐵)
24 forn 5357 . . . . . . . . . . . 12 (𝑓:suc 𝐴onto→suc 𝐵 → ran 𝑓 = suc 𝐵)
2523, 24syl 14 . . . . . . . . . . 11 (𝑓:suc 𝐴1-1-onto→suc 𝐵 → ran 𝑓 = suc 𝐵)
26 f1odm 5380 . . . . . . . . . . . 12 (𝑓:suc 𝐴1-1-onto→suc 𝐵 → dom 𝑓 = suc 𝐴)
2726imaeq2d 4890 . . . . . . . . . . 11 (𝑓:suc 𝐴1-1-onto→suc 𝐵 → (𝑓 “ dom 𝑓) = (𝑓 “ suc 𝐴))
2822, 25, 273eqtr3a 2197 . . . . . . . . . 10 (𝑓:suc 𝐴1-1-onto→suc 𝐵 → suc 𝐵 = (𝑓 “ suc 𝐴))
2928difeq1d 3199 . . . . . . . . 9 (𝑓:suc 𝐴1-1-onto→suc 𝐵 → (suc 𝐵 ∖ {(𝑓𝐴)}) = ((𝑓 “ suc 𝐴) ∖ {(𝑓𝐴)}))
30 dff1o3 5382 . . . . . . . . . . 11 (𝑓:suc 𝐴1-1-onto→suc 𝐵 ↔ (𝑓:suc 𝐴onto→suc 𝐵 ∧ Fun 𝑓))
3130simprbi 273 . . . . . . . . . 10 (𝑓:suc 𝐴1-1-onto→suc 𝐵 → Fun 𝑓)
32 imadif 5212 . . . . . . . . . 10 (Fun 𝑓 → (𝑓 “ (suc 𝐴 ∖ {𝐴})) = ((𝑓 “ suc 𝐴) ∖ (𝑓 “ {𝐴})))
3331, 32syl 14 . . . . . . . . 9 (𝑓:suc 𝐴1-1-onto→suc 𝐵 → (𝑓 “ (suc 𝐴 ∖ {𝐴})) = ((𝑓 “ suc 𝐴) ∖ (𝑓 “ {𝐴})))
3420, 29, 333eqtr4rd 2184 . . . . . . . 8 (𝑓:suc 𝐴1-1-onto→suc 𝐵 → (𝑓 “ (suc 𝐴 ∖ {𝐴})) = (suc 𝐵 ∖ {(𝑓𝐴)}))
3515, 34sylan9eq 2193 . . . . . . 7 ((𝐴 ∈ ω ∧ 𝑓:suc 𝐴1-1-onto→suc 𝐵) → (𝑓𝐴) = (suc 𝐵 ∖ {(𝑓𝐴)}))
3611, 35breqtrd 3963 . . . . . 6 ((𝐴 ∈ ω ∧ 𝑓:suc 𝐴1-1-onto→suc 𝐵) → 𝐴 ≈ (suc 𝐵 ∖ {(𝑓𝐴)}))
37 fnfvelrn 5561 . . . . . . . . . 10 ((𝑓 Fn suc 𝐴𝐴 ∈ suc 𝐴) → (𝑓𝐴) ∈ ran 𝑓)
3816, 17, 37sylancl 410 . . . . . . . . 9 (𝑓:suc 𝐴1-1-onto→suc 𝐵 → (𝑓𝐴) ∈ ran 𝑓)
3924eleq2d 2210 . . . . . . . . . 10 (𝑓:suc 𝐴onto→suc 𝐵 → ((𝑓𝐴) ∈ ran 𝑓 ↔ (𝑓𝐴) ∈ suc 𝐵))
4023, 39syl 14 . . . . . . . . 9 (𝑓:suc 𝐴1-1-onto→suc 𝐵 → ((𝑓𝐴) ∈ ran 𝑓 ↔ (𝑓𝐴) ∈ suc 𝐵))
4138, 40mpbid 146 . . . . . . . 8 (𝑓:suc 𝐴1-1-onto→suc 𝐵 → (𝑓𝐴) ∈ suc 𝐵)
42 vex 2693 . . . . . . . . . 10 𝑓 ∈ V
4342, 7fvex 5450 . . . . . . . . 9 (𝑓𝐴) ∈ V
444, 43phplem3 6757 . . . . . . . 8 ((𝐵 ∈ ω ∧ (𝑓𝐴) ∈ suc 𝐵) → 𝐵 ≈ (suc 𝐵 ∖ {(𝑓𝐴)}))
4541, 44sylan2 284 . . . . . . 7 ((𝐵 ∈ ω ∧ 𝑓:suc 𝐴1-1-onto→suc 𝐵) → 𝐵 ≈ (suc 𝐵 ∖ {(𝑓𝐴)}))
4645ensymd 6686 . . . . . 6 ((𝐵 ∈ ω ∧ 𝑓:suc 𝐴1-1-onto→suc 𝐵) → (suc 𝐵 ∖ {(𝑓𝐴)}) ≈ 𝐵)
47 entr 6687 . . . . . 6 ((𝐴 ≈ (suc 𝐵 ∖ {(𝑓𝐴)}) ∧ (suc 𝐵 ∖ {(𝑓𝐴)}) ≈ 𝐵) → 𝐴𝐵)
4836, 46, 47syl2an 287 . . . . 5 (((𝐴 ∈ ω ∧ 𝑓:suc 𝐴1-1-onto→suc 𝐵) ∧ (𝐵 ∈ ω ∧ 𝑓:suc 𝐴1-1-onto→suc 𝐵)) → 𝐴𝐵)
4948anandirs 583 . . . 4 (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝑓:suc 𝐴1-1-onto→suc 𝐵) → 𝐴𝐵)
5049ex 114 . . 3 ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝑓:suc 𝐴1-1-onto→suc 𝐵𝐴𝐵))
5150exlimdv 1792 . 2 ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (∃𝑓 𝑓:suc 𝐴1-1-onto→suc 𝐵𝐴𝐵))
521, 51syl5bi 151 1 ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (suc 𝐴 ≈ suc 𝐵𝐴𝐵))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   = wceq 1332  ∃wex 1469   ∈ wcel 1481  Vcvv 2690   ∖ cdif 3074   ⊆ wss 3077  {csn 3533   class class class wbr 3938  Ord word 4293  suc csuc 4296  ωcom 4513  ◡ccnv 4547  dom cdm 4548  ran crn 4549   “ cima 4551  Fun wfun 5126   Fn wfn 5127  –1-1→wf1 5129  –onto→wfo 5130  –1-1-onto→wf1o 5131  ‘cfv 5132   ≈ cen 6641 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4055  ax-nul 4063  ax-pow 4107  ax-pr 4140  ax-un 4364  ax-setind 4461  ax-iinf 4511 This theorem depends on definitions:  df-bi 116  df-dc 821  df-3or 964  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-ral 2422  df-rex 2423  df-rab 2426  df-v 2692  df-sbc 2915  df-dif 3079  df-un 3081  df-in 3083  df-ss 3090  df-nul 3370  df-pw 3518  df-sn 3539  df-pr 3540  df-op 3542  df-uni 3746  df-int 3781  df-br 3939  df-opab 3999  df-tr 4036  df-id 4224  df-iord 4297  df-on 4299  df-suc 4302  df-iom 4514  df-xp 4554  df-rel 4555  df-cnv 4556  df-co 4557  df-dm 4558  df-rn 4559  df-res 4560  df-ima 4561  df-iota 5097  df-fun 5134  df-fn 5135  df-f 5136  df-f1 5137  df-fo 5138  df-f1o 5139  df-fv 5140  df-er 6438  df-en 6644 This theorem is referenced by:  nneneq  6760  php5  6761
 Copyright terms: Public domain W3C validator