Metamath Proof Explorer


Theorem off2

Description: The function operation produces a function - alternative form with all antecedents as deduction. (Contributed by Thierry Arnoux, 17-Feb-2017)

Ref Expression
Hypotheses off2.1 φ x S y T x R y U
off2.2 φ F : A S
off2.3 φ G : B T
off2.4 φ A V
off2.5 φ B W
off2.6 φ A B = C
Assertion off2 φ F R f G : C U

Proof

Step Hyp Ref Expression
1 off2.1 φ x S y T x R y U
2 off2.2 φ F : A S
3 off2.3 φ G : B T
4 off2.4 φ A V
5 off2.5 φ B W
6 off2.6 φ A B = C
7 2 ffnd φ F Fn A
8 3 ffnd φ G Fn B
9 eqid A B = A B
10 eqidd φ z A F z = F z
11 eqidd φ z B G z = G z
12 7 8 4 5 9 10 11 offval φ F R f G = z A B F z R G z
13 6 mpteq1d φ z A B F z R G z = z C F z R G z
14 12 13 eqtrd φ F R f G = z C F z R G z
15 2 adantr φ z C F : A S
16 inss1 A B A
17 6 16 eqsstrrdi φ C A
18 17 sselda φ z C z A
19 15 18 ffvelrnd φ z C F z S
20 3 adantr φ z C G : B T
21 inss2 A B B
22 6 21 eqsstrrdi φ C B
23 22 sselda φ z C z B
24 20 23 ffvelrnd φ z C G z T
25 1 ralrimivva φ x S y T x R y U
26 25 adantr φ z C x S y T x R y U
27 ovrspc2v F z S G z T x S y T x R y U F z R G z U
28 19 24 26 27 syl21anc φ z C F z R G z U
29 14 28 fmpt3d φ F R f G : C U