Metamath Proof Explorer

Theorem ofmpteq

Description: Value of a pointwise operation on two functions defined using maps-to notation. (Contributed by Stefan O'Rear, 5-Oct-2014)

Ref Expression
Assertion ofmpteq ⊢A∈V∧x∈A⟼BFnA∧x∈A⟼CFnA→x∈A⟼BRfx∈A⟼C=x∈A⟼BRC

Proof

Step Hyp Ref Expression
1 simp1 ⊢A∈V∧x∈A⟼BFnA∧x∈A⟼CFnA→A∈V
2 simpr ⊢A∈V∧x∈A⟼BFnA∧x∈A⟼CFnA∧a∈A→a∈A
3 simpl2 ⊢A∈V∧x∈A⟼BFnA∧x∈A⟼CFnA∧a∈A→x∈A⟼BFnA
4 eqid ⊢x∈A⟼B=x∈A⟼B
5 4 mptfng ⊢∀x∈AB∈V↔x∈A⟼BFnA
6 3 5 sylibr ⊢A∈V∧x∈A⟼BFnA∧x∈A⟼CFnA∧a∈A→∀x∈AB∈V
7 nfcsb1v ⊢Ⅎ_x⦋a/x⦌B
8 7 nfel1 ⊢Ⅎx⦋a/x⦌B∈V
9 csbeq1a ⊢x=a→B=⦋a/x⦌B
10 9 eleq1d ⊢x=a→B∈V↔⦋a/x⦌B∈V
11 8 10 rspc ⊢a∈A→∀x∈AB∈V→⦋a/x⦌B∈V
12 2 6 11 sylc ⊢A∈V∧x∈A⟼BFnA∧x∈A⟼CFnA∧a∈A→⦋a/x⦌B∈V
13 simpl3 ⊢A∈V∧x∈A⟼BFnA∧x∈A⟼CFnA∧a∈A→x∈A⟼CFnA
14 eqid ⊢x∈A⟼C=x∈A⟼C
15 14 mptfng ⊢∀x∈AC∈V↔x∈A⟼CFnA
16 13 15 sylibr ⊢A∈V∧x∈A⟼BFnA∧x∈A⟼CFnA∧a∈A→∀x∈AC∈V
17 nfcsb1v ⊢Ⅎ_x⦋a/x⦌C
18 17 nfel1 ⊢Ⅎx⦋a/x⦌C∈V
19 csbeq1a ⊢x=a→C=⦋a/x⦌C
20 19 eleq1d ⊢x=a→C∈V↔⦋a/x⦌C∈V
21 18 20 rspc ⊢a∈A→∀x∈AC∈V→⦋a/x⦌C∈V
22 2 16 21 sylc ⊢A∈V∧x∈A⟼BFnA∧x∈A⟼CFnA∧a∈A→⦋a/x⦌C∈V
23 nfcv ⊢Ⅎ_aB
24 23 7 9 cbvmpt ⊢x∈A⟼B=a∈A⟼⦋a/x⦌B
25 24 a1i ⊢A∈V∧x∈A⟼BFnA∧x∈A⟼CFnA→x∈A⟼B=a∈A⟼⦋a/x⦌B
26 nfcv ⊢Ⅎ_aC
27 26 17 19 cbvmpt ⊢x∈A⟼C=a∈A⟼⦋a/x⦌C
28 27 a1i ⊢A∈V∧x∈A⟼BFnA∧x∈A⟼CFnA→x∈A⟼C=a∈A⟼⦋a/x⦌C
29 1 12 22 25 28 offval2 ⊢A∈V∧x∈A⟼BFnA∧x∈A⟼CFnA→x∈A⟼BRfx∈A⟼C=a∈A⟼⦋a/x⦌BR⦋a/x⦌C
30 nfcv ⊢Ⅎ_aBRC
31 nfcv ⊢Ⅎ_xR
32 7 31 17 nfov ⊢Ⅎ_x⦋a/x⦌BR⦋a/x⦌C
33 9 19 oveq12d ⊢x=a→BRC=⦋a/x⦌BR⦋a/x⦌C
34 30 32 33 cbvmpt ⊢x∈A⟼BRC=a∈A⟼⦋a/x⦌BR⦋a/x⦌C
35 29 34 eqtr4di ⊢A∈V∧x∈A⟼BFnA∧x∈A⟼CFnA→x∈A⟼BRfx∈A⟼C=x∈A⟼BRC