Metamath Proof Explorer

Theorem ofoafg

Description: Addition operator for functions from sets into ordinals results in a function from the intersection of sets into an ordinal. (Contributed by RP, 5-Jan-2025)

Ref Expression
Assertion ofoafg 
|- ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) ) -> ( oF +o |` ( ( D ^m A ) X. ( E ^m B ) ) ) : ( ( D ^m A ) X. ( E ^m B ) ) --> ( F ^m C ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) -> D e. On )
2 simp1 
 |-  ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) -> A e. V )
3 elmapg 
 |-  ( ( D e. On /\ A e. V ) -> ( f e. ( D ^m A ) <-> f : A --> D ) )
4 1 2 3 syl2anr 
 |-  ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) ) -> ( f e. ( D ^m A ) <-> f : A --> D ) )
5 simp2 
 |-  ( ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) -> E e. On )
6 simp2 
 |-  ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) -> B e. W )
7 elmapg 
 |-  ( ( E e. On /\ B e. W ) -> ( g e. ( E ^m B ) <-> g : B --> E ) )
8 5 6 7 syl2anr 
 |-  ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) ) -> ( g e. ( E ^m B ) <-> g : B --> E ) )
9 8 adantr 
 |-  ( ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) ) /\ f : A --> D ) -> ( g e. ( E ^m B ) <-> g : B --> E ) )
10 simpl 
 |-  ( ( f : A --> D /\ g : B --> E ) -> f : A --> D )
11 10 ffnd 
 |-  ( ( f : A --> D /\ g : B --> E ) -> f Fn A )
12 11 adantl 
 |-  ( ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) ) /\ ( f : A --> D /\ g : B --> E ) ) -> f Fn A )
13 simpr 
 |-  ( ( f : A --> D /\ g : B --> E ) -> g : B --> E )
14 13 ffnd 
 |-  ( ( f : A --> D /\ g : B --> E ) -> g Fn B )
15 14 adantl 
 |-  ( ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) ) /\ ( f : A --> D /\ g : B --> E ) ) -> g Fn B )
16 2 ad2antrr 
 |-  ( ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) ) /\ ( f : A --> D /\ g : B --> E ) ) -> A e. V )
17 6 ad2antrr 
 |-  ( ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) ) /\ ( f : A --> D /\ g : B --> E ) ) -> B e. W )
18 eqid 
 |-  ( A i^i B ) = ( A i^i B )
19 12 15 16 17 18 offn 
 |-  ( ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) ) /\ ( f : A --> D /\ g : B --> E ) ) -> ( f oF +o g ) Fn ( A i^i B ) )
20 simp3 
 |-  ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) -> C = ( A i^i B ) )
21 20 fneq2d 
 |-  ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) -> ( ( f oF +o g ) Fn C <-> ( f oF +o g ) Fn ( A i^i B ) ) )
22 21 ad2antrr 
 |-  ( ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) ) /\ ( f : A --> D /\ g : B --> E ) ) -> ( ( f oF +o g ) Fn C <-> ( f oF +o g ) Fn ( A i^i B ) ) )
23 19 22 mpbird 
 |-  ( ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) ) /\ ( f : A --> D /\ g : B --> E ) ) -> ( f oF +o g ) Fn C )
24 fresin 
 |-  ( f : A --> D -> ( f |` C ) : ( A i^i C ) --> D )
25 24 adantr 
 |-  ( ( f : A --> D /\ g : B --> E ) -> ( f |` C ) : ( A i^i C ) --> D )
26 25 adantl 
 |-  ( ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) ) /\ ( f : A --> D /\ g : B --> E ) ) -> ( f |` C ) : ( A i^i C ) --> D )
27 inss1 
 |-  ( A i^i B ) C_ A
28 20 27 eqsstrdi 
 |-  ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) -> C C_ A )
29 sseqin2 
 |-  ( C C_ A <-> ( A i^i C ) = C )
30 28 29 sylib 
 |-  ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) -> ( A i^i C ) = C )
31 30 ad2antrr 
 |-  ( ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) ) /\ ( f : A --> D /\ g : B --> E ) ) -> ( A i^i C ) = C )
32 31 feq2d 
 |-  ( ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) ) /\ ( f : A --> D /\ g : B --> E ) ) -> ( ( f |` C ) : ( A i^i C ) --> D <-> ( f |` C ) : C --> D ) )
33 26 32 mpbid 
 |-  ( ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) ) /\ ( f : A --> D /\ g : B --> E ) ) -> ( f |` C ) : C --> D )
34 33 ffvelcdmda 
 |-  ( ( ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) ) /\ ( f : A --> D /\ g : B --> E ) ) /\ c e. C ) -> ( ( f |` C ) ` c ) e. D )
35 5 ad3antlr 
 |-  ( ( ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) ) /\ ( f : A --> D /\ g : B --> E ) ) /\ c e. C ) -> E e. On )
36 1 ad3antlr 
 |-  ( ( ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) ) /\ ( f : A --> D /\ g : B --> E ) ) /\ c e. C ) -> D e. On )
37 onelon 
 |-  ( ( D e. On /\ ( ( f |` C ) ` c ) e. D ) -> ( ( f |` C ) ` c ) e. On )
38 36 34 37 syl2anc 
 |-  ( ( ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) ) /\ ( f : A --> D /\ g : B --> E ) ) /\ c e. C ) -> ( ( f |` C ) ` c ) e. On )
39 fresin 
 |-  ( g : B --> E -> ( g |` C ) : ( B i^i C ) --> E )
40 39 adantl 
 |-  ( ( f : A --> D /\ g : B --> E ) -> ( g |` C ) : ( B i^i C ) --> E )
41 40 adantl 
 |-  ( ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) ) /\ ( f : A --> D /\ g : B --> E ) ) -> ( g |` C ) : ( B i^i C ) --> E )
42 inss2 
 |-  ( A i^i B ) C_ B
43 20 42 eqsstrdi 
 |-  ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) -> C C_ B )
44 sseqin2 
 |-  ( C C_ B <-> ( B i^i C ) = C )
45 43 44 sylib 
 |-  ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) -> ( B i^i C ) = C )
46 45 ad2antrr 
 |-  ( ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) ) /\ ( f : A --> D /\ g : B --> E ) ) -> ( B i^i C ) = C )
47 46 feq2d 
 |-  ( ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) ) /\ ( f : A --> D /\ g : B --> E ) ) -> ( ( g |` C ) : ( B i^i C ) --> E <-> ( g |` C ) : C --> E ) )
48 41 47 mpbid 
 |-  ( ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) ) /\ ( f : A --> D /\ g : B --> E ) ) -> ( g |` C ) : C --> E )
49 48 ffvelcdmda 
 |-  ( ( ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) ) /\ ( f : A --> D /\ g : B --> E ) ) /\ c e. C ) -> ( ( g |` C ) ` c ) e. E )
50 oaordi 
 |-  ( ( E e. On /\ ( ( f |` C ) ` c ) e. On ) -> ( ( ( g |` C ) ` c ) e. E -> ( ( ( f |` C ) ` c ) +o ( ( g |` C ) ` c ) ) e. ( ( ( f |` C ) ` c ) +o E ) ) )
51 50 imp 
 |-  ( ( ( E e. On /\ ( ( f |` C ) ` c ) e. On ) /\ ( ( g |` C ) ` c ) e. E ) -> ( ( ( f |` C ) ` c ) +o ( ( g |` C ) ` c ) ) e. ( ( ( f |` C ) ` c ) +o E ) )
52 35 38 49 51 syl21anc 
 |-  ( ( ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) ) /\ ( f : A --> D /\ g : B --> E ) ) /\ c e. C ) -> ( ( ( f |` C ) ` c ) +o ( ( g |` C ) ` c ) ) e. ( ( ( f |` C ) ` c ) +o E ) )
53 oveq1 
 |-  ( d = ( ( f |` C ) ` c ) -> ( d +o E ) = ( ( ( f |` C ) ` c ) +o E ) )
54 53 eliuni 
 |-  ( ( ( ( f |` C ) ` c ) e. D /\ ( ( ( f |` C ) ` c ) +o ( ( g |` C ) ` c ) ) e. ( ( ( f |` C ) ` c ) +o E ) ) -> ( ( ( f |` C ) ` c ) +o ( ( g |` C ) ` c ) ) e. U_ d e. D ( d +o E ) )
55 34 52 54 syl2anc 
 |-  ( ( ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) ) /\ ( f : A --> D /\ g : B --> E ) ) /\ c e. C ) -> ( ( ( f |` C ) ` c ) +o ( ( g |` C ) ` c ) ) e. U_ d e. D ( d +o E ) )
56 12 15 16 17 18 ofres 
 |-  ( ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) ) /\ ( f : A --> D /\ g : B --> E ) ) -> ( f oF +o g ) = ( ( f |` ( A i^i B ) ) oF +o ( g |` ( A i^i B ) ) ) )
57 20 reseq2d 
 |-  ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) -> ( f |` C ) = ( f |` ( A i^i B ) ) )
58 20 reseq2d 
 |-  ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) -> ( g |` C ) = ( g |` ( A i^i B ) ) )
59 57 58 oveq12d 
 |-  ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) -> ( ( f |` C ) oF +o ( g |` C ) ) = ( ( f |` ( A i^i B ) ) oF +o ( g |` ( A i^i B ) ) ) )
60 59 ad2antrr 
 |-  ( ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) ) /\ ( f : A --> D /\ g : B --> E ) ) -> ( ( f |` C ) oF +o ( g |` C ) ) = ( ( f |` ( A i^i B ) ) oF +o ( g |` ( A i^i B ) ) ) )
61 56 60 eqtr4d 
 |-  ( ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) ) /\ ( f : A --> D /\ g : B --> E ) ) -> ( f oF +o g ) = ( ( f |` C ) oF +o ( g |` C ) ) )
62 61 fveq1d 
 |-  ( ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) ) /\ ( f : A --> D /\ g : B --> E ) ) -> ( ( f oF +o g ) ` c ) = ( ( ( f |` C ) oF +o ( g |` C ) ) ` c ) )
63 62 adantr 
 |-  ( ( ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) ) /\ ( f : A --> D /\ g : B --> E ) ) /\ c e. C ) -> ( ( f oF +o g ) ` c ) = ( ( ( f |` C ) oF +o ( g |` C ) ) ` c ) )
64 28 ad2antrr 
 |-  ( ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) ) /\ ( f : A --> D /\ g : B --> E ) ) -> C C_ A )
65 12 64 fnssresd 
 |-  ( ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) ) /\ ( f : A --> D /\ g : B --> E ) ) -> ( f |` C ) Fn C )
66 43 ad2antrr 
 |-  ( ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) ) /\ ( f : A --> D /\ g : B --> E ) ) -> C C_ B )
67 15 66 fnssresd 
 |-  ( ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) ) /\ ( f : A --> D /\ g : B --> E ) ) -> ( g |` C ) Fn C )
68 65 67 jca 
 |-  ( ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) ) /\ ( f : A --> D /\ g : B --> E ) ) -> ( ( f |` C ) Fn C /\ ( g |` C ) Fn C ) )
69 inex1g 
 |-  ( A e. V -> ( A i^i B ) e. _V )
70 2 69 syl 
 |-  ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) -> ( A i^i B ) e. _V )
71 20 70 eqeltrd 
 |-  ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) -> C e. _V )
72 71 ad2antrr 
 |-  ( ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) ) /\ ( f : A --> D /\ g : B --> E ) ) -> C e. _V )
73 72 anim1i 
 |-  ( ( ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) ) /\ ( f : A --> D /\ g : B --> E ) ) /\ c e. C ) -> ( C e. _V /\ c e. C ) )
74 fnfvof 
 |-  ( ( ( ( f |` C ) Fn C /\ ( g |` C ) Fn C ) /\ ( C e. _V /\ c e. C ) ) -> ( ( ( f |` C ) oF +o ( g |` C ) ) ` c ) = ( ( ( f |` C ) ` c ) +o ( ( g |` C ) ` c ) ) )
75 68 73 74 syl2an2r 
 |-  ( ( ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) ) /\ ( f : A --> D /\ g : B --> E ) ) /\ c e. C ) -> ( ( ( f |` C ) oF +o ( g |` C ) ) ` c ) = ( ( ( f |` C ) ` c ) +o ( ( g |` C ) ` c ) ) )
76 63 75 eqtrd 
 |-  ( ( ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) ) /\ ( f : A --> D /\ g : B --> E ) ) /\ c e. C ) -> ( ( f oF +o g ) ` c ) = ( ( ( f |` C ) ` c ) +o ( ( g |` C ) ` c ) ) )
77 simp3 
 |-  ( ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) -> F = U_ d e. D ( d +o E ) )
78 77 ad3antlr 
 |-  ( ( ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) ) /\ ( f : A --> D /\ g : B --> E ) ) /\ c e. C ) -> F = U_ d e. D ( d +o E ) )
79 55 76 78 3eltr4d 
 |-  ( ( ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) ) /\ ( f : A --> D /\ g : B --> E ) ) /\ c e. C ) -> ( ( f oF +o g ) ` c ) e. F )
80 79 ralrimiva 
 |-  ( ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) ) /\ ( f : A --> D /\ g : B --> E ) ) -> A. c e. C ( ( f oF +o g ) ` c ) e. F )
81 fnfvrnss 
 |-  ( ( ( f oF +o g ) Fn C /\ A. c e. C ( ( f oF +o g ) ` c ) e. F ) -> ran ( f oF +o g ) C_ F )
82 80 81 sylan2 
 |-  ( ( ( f oF +o g ) Fn C /\ ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) ) /\ ( f : A --> D /\ g : B --> E ) ) ) -> ran ( f oF +o g ) C_ F )
83 82 expcom 
 |-  ( ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) ) /\ ( f : A --> D /\ g : B --> E ) ) -> ( ( f oF +o g ) Fn C -> ran ( f oF +o g ) C_ F ) )
84 23 83 jcai 
 |-  ( ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) ) /\ ( f : A --> D /\ g : B --> E ) ) -> ( ( f oF +o g ) Fn C /\ ran ( f oF +o g ) C_ F ) )
85 onelon 
 |-  ( ( D e. On /\ d e. D ) -> d e. On )
86 85 adantlr 
 |-  ( ( ( D e. On /\ E e. On ) /\ d e. D ) -> d e. On )
87 simpr 
 |-  ( ( D e. On /\ E e. On ) -> E e. On )
88 87 adantr 
 |-  ( ( ( D e. On /\ E e. On ) /\ d e. D ) -> E e. On )
89 oacl 
 |-  ( ( d e. On /\ E e. On ) -> ( d +o E ) e. On )
90 86 88 89 syl2anc 
 |-  ( ( ( D e. On /\ E e. On ) /\ d e. D ) -> ( d +o E ) e. On )
91 90 ralrimiva 
 |-  ( ( D e. On /\ E e. On ) -> A. d e. D ( d +o E ) e. On )
92 iunon 
 |-  ( ( D e. On /\ A. d e. D ( d +o E ) e. On ) -> U_ d e. D ( d +o E ) e. On )
93 91 92 syldan 
 |-  ( ( D e. On /\ E e. On ) -> U_ d e. D ( d +o E ) e. On )
94 93 3adant3 
 |-  ( ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) -> U_ d e. D ( d +o E ) e. On )
95 77 94 eqeltrd 
 |-  ( ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) -> F e. On )
96 95 adantl 
 |-  ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) ) -> F e. On )
97 96 adantr 
 |-  ( ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) ) /\ ( f : A --> D /\ g : B --> E ) ) -> F e. On )
98 97 72 elmapd 
 |-  ( ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) ) /\ ( f : A --> D /\ g : B --> E ) ) -> ( ( f oF +o g ) e. ( F ^m C ) <-> ( f oF +o g ) : C --> F ) )
99 df-f 
 |-  ( ( f oF +o g ) : C --> F <-> ( ( f oF +o g ) Fn C /\ ran ( f oF +o g ) C_ F ) )
100 98 99 bitrdi 
 |-  ( ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) ) /\ ( f : A --> D /\ g : B --> E ) ) -> ( ( f oF +o g ) e. ( F ^m C ) <-> ( ( f oF +o g ) Fn C /\ ran ( f oF +o g ) C_ F ) ) )
101 84 100 mpbird 
 |-  ( ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) ) /\ ( f : A --> D /\ g : B --> E ) ) -> ( f oF +o g ) e. ( F ^m C ) )
102 101 expr 
 |-  ( ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) ) /\ f : A --> D ) -> ( g : B --> E -> ( f oF +o g ) e. ( F ^m C ) ) )
103 9 102 sylbid 
 |-  ( ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) ) /\ f : A --> D ) -> ( g e. ( E ^m B ) -> ( f oF +o g ) e. ( F ^m C ) ) )
104 103 ralrimiv 
 |-  ( ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) ) /\ f : A --> D ) -> A. g e. ( E ^m B ) ( f oF +o g ) e. ( F ^m C ) )
105 104 ex 
 |-  ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) ) -> ( f : A --> D -> A. g e. ( E ^m B ) ( f oF +o g ) e. ( F ^m C ) ) )
106 4 105 sylbid 
 |-  ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) ) -> ( f e. ( D ^m A ) -> A. g e. ( E ^m B ) ( f oF +o g ) e. ( F ^m C ) ) )
107 106 ralrimiv 
 |-  ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) ) -> A. f e. ( D ^m A ) A. g e. ( E ^m B ) ( f oF +o g ) e. ( F ^m C ) )
108 ofmres 
 |-  ( oF +o |` ( ( D ^m A ) X. ( E ^m B ) ) ) = ( f e. ( D ^m A ) , g e. ( E ^m B ) |-> ( f oF +o g ) )
109 108 fmpo 
 |-  ( A. f e. ( D ^m A ) A. g e. ( E ^m B ) ( f oF +o g ) e. ( F ^m C ) <-> ( oF +o |` ( ( D ^m A ) X. ( E ^m B ) ) ) : ( ( D ^m A ) X. ( E ^m B ) ) --> ( F ^m C ) )
110 107 109 sylib 
 |-  ( ( ( A e. V /\ B e. W /\ C = ( A i^i B ) ) /\ ( D e. On /\ E e. On /\ F = U_ d e. D ( d +o E ) ) ) -> ( oF +o |` ( ( D ^m A ) X. ( E ^m B ) ) ) : ( ( D ^m A ) X. ( E ^m B ) ) --> ( F ^m C ) )