![]() |
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 6649 | . . . 4 ⊢ (𝐺 Fn 𝐵 → Fun 𝐺) | |
2 | fncofn 6666 | . . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ Fun 𝐺) → (𝐹 ∘ 𝐺) Fn (◡𝐺 “ 𝐴)) | |
3 | 1, 2 | sylan2 592 | . . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) → (𝐹 ∘ 𝐺) Fn (◡𝐺 “ 𝐴)) |
4 | 3 | 3adant3 1131 | . 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐴) → (𝐹 ∘ 𝐺) Fn (◡𝐺 “ 𝐴)) |
5 | cnvimassrndm 6151 | . . . . 5 ⊢ (ran 𝐺 ⊆ 𝐴 → (◡𝐺 “ 𝐴) = dom 𝐺) | |
6 | 5 | 3ad2ant3 1134 | . . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐴) → (◡𝐺 “ 𝐴) = dom 𝐺) |
7 | fndm 6652 | . . . . 5 ⊢ (𝐺 Fn 𝐵 → dom 𝐺 = 𝐵) | |
8 | 7 | 3ad2ant2 1133 | . . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐴) → dom 𝐺 = 𝐵) |
9 | 6, 8 | eqtr2d 2772 | . . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐴) → 𝐵 = (◡𝐺 “ 𝐴)) |
10 | 9 | fneq2d 6643 | . 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 1540 ⊆ wss 3948 ◡ccnv 5675 dom cdm 5676 ran crn 5677 “ cima 5679 ∘ ccom 5680 Fun wfun 6537 Fn wfn 6538 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2702 ax-sep 5299 ax-nul 5306 ax-pr 5427 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ral 3061 df-rex 3070 df-rab 3432 df-v 3475 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-sn 4629 df-pr 4631 df-op 4635 df-br 5149 df-opab 5211 df-id 5574 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-fun 6545 df-fn 6546 |
This theorem is referenced by: fcoOLD 6742 fnfco 6756 fsplitfpar 8109 fipreima 9364 updjudhcoinlf 9933 updjudhcoinrg 9934 cshco 14794 swrdco 14795 isofn 17729 prdsinvlem 18975 prdsmgp 20052 pws1 20220 frlmbas 21620 frlmup3 21665 frlmup4 21666 evlslem1 21956 upxp 23447 uptx 23449 0vfval 30292 xppreima2 32309 psgnfzto1stlem 32695 tocycfvres1 32705 tocycfvres2 32706 cycpmfvlem 32707 cycpmfv3 32710 cycpmco2 32728 sseqfv1 33852 sseqfn 33853 sseqfv2 33857 volsupnfl 36997 ftc1anclem5 37029 ftc1anclem8 37032 choicefi 44358 fourierdlem42 45324 fcoreslem4 46235 ackvalsucsucval 47536 |
Copyright terms: Public domain | W3C validator |