| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > fvexg | GIF version | ||
| Description: Evaluating a set function at a set exists. (Contributed by Mario Carneiro and Jim Kingdon, 28-May-2019.) |
| Ref | Expression |
|---|---|
| fvexg | ⊢ ((𝐹 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝐹‘𝐴) ∈ V) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elex 2811 | . . 3 ⊢ (𝐴 ∈ 𝑊 → 𝐴 ∈ V) | |
| 2 | fvssunirng 5647 | . . 3 ⊢ (𝐴 ∈ V → (𝐹‘𝐴) ⊆ ∪ ran 𝐹) | |
| 3 | 1, 2 | syl 14 | . 2 ⊢ (𝐴 ∈ 𝑊 → (𝐹‘𝐴) ⊆ ∪ ran 𝐹) |
| 4 | rnexg 4992 | . . 3 ⊢ (𝐹 ∈ 𝑉 → ran 𝐹 ∈ V) | |
| 5 | uniexg 4531 | . . 3 ⊢ (ran 𝐹 ∈ V → ∪ ran 𝐹 ∈ V) | |
| 6 | 4, 5 | syl 14 | . 2 ⊢ (𝐹 ∈ 𝑉 → ∪ ran 𝐹 ∈ V) |
| 7 | ssexg 4223 | . 2 ⊢ (((𝐹‘𝐴) ⊆ ∪ ran 𝐹 ∧ ∪ ran 𝐹 ∈ V) → (𝐹‘𝐴) ∈ V) | |
| 8 | 3, 6, 7 | syl2anr 290 | 1 ⊢ ((𝐹 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝐹‘𝐴) ∈ V) |
| Colors of variables: wff set class |
| Syntax hints: → wi 4 ∧ wa 104 ∈ wcel 2200 Vcvv 2799 ⊆ wss 3197 ∪ cuni 3888 ran crn 4721 ‘cfv 5321 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 714 ax-5 1493 ax-7 1494 ax-gen 1495 ax-ie1 1539 ax-ie2 1540 ax-8 1550 ax-10 1551 ax-11 1552 ax-i12 1553 ax-bndl 1555 ax-4 1556 ax-17 1572 ax-i9 1576 ax-ial 1580 ax-i5r 1581 ax-13 2202 ax-14 2203 ax-ext 2211 ax-sep 4202 ax-pow 4259 ax-pr 4294 ax-un 4525 |
| This theorem depends on definitions: df-bi 117 df-3an 1004 df-tru 1398 df-nf 1507 df-sb 1809 df-eu 2080 df-mo 2081 df-clab 2216 df-cleq 2222 df-clel 2225 df-nfc 2361 df-ral 2513 df-rex 2514 df-v 2801 df-un 3201 df-in 3203 df-ss 3210 df-pw 3651 df-sn 3672 df-pr 3673 df-op 3675 df-uni 3889 df-br 4084 df-opab 4146 df-cnv 4728 df-dm 4730 df-rn 4731 df-iota 5281 df-fv 5329 |
| This theorem is referenced by: fvex 5652 ovexg 6044 rdgivallem 6538 frecabex 6555 mapsnconst 6854 cc2lem 7468 addvalex 8047 uzennn 10675 seq1g 10702 seqp1g 10705 seqclg 10711 seqm1g 10713 seqfeq4g 10770 lswwrd 11136 ccatlen 11148 ccatval2 11151 ccatvalfn 11154 ccatalpha 11166 eqs1 11181 swrdlen 11205 swrdfv 11206 swrdwrdsymbg 11217 swrdswrd 11258 absval 11533 climmpt 11832 strnfvnd 13073 prdsex 13323 prdsval 13327 prdsbaslemss 13328 prdsbas 13330 prdsplusgfval 13338 prdsmulrfval 13340 pwsplusgval 13349 pwsmulrval 13350 imasex 13359 imasival 13360 imasbas 13361 imasplusg 13362 imasmulr 13363 imasaddfnlemg 13368 imasaddvallemg 13369 gsumfzval 13445 gsumval2 13451 gsumsplit1r 13452 gsumprval 13453 gsumfzz 13549 gsumwsubmcl 13550 gsumfzcl 13553 grpsubval 13600 mulgval 13680 mulgfng 13682 mulgnngsum 13685 znval 14621 znle 14622 znbaslemnn 14624 znbas 14629 znzrhval 14632 znzrhfo 14633 znleval 14638 iscnp4 14913 cnpnei 14914 wlkvtxiedg 16117 wlkvtxiedgg 16118 wlk1walkdom 16131 wlklenvclwlk 16145 |
| Copyright terms: Public domain | W3C validator |