![]() |
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 8091 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ↔ 𝐹:∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)⟶𝐷) |
3 | iunxpconst 5761 | . . 3 ⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) = (𝐴 × 𝐵) | |
4 | 3 | feq2i 6729 | . 2 ⊢ (𝐹:∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)⟶𝐷 ↔ 𝐹:(𝐴 × 𝐵)⟶𝐷) |
5 | 2, 4 | bitri 275 | 1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ↔ 𝐹:(𝐴 × 𝐵)⟶𝐷) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 206 = wceq 1537 ∈ wcel 2106 ∀wral 3059 {csn 4631 ∪ ciun 4996 × cxp 5687 ⟶wf 6559 ∈ cmpo 7433 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-10 2139 ax-11 2155 ax-12 2175 ax-ext 2706 ax-sep 5302 ax-nul 5312 ax-pr 5438 ax-un 7754 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1540 df-fal 1550 df-ex 1777 df-nf 1781 df-sb 2063 df-mo 2538 df-eu 2567 df-clab 2713 df-cleq 2727 df-clel 2814 df-nfc 2890 df-ral 3060 df-rex 3069 df-rab 3434 df-v 3480 df-sbc 3792 df-csb 3909 df-dif 3966 df-un 3968 df-in 3970 df-ss 3980 df-nul 4340 df-if 4532 df-sn 4632 df-pr 4634 df-op 4638 df-uni 4913 df-iun 4998 df-br 5149 df-opab 5211 df-mpt 5232 df-id 5583 df-xp 5695 df-rel 5696 df-cnv 5697 df-co 5698 df-dm 5699 df-rn 5700 df-res 5701 df-ima 5702 df-iota 6516 df-fun 6565 df-fn 6566 df-f 6567 df-fv 6571 df-oprab 7435 df-mpo 7436 df-1st 8013 df-2nd 8014 |
This theorem is referenced by: fnmpo 8093 ovmpoelrn 8096 fmpoco 8119 eroprf 8854 omxpenlem 9112 mapxpen 9182 dffi3 9469 ixpiunwdom 9628 cantnfvalf 9703 iunfictbso 10152 axdc4lem 10493 axcclem 10495 addpqf 10982 mulpqf 10984 subf 11508 xaddf 13263 xmulf 13311 ixxf 13394 ioof 13484 fzf 13548 fzof 13693 axdc4uzlem 14021 sadcf 16487 smupf 16512 gcdf 16546 eucalgf 16617 vdwapf 17006 prdsplusg 17505 prdsmulr 17506 prdsvsca 17507 prdshom 17514 imasvscaf 17586 xpsff1o 17614 wunnat 18011 wunnatOLD 18012 catcoppccl 18171 catcoppcclOLD 18172 catcfuccl 18173 catcfucclOLD 18174 catcxpccl 18263 catcxpcclOLD 18264 evlfcl 18279 hofcl 18316 mgmplusf 18676 grpsubf 19050 subgga 19331 lactghmga 19438 sylow1lem2 19632 sylow3lem1 19660 lsmssv 19676 smndlsmidm 19689 efgmf 19746 efgtf 19755 frgpuptf 19803 lmodscaf 20899 xrsds 21445 phlipf 21688 evlslem2 22121 mamucl 22421 matbas2d 22445 mamumat1cl 22461 ordtbas2 23215 iccordt 23238 txuni2 23589 xkotf 23609 txbasval 23630 tx1stc 23674 xkococn 23684 cnmpt12 23691 cnmpt21 23695 cnmpt2t 23697 cnmpt22 23698 cnmptcom 23702 cnmpt2k 23712 txswaphmeo 23829 xpstopnlem1 23833 cnmpt2plusg 24112 cnmpt2vsca 24219 prdsdsf 24393 blfvalps 24409 blfps 24432 blf 24433 stdbdmet 24545 met2ndci 24551 dscmet 24601 xrsxmet 24845 cnmpt2ds 24879 cnmpopc 24969 iimulcn 24981 iimulcnOLD 24982 ishtpy 25018 reparphti 25043 reparphtiOLD 25044 cnmpt2ip 25296 bcthlem5 25376 rrxmet 25456 dyadf 25640 itg1addlem2 25746 mbfi1fseqlem1 25765 mbfi1fseqlem3 25767 mbfi1fseqlem4 25768 mbfi1fseqlem5 25769 cxpcn3 26806 sgmf 27203 subsf 28109 midf 28799 grpodivf 30567 nvmf 30674 ipf 30742 hvsubf 31044 ofoprabco 32681 suppovss 32696 elrgspnlem2 33233 fedgmullem1 33657 fedgmullem2 33658 fedgmul 33659 sitmf 34334 cvxsconn 35228 cvmlift2lem5 35292 uncf 37586 mblfinlem1 37644 mblfinlem2 37645 sdclem1 37730 metf1o 37742 rrnval 37814 rrnmet 37816 aks6d1c3 42105 fmpocos 42254 resubf 42388 sn-subf 42435 evlselv 42574 frmx 42902 frmy 42903 ofoafg 43344 naddcnff 43352 mnringmulrcld 44224 icof 45162 |
Copyright terms: Public domain | W3C validator |