MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  f1opwfi Structured version   Visualization version   GIF version

Theorem f1opwfi 8980
Description: A one-to-one mapping induces a one-to-one mapping on finite subsets. (Contributed by Mario Carneiro, 25-Jan-2015.)
Assertion
Ref Expression
f1opwfi (𝐹:𝐴1-1-onto𝐵 → (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐹𝑏)):(𝒫 𝐴 ∩ Fin)–1-1-onto→(𝒫 𝐵 ∩ Fin))
Distinct variable groups:   𝐴,𝑏   𝐵,𝑏   𝐹,𝑏

Proof of Theorem f1opwfi
Dummy variable 𝑎 is distinct from all other variables.
StepHypRef Expression
1 eqid 2737 . 2 (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐹𝑏)) = (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐹𝑏))
2 simpr 488 . . . . . 6 ((𝐹:𝐴1-1-onto𝐵𝑏 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑏 ∈ (𝒫 𝐴 ∩ Fin))
32elin2d 4113 . . . . 5 ((𝐹:𝐴1-1-onto𝐵𝑏 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑏 ∈ Fin)
4 f1ofun 6663 . . . . . 6 (𝐹:𝐴1-1-onto𝐵 → Fun 𝐹)
5 elinel1 4109 . . . . . . . . 9 (𝑏 ∈ (𝒫 𝐴 ∩ Fin) → 𝑏 ∈ 𝒫 𝐴)
6 elpwi 4522 . . . . . . . . 9 (𝑏 ∈ 𝒫 𝐴𝑏𝐴)
75, 6syl 17 . . . . . . . 8 (𝑏 ∈ (𝒫 𝐴 ∩ Fin) → 𝑏𝐴)
87adantl 485 . . . . . . 7 ((𝐹:𝐴1-1-onto𝐵𝑏 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑏𝐴)
9 f1odm 6665 . . . . . . . 8 (𝐹:𝐴1-1-onto𝐵 → dom 𝐹 = 𝐴)
109adantr 484 . . . . . . 7 ((𝐹:𝐴1-1-onto𝐵𝑏 ∈ (𝒫 𝐴 ∩ Fin)) → dom 𝐹 = 𝐴)
118, 10sseqtrrd 3942 . . . . . 6 ((𝐹:𝐴1-1-onto𝐵𝑏 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑏 ⊆ dom 𝐹)
12 fores 6643 . . . . . 6 ((Fun 𝐹𝑏 ⊆ dom 𝐹) → (𝐹𝑏):𝑏onto→(𝐹𝑏))
134, 11, 12syl2an2r 685 . . . . 5 ((𝐹:𝐴1-1-onto𝐵𝑏 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹𝑏):𝑏onto→(𝐹𝑏))
14 fofi 8962 . . . . 5 ((𝑏 ∈ Fin ∧ (𝐹𝑏):𝑏onto→(𝐹𝑏)) → (𝐹𝑏) ∈ Fin)
153, 13, 14syl2anc 587 . . . 4 ((𝐹:𝐴1-1-onto𝐵𝑏 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹𝑏) ∈ Fin)
16 imassrn 5940 . . . . . 6 (𝐹𝑏) ⊆ ran 𝐹
17 f1ofo 6668 . . . . . . 7 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴onto𝐵)
18 forn 6636 . . . . . . 7 (𝐹:𝐴onto𝐵 → ran 𝐹 = 𝐵)
1917, 18syl 17 . . . . . 6 (𝐹:𝐴1-1-onto𝐵 → ran 𝐹 = 𝐵)
2016, 19sseqtrid 3953 . . . . 5 (𝐹:𝐴1-1-onto𝐵 → (𝐹𝑏) ⊆ 𝐵)
2120adantr 484 . . . 4 ((𝐹:𝐴1-1-onto𝐵𝑏 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹𝑏) ⊆ 𝐵)
2215, 21elpwd 4521 . . 3 ((𝐹:𝐴1-1-onto𝐵𝑏 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹𝑏) ∈ 𝒫 𝐵)
2322, 15elind 4108 . 2 ((𝐹:𝐴1-1-onto𝐵𝑏 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹𝑏) ∈ (𝒫 𝐵 ∩ Fin))
24 simpr 488 . . . . . 6 ((𝐹:𝐴1-1-onto𝐵𝑎 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑎 ∈ (𝒫 𝐵 ∩ Fin))
2524elin2d 4113 . . . . 5 ((𝐹:𝐴1-1-onto𝐵𝑎 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑎 ∈ Fin)
26 dff1o3 6667 . . . . . . 7 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴onto𝐵 ∧ Fun 𝐹))
2726simprbi 500 . . . . . 6 (𝐹:𝐴1-1-onto𝐵 → Fun 𝐹)
28 elinel1 4109 . . . . . . . . 9 (𝑎 ∈ (𝒫 𝐵 ∩ Fin) → 𝑎 ∈ 𝒫 𝐵)
2928adantl 485 . . . . . . . 8 ((𝐹:𝐴1-1-onto𝐵𝑎 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑎 ∈ 𝒫 𝐵)
30 elpwi 4522 . . . . . . . 8 (𝑎 ∈ 𝒫 𝐵𝑎𝐵)
3129, 30syl 17 . . . . . . 7 ((𝐹:𝐴1-1-onto𝐵𝑎 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑎𝐵)
32 f1ocnv 6673 . . . . . . . . 9 (𝐹:𝐴1-1-onto𝐵𝐹:𝐵1-1-onto𝐴)
3332adantr 484 . . . . . . . 8 ((𝐹:𝐴1-1-onto𝐵𝑎 ∈ (𝒫 𝐵 ∩ Fin)) → 𝐹:𝐵1-1-onto𝐴)
34 f1odm 6665 . . . . . . . 8 (𝐹:𝐵1-1-onto𝐴 → dom 𝐹 = 𝐵)
3533, 34syl 17 . . . . . . 7 ((𝐹:𝐴1-1-onto𝐵𝑎 ∈ (𝒫 𝐵 ∩ Fin)) → dom 𝐹 = 𝐵)
3631, 35sseqtrrd 3942 . . . . . 6 ((𝐹:𝐴1-1-onto𝐵𝑎 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑎 ⊆ dom 𝐹)
37 fores 6643 . . . . . 6 ((Fun 𝐹𝑎 ⊆ dom 𝐹) → (𝐹𝑎):𝑎onto→(𝐹𝑎))
3827, 36, 37syl2an2r 685 . . . . 5 ((𝐹:𝐴1-1-onto𝐵𝑎 ∈ (𝒫 𝐵 ∩ Fin)) → (𝐹𝑎):𝑎onto→(𝐹𝑎))
39 fofi 8962 . . . . 5 ((𝑎 ∈ Fin ∧ (𝐹𝑎):𝑎onto→(𝐹𝑎)) → (𝐹𝑎) ∈ Fin)
4025, 38, 39syl2anc 587 . . . 4 ((𝐹:𝐴1-1-onto𝐵𝑎 ∈ (𝒫 𝐵 ∩ Fin)) → (𝐹𝑎) ∈ Fin)
41 imassrn 5940 . . . . . 6 (𝐹𝑎) ⊆ ran 𝐹
42 dfdm4 5764 . . . . . . 7 dom 𝐹 = ran 𝐹
4342, 9eqtr3id 2792 . . . . . 6 (𝐹:𝐴1-1-onto𝐵 → ran 𝐹 = 𝐴)
4441, 43sseqtrid 3953 . . . . 5 (𝐹:𝐴1-1-onto𝐵 → (𝐹𝑎) ⊆ 𝐴)
4544adantr 484 . . . 4 ((𝐹:𝐴1-1-onto𝐵𝑎 ∈ (𝒫 𝐵 ∩ Fin)) → (𝐹𝑎) ⊆ 𝐴)
4640, 45elpwd 4521 . . 3 ((𝐹:𝐴1-1-onto𝐵𝑎 ∈ (𝒫 𝐵 ∩ Fin)) → (𝐹𝑎) ∈ 𝒫 𝐴)
4746, 40elind 4108 . 2 ((𝐹:𝐴1-1-onto𝐵𝑎 ∈ (𝒫 𝐵 ∩ Fin)) → (𝐹𝑎) ∈ (𝒫 𝐴 ∩ Fin))
485, 28anim12i 616 . . 3 ((𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑎 ∈ (𝒫 𝐵 ∩ Fin)) → (𝑏 ∈ 𝒫 𝐴𝑎 ∈ 𝒫 𝐵))
4930adantl 485 . . . . . . 7 ((𝑏 ∈ 𝒫 𝐴𝑎 ∈ 𝒫 𝐵) → 𝑎𝐵)
50 foimacnv 6678 . . . . . . 7 ((𝐹:𝐴onto𝐵𝑎𝐵) → (𝐹 “ (𝐹𝑎)) = 𝑎)
5117, 49, 50syl2an 599 . . . . . 6 ((𝐹:𝐴1-1-onto𝐵 ∧ (𝑏 ∈ 𝒫 𝐴𝑎 ∈ 𝒫 𝐵)) → (𝐹 “ (𝐹𝑎)) = 𝑎)
5251eqcomd 2743 . . . . 5 ((𝐹:𝐴1-1-onto𝐵 ∧ (𝑏 ∈ 𝒫 𝐴𝑎 ∈ 𝒫 𝐵)) → 𝑎 = (𝐹 “ (𝐹𝑎)))
53 imaeq2 5925 . . . . . 6 (𝑏 = (𝐹𝑎) → (𝐹𝑏) = (𝐹 “ (𝐹𝑎)))
5453eqeq2d 2748 . . . . 5 (𝑏 = (𝐹𝑎) → (𝑎 = (𝐹𝑏) ↔ 𝑎 = (𝐹 “ (𝐹𝑎))))
5552, 54syl5ibrcom 250 . . . 4 ((𝐹:𝐴1-1-onto𝐵 ∧ (𝑏 ∈ 𝒫 𝐴𝑎 ∈ 𝒫 𝐵)) → (𝑏 = (𝐹𝑎) → 𝑎 = (𝐹𝑏)))
56 f1of1 6660 . . . . . . 7 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴1-1𝐵)
576adantr 484 . . . . . . 7 ((𝑏 ∈ 𝒫 𝐴𝑎 ∈ 𝒫 𝐵) → 𝑏𝐴)
58 f1imacnv 6677 . . . . . . 7 ((𝐹:𝐴1-1𝐵𝑏𝐴) → (𝐹 “ (𝐹𝑏)) = 𝑏)
5956, 57, 58syl2an 599 . . . . . 6 ((𝐹:𝐴1-1-onto𝐵 ∧ (𝑏 ∈ 𝒫 𝐴𝑎 ∈ 𝒫 𝐵)) → (𝐹 “ (𝐹𝑏)) = 𝑏)
6059eqcomd 2743 . . . . 5 ((𝐹:𝐴1-1-onto𝐵 ∧ (𝑏 ∈ 𝒫 𝐴𝑎 ∈ 𝒫 𝐵)) → 𝑏 = (𝐹 “ (𝐹𝑏)))
61 imaeq2 5925 . . . . . 6 (𝑎 = (𝐹𝑏) → (𝐹𝑎) = (𝐹 “ (𝐹𝑏)))
6261eqeq2d 2748 . . . . 5 (𝑎 = (𝐹𝑏) → (𝑏 = (𝐹𝑎) ↔ 𝑏 = (𝐹 “ (𝐹𝑏))))
6360, 62syl5ibrcom 250 . . . 4 ((𝐹:𝐴1-1-onto𝐵 ∧ (𝑏 ∈ 𝒫 𝐴𝑎 ∈ 𝒫 𝐵)) → (𝑎 = (𝐹𝑏) → 𝑏 = (𝐹𝑎)))
6455, 63impbid 215 . . 3 ((𝐹:𝐴1-1-onto𝐵 ∧ (𝑏 ∈ 𝒫 𝐴𝑎 ∈ 𝒫 𝐵)) → (𝑏 = (𝐹𝑎) ↔ 𝑎 = (𝐹𝑏)))
6548, 64sylan2 596 . 2 ((𝐹:𝐴1-1-onto𝐵 ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑎 ∈ (𝒫 𝐵 ∩ Fin))) → (𝑏 = (𝐹𝑎) ↔ 𝑎 = (𝐹𝑏)))
661, 23, 47, 65f1o2d 7459 1 (𝐹:𝐴1-1-onto𝐵 → (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐹𝑏)):(𝒫 𝐴 ∩ Fin)–1-1-onto→(𝒫 𝐵 ∩ Fin))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1543  wcel 2110  cin 3865  wss 3866  𝒫 cpw 4513  cmpt 5135  ccnv 5550  dom cdm 5551  ran crn 5552  cres 5553  cima 5554  Fun wfun 6374  1-1wf1 6377  ontowfo 6378  1-1-ontowf1o 6379  Fincfn 8626
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3410  df-sbc 3695  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-pss 3885  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-tp 4546  df-op 4548  df-uni 4820  df-br 5054  df-opab 5116  df-mpt 5136  df-tr 5162  df-id 5455  df-eprel 5460  df-po 5468  df-so 5469  df-fr 5509  df-we 5511  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-ord 6216  df-on 6217  df-lim 6218  df-suc 6219  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-fv 6388  df-om 7645  df-1o 8202  df-er 8391  df-en 8627  df-dom 8628  df-fin 8630
This theorem is referenced by:  fictb  9859  ackbijnn  15392  tsmsf1o  23042  eulerpartgbij  32051
  Copyright terms: Public domain W3C validator