| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > fmpt | GIF version | ||
| Description: Functionality of the mapping operation. (Contributed by Mario Carneiro, 26-Jul-2013.) (Revised by Mario Carneiro, 31-Aug-2015.) |
| Ref | Expression |
|---|---|
| fmpt.1 | ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶) |
| Ref | Expression |
|---|---|
| fmpt | ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐵) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fmpt.1 | . . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶) | |
| 2 | 1 | fnmpt 5456 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹 Fn 𝐴) |
| 3 | 1 | rnmpt 4978 | . . . 4 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶} |
| 4 | r19.29 2668 | . . . . . . 7 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → ∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶)) | |
| 5 | eleq1 2292 | . . . . . . . . 9 ⊢ (𝑦 = 𝐶 → (𝑦 ∈ 𝐵 ↔ 𝐶 ∈ 𝐵)) | |
| 6 | 5 | biimparc 299 | . . . . . . . 8 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵) |
| 7 | 6 | rexlimivw 2644 | . . . . . . 7 ⊢ (∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵) |
| 8 | 4, 7 | syl 14 | . . . . . 6 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → 𝑦 ∈ 𝐵) |
| 9 | 8 | ex 115 | . . . . 5 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = 𝐶 → 𝑦 ∈ 𝐵)) |
| 10 | 9 | abssdv 3299 | . . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶} ⊆ 𝐵) |
| 11 | 3, 10 | eqsstrid 3271 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → ran 𝐹 ⊆ 𝐵) |
| 12 | df-f 5328 | . . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)) | |
| 13 | 2, 11, 12 | sylanbrc 417 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹:𝐴⟶𝐵) |
| 14 | fimacnv 5772 | . . . 4 ⊢ (𝐹:𝐴⟶𝐵 → (◡𝐹 “ 𝐵) = 𝐴) | |
| 15 | 1 | mptpreima 5228 | . . . 4 ⊢ (◡𝐹 “ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵} |
| 16 | 14, 15 | eqtr3di 2277 | . . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵}) |
| 17 | rabid2 2708 | . . 3 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵} ↔ ∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵) | |
| 18 | 16, 17 | sylib 122 | . 2 ⊢ (𝐹:𝐴⟶𝐵 → ∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵) |
| 19 | 13, 18 | impbii 126 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐵) |
| Colors of variables: wff set class |
| Syntax hints: ∧ wa 104 ↔ wb 105 = wceq 1395 ∈ wcel 2200 {cab 2215 ∀wral 2508 ∃wrex 2509 {crab 2512 ⊆ wss 3198 ↦ cmpt 4148 ◡ccnv 4722 ran crn 4724 “ cima 4726 Fn wfn 5319 ⟶wf 5320 |
| 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-14 2203 ax-ext 2211 ax-sep 4205 ax-pow 4262 ax-pr 4297 |
| 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-rab 2517 df-v 2802 df-sbc 3030 df-un 3202 df-in 3204 df-ss 3211 df-pw 3652 df-sn 3673 df-pr 3674 df-op 3676 df-uni 3892 df-br 4087 df-opab 4149 df-mpt 4150 df-id 4388 df-xp 4729 df-rel 4730 df-cnv 4731 df-co 4732 df-dm 4733 df-rn 4734 df-res 4735 df-ima 4736 df-iota 5284 df-fun 5326 df-fn 5327 df-f 5328 df-fv 5332 |
| This theorem is referenced by: f1ompt 5794 fmpti 5795 fvmptelcdm 5796 fmptd 5797 fmptdf 5800 rnmptss 5804 f1oresrab 5808 idref 5892 f1mpt 5907 f1stres 6317 f2ndres 6318 fmpox 6360 fmpoco 6376 iunon 6445 mptelixpg 6898 dom2lem 6940 uzf 9748 ccatalpha 11180 pcmptcl 12905 gsumfzmhm2 13921 upxp 14986 txdis1cn 14992 cnmpt11 14997 cnmpt21 15005 fsumcncntop 15281 cncfmpt1f 15312 mulcncflem 15321 mulcncf 15322 cnmptlimc 15388 sincn 15483 coscn 15484 lgseisenlem3 15791 |
| Copyright terms: Public domain | W3C validator |