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

Theorem indf1ofs 30470
Description: The bijection between finite subsets and the indicator functions with finite support. (Contributed by Thierry Arnoux, 22-Aug-2017.)
Assertion
Ref Expression
indf1ofs (𝑂𝑉 → ((𝟭‘𝑂) ↾ Fin):(𝒫 𝑂 ∩ Fin)–1-1-onto→{𝑓 ∈ ({0, 1} ↑𝑚 𝑂) ∣ (𝑓 “ {1}) ∈ Fin})
Distinct variable group:   𝑓,𝑂
Allowed substitution hint:   𝑉(𝑓)

Proof of Theorem indf1ofs
Dummy variables 𝑎 𝑔 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 indf1o 30468 . . . 4 (𝑂𝑉 → (𝟭‘𝑂):𝒫 𝑂1-1-onto→({0, 1} ↑𝑚 𝑂))
2 f1of1 6319 . . . 4 ((𝟭‘𝑂):𝒫 𝑂1-1-onto→({0, 1} ↑𝑚 𝑂) → (𝟭‘𝑂):𝒫 𝑂1-1→({0, 1} ↑𝑚 𝑂))
31, 2syl 17 . . 3 (𝑂𝑉 → (𝟭‘𝑂):𝒫 𝑂1-1→({0, 1} ↑𝑚 𝑂))
4 inss1 3992 . . 3 (𝒫 𝑂 ∩ Fin) ⊆ 𝒫 𝑂
5 f1ores 6334 . . 3 (((𝟭‘𝑂):𝒫 𝑂1-1→({0, 1} ↑𝑚 𝑂) ∧ (𝒫 𝑂 ∩ Fin) ⊆ 𝒫 𝑂) → ((𝟭‘𝑂) ↾ (𝒫 𝑂 ∩ Fin)):(𝒫 𝑂 ∩ Fin)–1-1-onto→((𝟭‘𝑂) “ (𝒫 𝑂 ∩ Fin)))
63, 4, 5sylancl 580 . 2 (𝑂𝑉 → ((𝟭‘𝑂) ↾ (𝒫 𝑂 ∩ Fin)):(𝒫 𝑂 ∩ Fin)–1-1-onto→((𝟭‘𝑂) “ (𝒫 𝑂 ∩ Fin)))
7 resres 5585 . . . 4 (((𝟭‘𝑂) ↾ 𝒫 𝑂) ↾ Fin) = ((𝟭‘𝑂) ↾ (𝒫 𝑂 ∩ Fin))
8 f1ofn 6321 . . . . . 6 ((𝟭‘𝑂):𝒫 𝑂1-1-onto→({0, 1} ↑𝑚 𝑂) → (𝟭‘𝑂) Fn 𝒫 𝑂)
9 fnresdm 6178 . . . . . 6 ((𝟭‘𝑂) Fn 𝒫 𝑂 → ((𝟭‘𝑂) ↾ 𝒫 𝑂) = (𝟭‘𝑂))
101, 8, 93syl 18 . . . . 5 (𝑂𝑉 → ((𝟭‘𝑂) ↾ 𝒫 𝑂) = (𝟭‘𝑂))
1110reseq1d 5564 . . . 4 (𝑂𝑉 → (((𝟭‘𝑂) ↾ 𝒫 𝑂) ↾ Fin) = ((𝟭‘𝑂) ↾ Fin))
127, 11syl5eqr 2813 . . 3 (𝑂𝑉 → ((𝟭‘𝑂) ↾ (𝒫 𝑂 ∩ Fin)) = ((𝟭‘𝑂) ↾ Fin))
13 eqidd 2766 . . 3 (𝑂𝑉 → (𝒫 𝑂 ∩ Fin) = (𝒫 𝑂 ∩ Fin))
14 simpll 783 . . . . . . . . . 10 (((𝑂𝑉𝑎 ∈ (𝒫 𝑂 ∩ Fin)) ∧ ((𝟭‘𝑂)‘𝑎) = 𝑔) → 𝑂𝑉)
15 simpr 477 . . . . . . . . . . . . . . 15 ((𝑂𝑉𝑎 ∈ (𝒫 𝑂 ∩ Fin)) → 𝑎 ∈ (𝒫 𝑂 ∩ Fin))
164, 15sseldi 3759 . . . . . . . . . . . . . 14 ((𝑂𝑉𝑎 ∈ (𝒫 𝑂 ∩ Fin)) → 𝑎 ∈ 𝒫 𝑂)
1716elpwid 4327 . . . . . . . . . . . . 13 ((𝑂𝑉𝑎 ∈ (𝒫 𝑂 ∩ Fin)) → 𝑎𝑂)
18 indf 30459 . . . . . . . . . . . . 13 ((𝑂𝑉𝑎𝑂) → ((𝟭‘𝑂)‘𝑎):𝑂⟶{0, 1})
1917, 18syldan 585 . . . . . . . . . . . 12 ((𝑂𝑉𝑎 ∈ (𝒫 𝑂 ∩ Fin)) → ((𝟭‘𝑂)‘𝑎):𝑂⟶{0, 1})
2019adantr 472 . . . . . . . . . . 11 (((𝑂𝑉𝑎 ∈ (𝒫 𝑂 ∩ Fin)) ∧ ((𝟭‘𝑂)‘𝑎) = 𝑔) → ((𝟭‘𝑂)‘𝑎):𝑂⟶{0, 1})
21 simpr 477 . . . . . . . . . . . 12 (((𝑂𝑉𝑎 ∈ (𝒫 𝑂 ∩ Fin)) ∧ ((𝟭‘𝑂)‘𝑎) = 𝑔) → ((𝟭‘𝑂)‘𝑎) = 𝑔)
2221feq1d 6208 . . . . . . . . . . 11 (((𝑂𝑉𝑎 ∈ (𝒫 𝑂 ∩ Fin)) ∧ ((𝟭‘𝑂)‘𝑎) = 𝑔) → (((𝟭‘𝑂)‘𝑎):𝑂⟶{0, 1} ↔ 𝑔:𝑂⟶{0, 1}))
2320, 22mpbid 223 . . . . . . . . . 10 (((𝑂𝑉𝑎 ∈ (𝒫 𝑂 ∩ Fin)) ∧ ((𝟭‘𝑂)‘𝑎) = 𝑔) → 𝑔:𝑂⟶{0, 1})
24 prex 5065 . . . . . . . . . . . 12 {0, 1} ∈ V
25 elmapg 8073 . . . . . . . . . . . 12 (({0, 1} ∈ V ∧ 𝑂𝑉) → (𝑔 ∈ ({0, 1} ↑𝑚 𝑂) ↔ 𝑔:𝑂⟶{0, 1}))
2624, 25mpan 681 . . . . . . . . . . 11 (𝑂𝑉 → (𝑔 ∈ ({0, 1} ↑𝑚 𝑂) ↔ 𝑔:𝑂⟶{0, 1}))
2726biimpar 469 . . . . . . . . . 10 ((𝑂𝑉𝑔:𝑂⟶{0, 1}) → 𝑔 ∈ ({0, 1} ↑𝑚 𝑂))
2814, 23, 27syl2anc 579 . . . . . . . . 9 (((𝑂𝑉𝑎 ∈ (𝒫 𝑂 ∩ Fin)) ∧ ((𝟭‘𝑂)‘𝑎) = 𝑔) → 𝑔 ∈ ({0, 1} ↑𝑚 𝑂))
2921cnveqd 5466 . . . . . . . . . . 11 (((𝑂𝑉𝑎 ∈ (𝒫 𝑂 ∩ Fin)) ∧ ((𝟭‘𝑂)‘𝑎) = 𝑔) → ((𝟭‘𝑂)‘𝑎) = 𝑔)
3029imaeq1d 5647 . . . . . . . . . 10 (((𝑂𝑉𝑎 ∈ (𝒫 𝑂 ∩ Fin)) ∧ ((𝟭‘𝑂)‘𝑎) = 𝑔) → (((𝟭‘𝑂)‘𝑎) “ {1}) = (𝑔 “ {1}))
31 indpi1 30464 . . . . . . . . . . . . 13 ((𝑂𝑉𝑎𝑂) → (((𝟭‘𝑂)‘𝑎) “ {1}) = 𝑎)
3217, 31syldan 585 . . . . . . . . . . . 12 ((𝑂𝑉𝑎 ∈ (𝒫 𝑂 ∩ Fin)) → (((𝟭‘𝑂)‘𝑎) “ {1}) = 𝑎)
33 inss2 3993 . . . . . . . . . . . . 13 (𝒫 𝑂 ∩ Fin) ⊆ Fin
3433, 15sseldi 3759 . . . . . . . . . . . 12 ((𝑂𝑉𝑎 ∈ (𝒫 𝑂 ∩ Fin)) → 𝑎 ∈ Fin)
3532, 34eqeltrd 2844 . . . . . . . . . . 11 ((𝑂𝑉𝑎 ∈ (𝒫 𝑂 ∩ Fin)) → (((𝟭‘𝑂)‘𝑎) “ {1}) ∈ Fin)
3635adantr 472 . . . . . . . . . 10 (((𝑂𝑉𝑎 ∈ (𝒫 𝑂 ∩ Fin)) ∧ ((𝟭‘𝑂)‘𝑎) = 𝑔) → (((𝟭‘𝑂)‘𝑎) “ {1}) ∈ Fin)
3730, 36eqeltrrd 2845 . . . . . . . . 9 (((𝑂𝑉𝑎 ∈ (𝒫 𝑂 ∩ Fin)) ∧ ((𝟭‘𝑂)‘𝑎) = 𝑔) → (𝑔 “ {1}) ∈ Fin)
3828, 37jca 507 . . . . . . . 8 (((𝑂𝑉𝑎 ∈ (𝒫 𝑂 ∩ Fin)) ∧ ((𝟭‘𝑂)‘𝑎) = 𝑔) → (𝑔 ∈ ({0, 1} ↑𝑚 𝑂) ∧ (𝑔 “ {1}) ∈ Fin))
3938ex 401 . . . . . . 7 ((𝑂𝑉𝑎 ∈ (𝒫 𝑂 ∩ Fin)) → (((𝟭‘𝑂)‘𝑎) = 𝑔 → (𝑔 ∈ ({0, 1} ↑𝑚 𝑂) ∧ (𝑔 “ {1}) ∈ Fin)))
4039rexlimdva 3178 . . . . . 6 (𝑂𝑉 → (∃𝑎 ∈ (𝒫 𝑂 ∩ Fin)((𝟭‘𝑂)‘𝑎) = 𝑔 → (𝑔 ∈ ({0, 1} ↑𝑚 𝑂) ∧ (𝑔 “ {1}) ∈ Fin)))
41 cnvimass 5667 . . . . . . . . . 10 (𝑔 “ {1}) ⊆ dom 𝑔
4226biimpa 468 . . . . . . . . . . . 12 ((𝑂𝑉𝑔 ∈ ({0, 1} ↑𝑚 𝑂)) → 𝑔:𝑂⟶{0, 1})
4342fdmd 6232 . . . . . . . . . . 11 ((𝑂𝑉𝑔 ∈ ({0, 1} ↑𝑚 𝑂)) → dom 𝑔 = 𝑂)
4443adantrr 708 . . . . . . . . . 10 ((𝑂𝑉 ∧ (𝑔 ∈ ({0, 1} ↑𝑚 𝑂) ∧ (𝑔 “ {1}) ∈ Fin)) → dom 𝑔 = 𝑂)
4541, 44syl5sseq 3813 . . . . . . . . 9 ((𝑂𝑉 ∧ (𝑔 ∈ ({0, 1} ↑𝑚 𝑂) ∧ (𝑔 “ {1}) ∈ Fin)) → (𝑔 “ {1}) ⊆ 𝑂)
46 simprr 789 . . . . . . . . 9 ((𝑂𝑉 ∧ (𝑔 ∈ ({0, 1} ↑𝑚 𝑂) ∧ (𝑔 “ {1}) ∈ Fin)) → (𝑔 “ {1}) ∈ Fin)
47 elfpw 8475 . . . . . . . . 9 ((𝑔 “ {1}) ∈ (𝒫 𝑂 ∩ Fin) ↔ ((𝑔 “ {1}) ⊆ 𝑂 ∧ (𝑔 “ {1}) ∈ Fin))
4845, 46, 47sylanbrc 578 . . . . . . . 8 ((𝑂𝑉 ∧ (𝑔 ∈ ({0, 1} ↑𝑚 𝑂) ∧ (𝑔 “ {1}) ∈ Fin)) → (𝑔 “ {1}) ∈ (𝒫 𝑂 ∩ Fin))
49 indpreima 30469 . . . . . . . . . . 11 ((𝑂𝑉𝑔:𝑂⟶{0, 1}) → 𝑔 = ((𝟭‘𝑂)‘(𝑔 “ {1})))
5049eqcomd 2771 . . . . . . . . . 10 ((𝑂𝑉𝑔:𝑂⟶{0, 1}) → ((𝟭‘𝑂)‘(𝑔 “ {1})) = 𝑔)
5142, 50syldan 585 . . . . . . . . 9 ((𝑂𝑉𝑔 ∈ ({0, 1} ↑𝑚 𝑂)) → ((𝟭‘𝑂)‘(𝑔 “ {1})) = 𝑔)
5251adantrr 708 . . . . . . . 8 ((𝑂𝑉 ∧ (𝑔 ∈ ({0, 1} ↑𝑚 𝑂) ∧ (𝑔 “ {1}) ∈ Fin)) → ((𝟭‘𝑂)‘(𝑔 “ {1})) = 𝑔)
53 fveqeq2 6384 . . . . . . . . 9 (𝑎 = (𝑔 “ {1}) → (((𝟭‘𝑂)‘𝑎) = 𝑔 ↔ ((𝟭‘𝑂)‘(𝑔 “ {1})) = 𝑔))
5453rspcev 3461 . . . . . . . 8 (((𝑔 “ {1}) ∈ (𝒫 𝑂 ∩ Fin) ∧ ((𝟭‘𝑂)‘(𝑔 “ {1})) = 𝑔) → ∃𝑎 ∈ (𝒫 𝑂 ∩ Fin)((𝟭‘𝑂)‘𝑎) = 𝑔)
5548, 52, 54syl2anc 579 . . . . . . 7 ((𝑂𝑉 ∧ (𝑔 ∈ ({0, 1} ↑𝑚 𝑂) ∧ (𝑔 “ {1}) ∈ Fin)) → ∃𝑎 ∈ (𝒫 𝑂 ∩ Fin)((𝟭‘𝑂)‘𝑎) = 𝑔)
5655ex 401 . . . . . 6 (𝑂𝑉 → ((𝑔 ∈ ({0, 1} ↑𝑚 𝑂) ∧ (𝑔 “ {1}) ∈ Fin) → ∃𝑎 ∈ (𝒫 𝑂 ∩ Fin)((𝟭‘𝑂)‘𝑎) = 𝑔))
5740, 56impbid 203 . . . . 5 (𝑂𝑉 → (∃𝑎 ∈ (𝒫 𝑂 ∩ Fin)((𝟭‘𝑂)‘𝑎) = 𝑔 ↔ (𝑔 ∈ ({0, 1} ↑𝑚 𝑂) ∧ (𝑔 “ {1}) ∈ Fin)))
581, 8syl 17 . . . . . 6 (𝑂𝑉 → (𝟭‘𝑂) Fn 𝒫 𝑂)
59 fvelimab 6442 . . . . . 6 (((𝟭‘𝑂) Fn 𝒫 𝑂 ∧ (𝒫 𝑂 ∩ Fin) ⊆ 𝒫 𝑂) → (𝑔 ∈ ((𝟭‘𝑂) “ (𝒫 𝑂 ∩ Fin)) ↔ ∃𝑎 ∈ (𝒫 𝑂 ∩ Fin)((𝟭‘𝑂)‘𝑎) = 𝑔))
6058, 4, 59sylancl 580 . . . . 5 (𝑂𝑉 → (𝑔 ∈ ((𝟭‘𝑂) “ (𝒫 𝑂 ∩ Fin)) ↔ ∃𝑎 ∈ (𝒫 𝑂 ∩ Fin)((𝟭‘𝑂)‘𝑎) = 𝑔))
61 cnveq 5464 . . . . . . . . 9 (𝑓 = 𝑔𝑓 = 𝑔)
6261imaeq1d 5647 . . . . . . . 8 (𝑓 = 𝑔 → (𝑓 “ {1}) = (𝑔 “ {1}))
6362eleq1d 2829 . . . . . . 7 (𝑓 = 𝑔 → ((𝑓 “ {1}) ∈ Fin ↔ (𝑔 “ {1}) ∈ Fin))
6463elrab 3519 . . . . . 6 (𝑔 ∈ {𝑓 ∈ ({0, 1} ↑𝑚 𝑂) ∣ (𝑓 “ {1}) ∈ Fin} ↔ (𝑔 ∈ ({0, 1} ↑𝑚 𝑂) ∧ (𝑔 “ {1}) ∈ Fin))
6564a1i 11 . . . . 5 (𝑂𝑉 → (𝑔 ∈ {𝑓 ∈ ({0, 1} ↑𝑚 𝑂) ∣ (𝑓 “ {1}) ∈ Fin} ↔ (𝑔 ∈ ({0, 1} ↑𝑚 𝑂) ∧ (𝑔 “ {1}) ∈ Fin)))
6657, 60, 653bitr4d 302 . . . 4 (𝑂𝑉 → (𝑔 ∈ ((𝟭‘𝑂) “ (𝒫 𝑂 ∩ Fin)) ↔ 𝑔 ∈ {𝑓 ∈ ({0, 1} ↑𝑚 𝑂) ∣ (𝑓 “ {1}) ∈ Fin}))
6766eqrdv 2763 . . 3 (𝑂𝑉 → ((𝟭‘𝑂) “ (𝒫 𝑂 ∩ Fin)) = {𝑓 ∈ ({0, 1} ↑𝑚 𝑂) ∣ (𝑓 “ {1}) ∈ Fin})
6812, 13, 67f1oeq123d 6316 . 2 (𝑂𝑉 → (((𝟭‘𝑂) ↾ (𝒫 𝑂 ∩ Fin)):(𝒫 𝑂 ∩ Fin)–1-1-onto→((𝟭‘𝑂) “ (𝒫 𝑂 ∩ Fin)) ↔ ((𝟭‘𝑂) ↾ Fin):(𝒫 𝑂 ∩ Fin)–1-1-onto→{𝑓 ∈ ({0, 1} ↑𝑚 𝑂) ∣ (𝑓 “ {1}) ∈ Fin}))
696, 68mpbid 223 1 (𝑂𝑉 → ((𝟭‘𝑂) ↾ Fin):(𝒫 𝑂 ∩ Fin)–1-1-onto→{𝑓 ∈ ({0, 1} ↑𝑚 𝑂) ∣ (𝑓 “ {1}) ∈ Fin})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384   = wceq 1652  wcel 2155  wrex 3056  {crab 3059  Vcvv 3350  cin 3731  wss 3732  𝒫 cpw 4315  {csn 4334  {cpr 4336  ccnv 5276  dom cdm 5277  cres 5279  cima 5280   Fn wfn 6063  wf 6064  1-1wf1 6065  1-1-ontowf1o 6067  cfv 6068  (class class class)co 6842  𝑚 cmap 8060  Fincfn 8160  0cc0 10189  1c1 10190  𝟭cind 30454
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-i2m1 10257  ax-1ne0 10258  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-reu 3062  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-op 4341  df-uni 4595  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-id 5185  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-map 8062  df-ind 30455
This theorem is referenced by:  eulerpartgbij  30816
  Copyright terms: Public domain W3C validator