Metamath Proof Explorer

Theorem offval2

Description: The function operation expressed as a mapping. (Contributed by Mario Carneiro, 20-Jul-2014)

Ref Expression
Hypotheses offval2.1 ⊢φ→A∈V
offval2.2 ⊢φ∧x∈A→B∈W
offval2.3 ⊢φ∧x∈A→C∈X
offval2.4 ⊢φ→F=x∈A⟼B
offval2.5 ⊢φ→G=x∈A⟼C
Assertion offval2 ⊢φ→FRfG=x∈A⟼BRC

Proof

Step Hyp Ref Expression
1 offval2.1 ⊢φ→A∈V
2 offval2.2 ⊢φ∧x∈A→B∈W
3 offval2.3 ⊢φ∧x∈A→C∈X
4 offval2.4 ⊢φ→F=x∈A⟼B
5 offval2.5 ⊢φ→G=x∈A⟼C
6 2 ralrimiva ⊢φ→∀x∈AB∈W
7 eqid ⊢x∈A⟼B=x∈A⟼B
8 7 fnmpt ⊢∀x∈AB∈W→x∈A⟼BFnA
9 6 8 syl ⊢φ→x∈A⟼BFnA
10 4 fneq1d ⊢φ→FFnA↔x∈A⟼BFnA
11 9 10 mpbird ⊢φ→FFnA
12 3 ralrimiva ⊢φ→∀x∈AC∈X
13 eqid ⊢x∈A⟼C=x∈A⟼C
14 13 fnmpt ⊢∀x∈AC∈X→x∈A⟼CFnA
15 12 14 syl ⊢φ→x∈A⟼CFnA
16 5 fneq1d ⊢φ→GFnA↔x∈A⟼CFnA
17 15 16 mpbird ⊢φ→GFnA
18 inidm ⊢A∩A=A
19 4 adantr ⊢φ∧y∈A→F=x∈A⟼B
20 19 fveq1d ⊢φ∧y∈A→F⁡y=x∈A⟼B⁡y
21 5 adantr ⊢φ∧y∈A→G=x∈A⟼C
22 21 fveq1d ⊢φ∧y∈A→G⁡y=x∈A⟼C⁡y
23 11 17 1 1 18 20 22 offval ⊢φ→FRfG=y∈A⟼x∈A⟼B⁡yRx∈A⟼C⁡y
24 nffvmpt1 ⊢Ⅎ_xx∈A⟼B⁡y
25 nfcv ⊢Ⅎ_xR
26 nffvmpt1 ⊢Ⅎ_xx∈A⟼C⁡y
27 24 25 26 nfov ⊢Ⅎ_xx∈A⟼B⁡yRx∈A⟼C⁡y
28 nfcv ⊢Ⅎ_yx∈A⟼B⁡xRx∈A⟼C⁡x
29 fveq2 ⊢y=x→x∈A⟼B⁡y=x∈A⟼B⁡x
30 fveq2 ⊢y=x→x∈A⟼C⁡y=x∈A⟼C⁡x
31 29 30 oveq12d ⊢y=x→x∈A⟼B⁡yRx∈A⟼C⁡y=x∈A⟼B⁡xRx∈A⟼C⁡x
32 27 28 31 cbvmpt ⊢y∈A⟼x∈A⟼B⁡yRx∈A⟼C⁡y=x∈A⟼x∈A⟼B⁡xRx∈A⟼C⁡x
33 simpr ⊢φ∧x∈A→x∈A
34 7 fvmpt2 ⊢x∈A∧B∈W→x∈A⟼B⁡x=B
35 33 2 34 syl2anc ⊢φ∧x∈A→x∈A⟼B⁡x=B
36 13 fvmpt2 ⊢x∈A∧C∈X→x∈A⟼C⁡x=C
37 33 3 36 syl2anc ⊢φ∧x∈A→x∈A⟼C⁡x=C
38 35 37 oveq12d ⊢φ∧x∈A→x∈A⟼B⁡xRx∈A⟼C⁡x=BRC
39 38 mpteq2dva ⊢φ→x∈A⟼x∈A⟼B⁡xRx∈A⟼C⁡x=x∈A⟼BRC
40 32 39 eqtrid ⊢φ→y∈A⟼x∈A⟼B⁡yRx∈A⟼C⁡y=x∈A⟼BRC
41 23 40 eqtrd ⊢φ→FRfG=x∈A⟼BRC