![]() |
Mathbox for Alexander van der Vekens |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > dmfcoafv | Structured version Visualization version GIF version |
Description: Domains of a function composition, analogous to dmfco 6585. (Contributed by Alexander van der Vekens, 23-Jul-2017.) |
Ref | Expression |
---|---|
dmfcoafv | ⊢ ((Fun 𝐺 ∧ 𝐴 ∈ dom 𝐺) → (𝐴 ∈ dom (𝐹 ∘ 𝐺) ↔ (𝐺'''𝐴) ∈ dom 𝐹)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dmfco 6585 | . 2 ⊢ ((Fun 𝐺 ∧ 𝐴 ∈ dom 𝐺) → (𝐴 ∈ dom (𝐹 ∘ 𝐺) ↔ (𝐺‘𝐴) ∈ dom 𝐹)) | |
2 | funres 6230 | . . . . . . 7 ⊢ (Fun 𝐺 → Fun (𝐺 ↾ {𝐴})) | |
3 | 2 | anim2i 607 | . . . . . 6 ⊢ ((𝐴 ∈ dom 𝐺 ∧ Fun 𝐺) → (𝐴 ∈ dom 𝐺 ∧ Fun (𝐺 ↾ {𝐴}))) |
4 | 3 | ancoms 451 | . . . . 5 ⊢ ((Fun 𝐺 ∧ 𝐴 ∈ dom 𝐺) → (𝐴 ∈ dom 𝐺 ∧ Fun (𝐺 ↾ {𝐴}))) |
5 | df-dfat 42722 | . . . . . 6 ⊢ (𝐺 defAt 𝐴 ↔ (𝐴 ∈ dom 𝐺 ∧ Fun (𝐺 ↾ {𝐴}))) | |
6 | afvfundmfveq 42741 | . . . . . 6 ⊢ (𝐺 defAt 𝐴 → (𝐺'''𝐴) = (𝐺‘𝐴)) | |
7 | 5, 6 | sylbir 227 | . . . . 5 ⊢ ((𝐴 ∈ dom 𝐺 ∧ Fun (𝐺 ↾ {𝐴})) → (𝐺'''𝐴) = (𝐺‘𝐴)) |
8 | 4, 7 | syl 17 | . . . 4 ⊢ ((Fun 𝐺 ∧ 𝐴 ∈ dom 𝐺) → (𝐺'''𝐴) = (𝐺‘𝐴)) |
9 | 8 | eqcomd 2785 | . . 3 ⊢ ((Fun 𝐺 ∧ 𝐴 ∈ dom 𝐺) → (𝐺‘𝐴) = (𝐺'''𝐴)) |
10 | 9 | eleq1d 2851 | . 2 ⊢ ((Fun 𝐺 ∧ 𝐴 ∈ dom 𝐺) → ((𝐺‘𝐴) ∈ dom 𝐹 ↔ (𝐺'''𝐴) ∈ dom 𝐹)) |
11 | 1, 10 | bitrd 271 | 1 ⊢ ((Fun 𝐺 ∧ 𝐴 ∈ dom 𝐺) → (𝐴 ∈ dom (𝐹 ∘ 𝐺) ↔ (𝐺'''𝐴) ∈ dom 𝐹)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 387 = wceq 1507 ∈ wcel 2050 {csn 4441 dom cdm 5407 ↾ cres 5409 ∘ ccom 5411 Fun wfun 6182 ‘cfv 6188 defAt wdfat 42719 '''cafv 42720 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2751 ax-sep 5060 ax-nul 5067 ax-pow 5119 ax-pr 5186 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-fal 1520 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2584 df-clab 2760 df-cleq 2772 df-clel 2847 df-nfc 2919 df-ne 2969 df-ral 3094 df-rex 3095 df-rab 3098 df-v 3418 df-sbc 3683 df-csb 3788 df-dif 3833 df-un 3835 df-in 3837 df-ss 3844 df-nul 4180 df-if 4351 df-sn 4442 df-pr 4444 df-op 4448 df-uni 4713 df-int 4750 df-br 4930 df-opab 4992 df-id 5312 df-xp 5413 df-rel 5414 df-cnv 5415 df-co 5416 df-dm 5417 df-res 5419 df-iota 6152 df-fun 6190 df-fn 6191 df-fv 6196 df-aiota 42689 df-dfat 42722 df-afv 42723 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |