Mathbox for Alexander van der Vekens |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > cfsetsnfsetfv | Structured version Visualization version GIF version |
Description: The function value of the mapping of the class of singleton functions into the class of constant functions. (Contributed by AV, 13-Sep-2024.) |
Ref | Expression |
---|---|
cfsetsnfsetfv.f | ⊢ 𝐹 = {𝑓 ∣ (𝑓:𝐴⟶𝐵 ∧ ∃𝑏 ∈ 𝐵 ∀𝑧 ∈ 𝐴 (𝑓‘𝑧) = 𝑏)} |
cfsetsnfsetfv.g | ⊢ 𝐺 = {𝑥 ∣ 𝑥:{𝑌}⟶𝐵} |
cfsetsnfsetfv.h | ⊢ 𝐻 = (𝑔 ∈ 𝐺 ↦ (𝑎 ∈ 𝐴 ↦ (𝑔‘𝑌))) |
Ref | Expression |
---|---|
cfsetsnfsetfv | ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐺) → (𝐻‘𝑋) = (𝑎 ∈ 𝐴 ↦ (𝑋‘𝑌))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cfsetsnfsetfv.h | . . 3 ⊢ 𝐻 = (𝑔 ∈ 𝐺 ↦ (𝑎 ∈ 𝐴 ↦ (𝑔‘𝑌))) | |
2 | 1 | a1i 11 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐺) → 𝐻 = (𝑔 ∈ 𝐺 ↦ (𝑎 ∈ 𝐴 ↦ (𝑔‘𝑌)))) |
3 | fveq1 6663 | . . . . 5 ⊢ (𝑔 = 𝑋 → (𝑔‘𝑌) = (𝑋‘𝑌)) | |
4 | 3 | adantr 484 | . . . 4 ⊢ ((𝑔 = 𝑋 ∧ 𝑎 ∈ 𝐴) → (𝑔‘𝑌) = (𝑋‘𝑌)) |
5 | 4 | mpteq2dva 5132 | . . 3 ⊢ (𝑔 = 𝑋 → (𝑎 ∈ 𝐴 ↦ (𝑔‘𝑌)) = (𝑎 ∈ 𝐴 ↦ (𝑋‘𝑌))) |
6 | 5 | adantl 485 | . 2 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐺) ∧ 𝑔 = 𝑋) → (𝑎 ∈ 𝐴 ↦ (𝑔‘𝑌)) = (𝑎 ∈ 𝐴 ↦ (𝑋‘𝑌))) |
7 | simpr 488 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐺) → 𝑋 ∈ 𝐺) | |
8 | simpl 486 | . . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐺) → 𝐴 ∈ 𝑉) | |
9 | 8 | mptexd 6985 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐺) → (𝑎 ∈ 𝐴 ↦ (𝑋‘𝑌)) ∈ V) |
10 | 2, 6, 7, 9 | fvmptd 6772 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐺) → (𝐻‘𝑋) = (𝑎 ∈ 𝐴 ↦ (𝑋‘𝑌))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 = wceq 1539 ∈ wcel 2112 {cab 2736 ∀wral 3071 ∃wrex 3072 Vcvv 3410 {csn 4526 ↦ cmpt 5117 ⟶wf 6337 ‘cfv 6341 |
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 5161 ax-sep 5174 ax-nul 5181 ax-pr 5303 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 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-rab 3080 df-v 3412 df-sbc 3700 df-csb 3809 df-dif 3864 df-un 3866 df-in 3868 df-ss 3878 df-nul 4229 df-if 4425 df-sn 4527 df-pr 4529 df-op 4533 df-uni 4803 df-iun 4889 df-br 5038 df-opab 5100 df-mpt 5118 df-id 5435 df-xp 5535 df-rel 5536 df-cnv 5537 df-co 5538 df-dm 5539 df-rn 5540 df-res 5541 df-ima 5542 df-iota 6300 df-fun 6343 df-fn 6344 df-f 6345 df-f1 6346 df-fo 6347 df-f1o 6348 df-fv 6349 |
This theorem is referenced by: cfsetsnfsetf1 44062 cfsetsnfsetfo 44063 |
Copyright terms: Public domain | W3C validator |