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 )