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 
|- ( ( ph /\ ( x e. S /\ y e. T ) ) -> ( x R y ) e. U )
off2.2 
|- ( ph -> F : A --> S )
off2.3 
|- ( ph -> G : B --> T )
off2.4 
|- ( ph -> A e. V )
off2.5 
|- ( ph -> B e. W )
off2.6 
|- ( ph -> ( A i^i B ) = C )
Assertion off2 
|- ( ph -> ( F oF R G ) : C --> U )

Proof

Step Hyp Ref Expression
1 off2.1 
 |-  ( ( ph /\ ( x e. S /\ y e. T ) ) -> ( x R y ) e. U )
2 off2.2 
 |-  ( ph -> F : A --> S )
3 off2.3 
 |-  ( ph -> G : B --> T )
4 off2.4 
 |-  ( ph -> A e. V )
5 off2.5 
 |-  ( ph -> B e. W )
6 off2.6 
 |-  ( ph -> ( A i^i B ) = C )
7 2 ffnd 
 |-  ( ph -> F Fn A )
8 3 ffnd 
 |-  ( ph -> G Fn B )
9 eqid 
 |-  ( A i^i B ) = ( A i^i B )
10 eqidd 
 |-  ( ( ph /\ z e. A ) -> ( F ` z ) = ( F ` z ) )
11 eqidd 
 |-  ( ( ph /\ z e. B ) -> ( G ` z ) = ( G ` z ) )
12 7 8 4 5 9 10 11 offval 
 |-  ( ph -> ( F oF R G ) = ( z e. ( A i^i B ) |-> ( ( F ` z ) R ( G ` z ) ) ) )
13 6 mpteq1d 
 |-  ( ph -> ( z e. ( A i^i B ) |-> ( ( F ` z ) R ( G ` z ) ) ) = ( z e. C |-> ( ( F ` z ) R ( G ` z ) ) ) )
14 12 13 eqtrd 
 |-  ( ph -> ( F oF R G ) = ( z e. C |-> ( ( F ` z ) R ( G ` z ) ) ) )
15 2 adantr 
 |-  ( ( ph /\ z e. C ) -> F : A --> S )
16 inss1 
 |-  ( A i^i B ) C_ A
17 6 16 eqsstrrdi 
 |-  ( ph -> C C_ A )
18 17 sselda 
 |-  ( ( ph /\ z e. C ) -> z e. A )
19 15 18 ffvelrnd 
 |-  ( ( ph /\ z e. C ) -> ( F ` z ) e. S )
20 3 adantr 
 |-  ( ( ph /\ z e. C ) -> G : B --> T )
21 inss2 
 |-  ( A i^i B ) C_ B
22 6 21 eqsstrrdi 
 |-  ( ph -> C C_ B )
23 22 sselda 
 |-  ( ( ph /\ z e. C ) -> z e. B )
24 20 23 ffvelrnd 
 |-  ( ( ph /\ z e. C ) -> ( G ` z ) e. T )
25 1 ralrimivva 
 |-  ( ph -> A. x e. S A. y e. T ( x R y ) e. U )
26 25 adantr 
 |-  ( ( ph /\ z e. C ) -> A. x e. S A. y e. T ( x R y ) e. U )
27 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 )
28 19 24 26 27 syl21anc 
 |-  ( ( ph /\ z e. C ) -> ( ( F ` z ) R ( G ` z ) ) e. U )
29 14 28 fmpt3d 
 |-  ( ph -> ( F oF R G ) : C --> U )