Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > fmpo | Structured version Visualization version GIF version |
Description: Functionality, domain and range of a class given by the maps-to notation. (Contributed by FL, 17-May-2010.) |
Ref | Expression |
---|---|
fmpo.1 | ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) |
Ref | Expression |
---|---|
fmpo | ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ↔ 𝐹:(𝐴 × 𝐵)⟶𝐷) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fmpo.1 | . . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | |
2 | 1 | fmpox 7837 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ↔ 𝐹:∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)⟶𝐷) |
3 | iunxpconst 5621 | . . 3 ⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) = (𝐴 × 𝐵) | |
4 | 3 | feq2i 6537 | . 2 ⊢ (𝐹:∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)⟶𝐷 ↔ 𝐹:(𝐴 × 𝐵)⟶𝐷) |
5 | 2, 4 | bitri 278 | 1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ↔ 𝐹:(𝐴 × 𝐵)⟶𝐷) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 = wceq 1543 ∈ wcel 2110 ∀wral 3061 {csn 4541 ∪ ciun 4904 × cxp 5549 ⟶wf 6376 ∈ cmpo 7215 |
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-pr 5322 ax-un 7523 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 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-rab 3070 df-v 3410 df-sbc 3695 df-csb 3812 df-dif 3869 df-un 3871 df-in 3873 df-ss 3883 df-nul 4238 df-if 4440 df-sn 4542 df-pr 4544 df-op 4548 df-uni 4820 df-iun 4906 df-br 5054 df-opab 5116 df-mpt 5136 df-id 5455 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-iota 6338 df-fun 6382 df-fn 6383 df-f 6384 df-fv 6388 df-oprab 7217 df-mpo 7218 df-1st 7761 df-2nd 7762 |
This theorem is referenced by: fnmpo 7839 ovmpoelrn 7842 fmpoco 7863 eroprf 8497 omxpenlem 8746 mapxpen 8812 dffi3 9047 ixpiunwdom 9206 cantnfvalf 9280 iunfictbso 9728 axdc4lem 10069 axcclem 10071 addpqf 10558 mulpqf 10560 subf 11080 xaddf 12814 xmulf 12862 ixxf 12945 ioof 13035 fzf 13099 fzof 13240 axdc4uzlem 13556 sadcf 16012 smupf 16037 gcdf 16071 eucalgf 16140 vdwapf 16525 prdsplusg 16963 prdsmulr 16964 prdsvsca 16965 prdshom 16972 imasvscaf 17044 xpsff1o 17072 wunnat 17463 wunnatOLD 17464 catcoppccl 17623 catcoppcclOLD 17624 catcfuccl 17625 catcfucclOLD 17626 catcxpccl 17714 catcxpcclOLD 17715 evlfcl 17730 hofcl 17767 mgmplusf 18124 grpsubf 18442 subgga 18694 lactghmga 18797 sylow1lem2 18988 sylow3lem1 19016 lsmssv 19032 smndlsmidm 19045 lsmidmOLD 19053 efgmf 19103 efgtf 19112 frgpuptf 19160 lmodscaf 19921 xrsds 20406 phlipf 20614 evlslem2 21039 mamucl 21298 matbas2d 21320 mamumat1cl 21336 ordtbas2 22088 iccordt 22111 txuni2 22462 xkotf 22482 txbasval 22503 tx1stc 22547 xkococn 22557 cnmpt12 22564 cnmpt21 22568 cnmpt2t 22570 cnmpt22 22571 cnmptcom 22575 cnmpt2k 22585 txswaphmeo 22702 xpstopnlem1 22706 cnmpt2plusg 22985 cnmpt2vsca 23092 prdsdsf 23265 blfvalps 23281 blfps 23304 blf 23305 stdbdmet 23414 met2ndci 23420 dscmet 23470 xrsxmet 23706 cnmpt2ds 23740 cnmpopc 23825 iimulcn 23835 ishtpy 23869 reparphti 23894 cnmpt2ip 24145 bcthlem5 24225 rrxmet 24305 dyadf 24488 itg1addlem2 24594 mbfi1fseqlem1 24613 mbfi1fseqlem3 24615 mbfi1fseqlem4 24616 mbfi1fseqlem5 24617 cxpcn3 25634 sgmf 26027 midf 26867 grpodivf 28619 nvmf 28726 ipf 28794 hvsubf 29096 ofoprabco 30721 suppovss 30737 fedgmullem1 31424 fedgmullem2 31425 fedgmul 31426 sitmf 32031 cvxsconn 32918 cvmlift2lem5 32982 uncf 35493 mblfinlem1 35551 mblfinlem2 35552 sdclem1 35638 metf1o 35650 rrnval 35722 rrnmet 35724 resubf 40072 sn-subf 40118 frmx 40438 frmy 40439 mnringmulrcld 41519 icof 42432 |
Copyright terms: Public domain | W3C validator |