Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fpwrelmapffs Structured version   Visualization version   GIF version

Theorem fpwrelmapffs 30594
 Description: Define a canonical mapping between finite relations (finite subsets of a cartesian product) and functions with finite support into finite subsets. (Contributed by Thierry Arnoux, 28-Aug-2017.) (Revised by Thierry Arnoux, 1-Sep-2019.)
Hypotheses
Ref Expression
fpwrelmap.1 𝐴 ∈ V
fpwrelmap.2 𝐵 ∈ V
fpwrelmap.3 𝑀 = (𝑓 ∈ (𝒫 𝐵m 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))})
fpwrelmapffs.1 𝑆 = {𝑓 ∈ ((𝒫 𝐵 ∩ Fin) ↑m 𝐴) ∣ (𝑓 supp ∅) ∈ Fin}
Assertion
Ref Expression
fpwrelmapffs (𝑀𝑆):𝑆1-1-onto→(𝒫 (𝐴 × 𝐵) ∩ Fin)
Distinct variable groups:   𝑥,𝑓,𝑦,𝐴   𝐵,𝑓,𝑥,𝑦
Allowed substitution hints:   𝑆(𝑥,𝑦,𝑓)   𝑀(𝑥,𝑦,𝑓)

Proof of Theorem fpwrelmapffs
Dummy variable 𝑟 is distinct from all other variables.
StepHypRef Expression
1 fpwrelmap.3 . . . 4 𝑀 = (𝑓 ∈ (𝒫 𝐵m 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))})
2 fpwrelmap.1 . . . . . 6 𝐴 ∈ V
3 fpwrelmap.2 . . . . . 6 𝐵 ∈ V
42, 3, 1fpwrelmap 30593 . . . . 5 𝑀:(𝒫 𝐵m 𝐴)–1-1-onto→𝒫 (𝐴 × 𝐵)
54a1i 11 . . . 4 (⊤ → 𝑀:(𝒫 𝐵m 𝐴)–1-1-onto→𝒫 (𝐴 × 𝐵))
6 simpl 487 . . . . . . 7 ((𝑓 ∈ (𝒫 𝐵m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) → 𝑓 ∈ (𝒫 𝐵m 𝐴))
73pwex 5250 . . . . . . . 8 𝒫 𝐵 ∈ V
87, 2elmap 8454 . . . . . . 7 (𝑓 ∈ (𝒫 𝐵m 𝐴) ↔ 𝑓:𝐴⟶𝒫 𝐵)
96, 8sylib 221 . . . . . 6 ((𝑓 ∈ (𝒫 𝐵m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) → 𝑓:𝐴⟶𝒫 𝐵)
10 simpr 489 . . . . . 6 ((𝑓 ∈ (𝒫 𝐵m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) → 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))})
112, 3, 9, 10fpwrelmapffslem 30592 . . . . 5 ((𝑓 ∈ (𝒫 𝐵m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) → (𝑟 ∈ Fin ↔ (ran 𝑓 ⊆ Fin ∧ (𝑓 supp ∅) ∈ Fin)))
12113adant1 1128 . . . 4 ((⊤ ∧ 𝑓 ∈ (𝒫 𝐵m 𝐴) ∧ 𝑟 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 ∈ (𝑓𝑥))}) → (𝑟 ∈ Fin ↔ (ran 𝑓 ⊆ Fin ∧ (𝑓 supp ∅) ∈ Fin)))
131, 5, 12f1oresrab 6881 . . 3 (⊤ → (𝑀 ↾ {𝑓 ∈ (𝒫 𝐵m 𝐴) ∣ (ran 𝑓 ⊆ Fin ∧ (𝑓 supp ∅) ∈ Fin)}):{𝑓 ∈ (𝒫 𝐵m 𝐴) ∣ (ran 𝑓 ⊆ Fin ∧ (𝑓 supp ∅) ∈ Fin)}–1-1-onto→{𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∣ 𝑟 ∈ Fin})
1413mptru 1546 . 2 (𝑀 ↾ {𝑓 ∈ (𝒫 𝐵m 𝐴) ∣ (ran 𝑓 ⊆ Fin ∧ (𝑓 supp ∅) ∈ Fin)}):{𝑓 ∈ (𝒫 𝐵m 𝐴) ∣ (ran 𝑓 ⊆ Fin ∧ (𝑓 supp ∅) ∈ Fin)}–1-1-onto→{𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∣ 𝑟 ∈ Fin}
15 fpwrelmapffs.1 . . . . 5 𝑆 = {𝑓 ∈ ((𝒫 𝐵 ∩ Fin) ↑m 𝐴) ∣ (𝑓 supp ∅) ∈ Fin}
162, 7maprnin 30591 . . . . . 6 ((𝒫 𝐵 ∩ Fin) ↑m 𝐴) = {𝑓 ∈ (𝒫 𝐵m 𝐴) ∣ ran 𝑓 ⊆ Fin}
17 nfcv 2920 . . . . . . 7 𝑓((𝒫 𝐵 ∩ Fin) ↑m 𝐴)
18 nfrab1 3303 . . . . . . 7 𝑓{𝑓 ∈ (𝒫 𝐵m 𝐴) ∣ ran 𝑓 ⊆ Fin}
1917, 18rabeqf 3394 . . . . . 6 (((𝒫 𝐵 ∩ Fin) ↑m 𝐴) = {𝑓 ∈ (𝒫 𝐵m 𝐴) ∣ ran 𝑓 ⊆ Fin} → {𝑓 ∈ ((𝒫 𝐵 ∩ Fin) ↑m 𝐴) ∣ (𝑓 supp ∅) ∈ Fin} = {𝑓 ∈ {𝑓 ∈ (𝒫 𝐵m 𝐴) ∣ ran 𝑓 ⊆ Fin} ∣ (𝑓 supp ∅) ∈ Fin})
2016, 19ax-mp 5 . . . . 5 {𝑓 ∈ ((𝒫 𝐵 ∩ Fin) ↑m 𝐴) ∣ (𝑓 supp ∅) ∈ Fin} = {𝑓 ∈ {𝑓 ∈ (𝒫 𝐵m 𝐴) ∣ ran 𝑓 ⊆ Fin} ∣ (𝑓 supp ∅) ∈ Fin}
21 rabrab 3298 . . . . 5 {𝑓 ∈ {𝑓 ∈ (𝒫 𝐵m 𝐴) ∣ ran 𝑓 ⊆ Fin} ∣ (𝑓 supp ∅) ∈ Fin} = {𝑓 ∈ (𝒫 𝐵m 𝐴) ∣ (ran 𝑓 ⊆ Fin ∧ (𝑓 supp ∅) ∈ Fin)}
2215, 20, 213eqtri 2786 . . . 4 𝑆 = {𝑓 ∈ (𝒫 𝐵m 𝐴) ∣ (ran 𝑓 ⊆ Fin ∧ (𝑓 supp ∅) ∈ Fin)}
23 dfin5 3867 . . . 4 (𝒫 (𝐴 × 𝐵) ∩ Fin) = {𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∣ 𝑟 ∈ Fin}
24 f1oeq23 6594 . . . 4 ((𝑆 = {𝑓 ∈ (𝒫 𝐵m 𝐴) ∣ (ran 𝑓 ⊆ Fin ∧ (𝑓 supp ∅) ∈ Fin)} ∧ (𝒫 (𝐴 × 𝐵) ∩ Fin) = {𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∣ 𝑟 ∈ Fin}) → ((𝑀𝑆):𝑆1-1-onto→(𝒫 (𝐴 × 𝐵) ∩ Fin) ↔ (𝑀𝑆):{𝑓 ∈ (𝒫 𝐵m 𝐴) ∣ (ran 𝑓 ⊆ Fin ∧ (𝑓 supp ∅) ∈ Fin)}–1-1-onto→{𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∣ 𝑟 ∈ Fin}))
2522, 23, 24mp2an 692 . . 3 ((𝑀𝑆):𝑆1-1-onto→(𝒫 (𝐴 × 𝐵) ∩ Fin) ↔ (𝑀𝑆):{𝑓 ∈ (𝒫 𝐵m 𝐴) ∣ (ran 𝑓 ⊆ Fin ∧ (𝑓 supp ∅) ∈ Fin)}–1-1-onto→{𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∣ 𝑟 ∈ Fin})
2622reseq2i 5821 . . . 4 (𝑀𝑆) = (𝑀 ↾ {𝑓 ∈ (𝒫 𝐵m 𝐴) ∣ (ran 𝑓 ⊆ Fin ∧ (𝑓 supp ∅) ∈ Fin)})
27 f1oeq1 6591 . . . 4 ((𝑀𝑆) = (𝑀 ↾ {𝑓 ∈ (𝒫 𝐵m 𝐴) ∣ (ran 𝑓 ⊆ Fin ∧ (𝑓 supp ∅) ∈ Fin)}) → ((𝑀𝑆):{𝑓 ∈ (𝒫 𝐵m 𝐴) ∣ (ran 𝑓 ⊆ Fin ∧ (𝑓 supp ∅) ∈ Fin)}–1-1-onto→{𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∣ 𝑟 ∈ Fin} ↔ (𝑀 ↾ {𝑓 ∈ (𝒫 𝐵m 𝐴) ∣ (ran 𝑓 ⊆ Fin ∧ (𝑓 supp ∅) ∈ Fin)}):{𝑓 ∈ (𝒫 𝐵m 𝐴) ∣ (ran 𝑓 ⊆ Fin ∧ (𝑓 supp ∅) ∈ Fin)}–1-1-onto→{𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∣ 𝑟 ∈ Fin}))
2826, 27ax-mp 5 . . 3 ((𝑀𝑆):{𝑓 ∈ (𝒫 𝐵m 𝐴) ∣ (ran 𝑓 ⊆ Fin ∧ (𝑓 supp ∅) ∈ Fin)}–1-1-onto→{𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∣ 𝑟 ∈ Fin} ↔ (𝑀 ↾ {𝑓 ∈ (𝒫 𝐵m 𝐴) ∣ (ran 𝑓 ⊆ Fin ∧ (𝑓 supp ∅) ∈ Fin)}):{𝑓 ∈ (𝒫 𝐵m 𝐴) ∣ (ran 𝑓 ⊆ Fin ∧ (𝑓 supp ∅) ∈ Fin)}–1-1-onto→{𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∣ 𝑟 ∈ Fin})
2925, 28bitr2i 279 . 2 ((𝑀 ↾ {𝑓 ∈ (𝒫 𝐵m 𝐴) ∣ (ran 𝑓 ⊆ Fin ∧ (𝑓 supp ∅) ∈ Fin)}):{𝑓 ∈ (𝒫 𝐵m 𝐴) ∣ (ran 𝑓 ⊆ Fin ∧ (𝑓 supp ∅) ∈ Fin)}–1-1-onto→{𝑟 ∈ 𝒫 (𝐴 × 𝐵) ∣ 𝑟 ∈ Fin} ↔ (𝑀𝑆):𝑆1-1-onto→(𝒫 (𝐴 × 𝐵) ∩ Fin))
3014, 29mpbi 233 1 (𝑀𝑆):𝑆1-1-onto→(𝒫 (𝐴 × 𝐵) ∩ Fin)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∧ wa 400   = wceq 1539  ⊤wtru 1540   ∈ wcel 2112  {crab 3075  Vcvv 3410   ∩ cin 3858   ⊆ wss 3859  ∅c0 4226  𝒫 cpw 4495  {copab 5095   ↦ cmpt 5113   × cxp 5523  ran crn 5526   ↾ cres 5527  ⟶wf 6332  –1-1-onto→wf1o 6335  ‘cfv 6336  (class class class)co 7151   supp csupp 7836   ↑m cmap 8417  Fincfn 8528 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5235  ax-pr 5299  ax-un 7460  ax-ac2 9924 This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-ral 3076  df-rex 3077  df-reu 3078  df-rmo 3079  df-rab 3080  df-v 3412  df-sbc 3698  df-csb 3807  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-pss 3878  df-nul 4227  df-if 4422  df-pw 4497  df-sn 4524  df-pr 4526  df-tp 4528  df-op 4530  df-uni 4800  df-int 4840  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5431  df-eprel 5436  df-po 5444  df-so 5445  df-fr 5484  df-se 5485  df-we 5486  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-pred 6127  df-ord 6173  df-on 6174  df-lim 6175  df-suc 6176  df-iota 6295  df-fun 6338  df-fn 6339  df-f 6340  df-f1 6341  df-fo 6342  df-f1o 6343  df-fv 6344  df-isom 6345  df-riota 7109  df-ov 7154  df-oprab 7155  df-mpo 7156  df-om 7581  df-1st 7694  df-2nd 7695  df-supp 7837  df-wrecs 7958  df-recs 8019  df-1o 8113  df-er 8300  df-map 8419  df-en 8529  df-dom 8530  df-fin 8532  df-card 9402  df-acn 9405  df-ac 9577 This theorem is referenced by:  eulerpartlem1  31854
 Copyright terms: Public domain W3C validator