Metamath Proof Explorer

Theorem ofcfval3

Description: General value of ( F oFC R C ) with no assumptions on functionality of F . (Contributed by Thierry Arnoux, 31-Jan-2017)

Ref Expression
Assertion ofcfval3 ⊢ F ∈ V ∧ C ∈ W → F ∘ fc ⁡ R C = x ∈ dom ⁡ F ⟼ F ⁡ x R C

Proof

Step Hyp Ref Expression
1 elex ⊢ F ∈ V → F ∈ V
2 1 adantr ⊢ F ∈ V ∧ C ∈ W → F ∈ V
3 elex ⊢ C ∈ W → C ∈ V
4 3 adantl ⊢ F ∈ V ∧ C ∈ W → C ∈ V
5 dmexg ⊢ F ∈ V → dom ⁡ F ∈ V
6 mptexg ⊢ dom ⁡ F ∈ V → x ∈ dom ⁡ F ⟼ F ⁡ x R C ∈ V
7 5 6 syl ⊢ F ∈ V → x ∈ dom ⁡ F ⟼ F ⁡ x R C ∈ V
8 7 adantr ⊢ F ∈ V ∧ C ∈ W → x ∈ dom ⁡ F ⟼ F ⁡ x R C ∈ V
9 simpl ⊢ f = F ∧ c = C → f = F
10 9 dmeqd ⊢ f = F ∧ c = C → dom ⁡ f = dom ⁡ F
11 9 fveq1d ⊢ f = F ∧ c = C → f ⁡ x = F ⁡ x
12 simpr ⊢ f = F ∧ c = C → c = C
13 11 12 oveq12d ⊢ f = F ∧ c = C → f ⁡ x R c = F ⁡ x R C
14 10 13 mpteq12dv ⊢ f = F ∧ c = C → x ∈ dom ⁡ f ⟼ f ⁡ x R c = x ∈ dom ⁡ F ⟼ F ⁡ x R C
15 df-ofc ⊢ ∘ fc ⁡ R = f ∈ V , c ∈ V ⟼ x ∈ dom ⁡ f ⟼ f ⁡ x R c
16 14 15 ovmpoga ⊢ F ∈ V ∧ C ∈ V ∧ x ∈ dom ⁡ F ⟼ F ⁡ x R C ∈ V → F ∘ fc ⁡ R C = x ∈ dom ⁡ F ⟼ F ⁡ x R C
17 2 4 8 16 syl3anc ⊢ F ∈ V ∧ C ∈ W → F ∘ fc ⁡ R C = x ∈ dom ⁡ F ⟼ F ⁡ x R C