![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fnco | Structured version Visualization version GIF version |
Description: Composition of two functions with domains as a function with domain. (Contributed by NM, 22-May-2006.) (Proof shortened by AV, 20-Sep-2024.) |
Ref | Expression |
---|---|
fnco | ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐴) → (𝐹 ∘ 𝐺) Fn 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fnfun 6668 | . . . 4 ⊢ (𝐺 Fn 𝐵 → Fun 𝐺) | |
2 | fncofn 6685 | . . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ Fun 𝐺) → (𝐹 ∘ 𝐺) Fn (◡𝐺 “ 𝐴)) | |
3 | 1, 2 | sylan2 593 | . . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) → (𝐹 ∘ 𝐺) Fn (◡𝐺 “ 𝐴)) |
4 | 3 | 3adant3 1131 | . 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐴) → (𝐹 ∘ 𝐺) Fn (◡𝐺 “ 𝐴)) |
5 | cnvimassrndm 6173 | . . . . 5 ⊢ (ran 𝐺 ⊆ 𝐴 → (◡𝐺 “ 𝐴) = dom 𝐺) | |
6 | 5 | 3ad2ant3 1134 | . . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐴) → (◡𝐺 “ 𝐴) = dom 𝐺) |
7 | fndm 6671 | . . . . 5 ⊢ (𝐺 Fn 𝐵 → dom 𝐺 = 𝐵) | |
8 | 7 | 3ad2ant2 1133 | . . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐴) → dom 𝐺 = 𝐵) |
9 | 6, 8 | eqtr2d 2775 | . . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐴) → 𝐵 = (◡𝐺 “ 𝐴)) |
10 | 9 | fneq2d 6662 | . 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐴) → ((𝐹 ∘ 𝐺) Fn 𝐵 ↔ (𝐹 ∘ 𝐺) Fn (◡𝐺 “ 𝐴))) |
11 | 4, 10 | mpbird 257 | 1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐴) → (𝐹 ∘ 𝐺) Fn 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1086 = wceq 1536 ⊆ wss 3962 ◡ccnv 5687 dom cdm 5688 ran crn 5689 “ cima 5691 ∘ ccom 5692 Fun wfun 6556 Fn wfn 6557 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-10 2138 ax-11 2154 ax-12 2174 ax-ext 2705 ax-sep 5301 ax-nul 5311 ax-pr 5437 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1539 df-fal 1549 df-ex 1776 df-nf 1780 df-sb 2062 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2726 df-clel 2813 df-nfc 2889 df-ral 3059 df-rex 3068 df-rab 3433 df-v 3479 df-dif 3965 df-un 3967 df-in 3969 df-ss 3979 df-nul 4339 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-br 5148 df-opab 5210 df-id 5582 df-xp 5694 df-rel 5695 df-cnv 5696 df-co 5697 df-dm 5698 df-rn 5699 df-res 5700 df-ima 5701 df-fun 6564 df-fn 6565 |
This theorem is referenced by: fnfco 6773 fsplitfpar 8141 fipreima 9395 updjudhcoinlf 9969 updjudhcoinrg 9970 cshco 14871 swrdco 14872 isofn 17822 prdsinvlem 19079 prdsmgp 20168 pws1 20338 frlmbas 21792 frlmup3 21837 frlmup4 21838 evlslem1 22123 upxp 23646 uptx 23648 0vfval 30634 xppreima2 32667 psgnfzto1stlem 33102 tocycfvres1 33112 tocycfvres2 33113 cycpmfvlem 33114 cycpmfv3 33117 cycpmco2 33135 sseqfv1 34370 sseqfn 34371 sseqfv2 34375 volsupnfl 37651 ftc1anclem5 37683 ftc1anclem8 37686 choicefi 45142 fourierdlem42 46104 fcoreslem4 47015 ackvalsucsucval 48537 |
Copyright terms: Public domain | W3C validator |