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 6479 | . . . 4 ⊢ (𝐺 Fn 𝐵 → Fun 𝐺) | |
2 | fncofn 6493 | . . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ Fun 𝐺) → (𝐹 ∘ 𝐺) Fn (◡𝐺 “ 𝐴)) | |
3 | 1, 2 | sylan2 596 | . . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) → (𝐹 ∘ 𝐺) Fn (◡𝐺 “ 𝐴)) |
4 | 3 | 3adant3 1134 | . 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐴) → (𝐹 ∘ 𝐺) Fn (◡𝐺 “ 𝐴)) |
5 | cnvimassrndm 6015 | . . . . 5 ⊢ (ran 𝐺 ⊆ 𝐴 → (◡𝐺 “ 𝐴) = dom 𝐺) | |
6 | 5 | 3ad2ant3 1137 | . . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐴) → (◡𝐺 “ 𝐴) = dom 𝐺) |
7 | fndm 6481 | . . . . 5 ⊢ (𝐺 Fn 𝐵 → dom 𝐺 = 𝐵) | |
8 | 7 | 3ad2ant2 1136 | . . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐴) → dom 𝐺 = 𝐵) |
9 | 6, 8 | eqtr2d 2778 | . . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐴) → 𝐵 = (◡𝐺 “ 𝐴)) |
10 | 9 | fneq2d 6473 | . 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐴) → ((𝐹 ∘ 𝐺) Fn 𝐵 ↔ (𝐹 ∘ 𝐺) Fn (◡𝐺 “ 𝐴))) |
11 | 4, 10 | mpbird 260 | 1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐴) → (𝐹 ∘ 𝐺) Fn 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1089 = wceq 1543 ⊆ wss 3866 ◡ccnv 5550 dom cdm 5551 ran crn 5552 “ cima 5554 ∘ ccom 5555 Fun wfun 6374 Fn wfn 6375 |
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 |
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-ral 3066 df-rex 3067 df-rab 3070 df-v 3410 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-br 5054 df-opab 5116 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-fun 6382 df-fn 6383 |
This theorem is referenced by: fcoOLD 6570 fnfco 6584 fsplitfpar 7887 fipreima 8982 updjudhcoinlf 9548 updjudhcoinrg 9549 cshco 14401 swrdco 14402 isofn 17280 prdsinvlem 18472 prdsmgp 19628 pws1 19634 frlmbas 20717 frlmup3 20762 frlmup4 20763 evlslem1 21042 upxp 22520 uptx 22522 0vfval 28687 xppreima2 30707 psgnfzto1stlem 31086 tocycfvres1 31096 tocycfvres2 31097 cycpmfvlem 31098 cycpmfv3 31101 cycpmco2 31119 sseqfv1 32068 sseqfn 32069 sseqfv2 32073 volsupnfl 35559 ftc1anclem5 35591 ftc1anclem8 35594 choicefi 42413 fourierdlem42 43365 fcoreslem4 44232 ackvalsucsucval 45707 |
Copyright terms: Public domain | W3C validator |