Metamath Proof Explorer

Theorem off

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

Ref Expression
Hypotheses off.1 
|- ( ( ph /\ ( x e. S /\ y e. T ) ) -> ( x R y ) e. U )
off.2 
|- ( ph -> F : A --> S )
off.3 
|- ( ph -> G : B --> T )
off.4 
|- ( ph -> A e. V )
off.5 
|- ( ph -> B e. W )
off.6 
|- ( A i^i B ) = C
Assertion off 
|- ( ph -> ( F oF R G ) : C --> U )

Proof

Step Hyp Ref Expression
1 off.1 
 |-  ( ( ph /\ ( x e. S /\ y e. T ) ) -> ( x R y ) e. U )
2 off.2 
 |-  ( ph -> F : A --> S )
3 off.3 
 |-  ( ph -> G : B --> T )
4 off.4 
 |-  ( ph -> A e. V )
5 off.5 
 |-  ( ph -> B e. W )
6 off.6 
 |-  ( A i^i B ) = C
7 2 ffnd 
 |-  ( ph -> F Fn A )
8 3 ffnd 
 |-  ( ph -> G Fn B )
9 eqidd 
 |-  ( ( ph /\ z e. A ) -> ( F ` z ) = ( F ` z ) )
10 eqidd 
 |-  ( ( ph /\ z e. B ) -> ( G ` z ) = ( G ` z ) )
11 7 8 4 5 6 9 10 offval 
 |-  ( ph -> ( F oF R G ) = ( z e. C |-> ( ( F ` z ) R ( G ` z ) ) ) )
12 inss1 
 |-  ( A i^i B ) C_ A
13 6 12 eqsstrri 
 |-  C C_ A
14 13 sseli 
 |-  ( z e. C -> z e. A )
15 ffvelrn 
 |-  ( ( F : A --> S /\ z e. A ) -> ( F ` z ) e. S )
16 2 14 15 syl2an 
 |-  ( ( ph /\ z e. C ) -> ( F ` z ) e. S )
17 inss2 
 |-  ( A i^i B ) C_ B
18 6 17 eqsstrri 
 |-  C C_ B
19 18 sseli 
 |-  ( z e. C -> z e. B )
20 ffvelrn 
 |-  ( ( G : B --> T /\ z e. B ) -> ( G ` z ) e. T )
21 3 19 20 syl2an 
 |-  ( ( ph /\ z e. C ) -> ( G ` z ) e. T )
22 1 ralrimivva 
 |-  ( ph -> A. x e. S A. y e. T ( x R y ) e. U )
23 22 adantr 
 |-  ( ( ph /\ z e. C ) -> A. x e. S A. y e. T ( x R y ) e. U )
24 ovrspc2v 
 |-  ( ( ( ( F ` z ) e. S /\ ( G ` z ) e. T ) /\ A. x e. S A. y e. T ( x R y ) e. U ) -> ( ( F ` z ) R ( G ` z ) ) e. U )
25 16 21 23 24 syl21anc 
 |-  ( ( ph /\ z e. C ) -> ( ( F ` z ) R ( G ` z ) ) e. U )
26 11 25 fmpt3d 
 |-  ( ph -> ( F oF R G ) : C --> U )